Order.idr

module Order

%access public export
%default total

ltLte : m `LT` n -> m `LTE` n
ltLte (LTESucc x) = lteSuccRight x

ltLteTransitive : m `LT` n -> n `LTE` p -> m `LT` p
ltLteTransitive (LTESucc x) (LTESucc y) = LTESucc $ lteTransitive x y

plusLtMonoLeft : (p:Nat) -> m `LT` n -> p + m `LT` p + n
plusLtMonoLeft Z     ltmn = ltmn
plusLtMonoLeft (S p) ltmn = LTESucc (plusLtMonoLeft p ltmn)

plusLteMonoLeft : (p:Nat) -> m `LTE` n -> p + m `LTE` p + n
plusLteMonoLeft Z x = x
plusLteMonoLeft (S k) x = LTESucc (plusLteMonoLeft k x)

plusLtMonoRight : (p:Nat) -> m `LT` n -> m + p `LT` n + p
plusLtMonoRight {m=m} {n=n} p ltmn =
  rewrite plusCommutative m p in
  rewrite plusCommutative n p in
  plusLtMonoLeft p ltmn

plusLtLteMono : m `LT` n -> p `LTE` q -> m + p `LT` n + q
plusLtLteMono {n} {p} ltmn ltepq =
  let prf  = plusLtMonoRight p ltmn in
  let prf' = plusLteMonoLeft n ltepq in
  ltLteTransitive prf prf'

plusLtMono : m `LT` n -> p `LT` q -> m + p `LT` n + q
plusLtMono ltmn ltpq = plusLtLteMono ltmn (ltLte ltpq)

multLtMonoLeft : 0 `LT` p -> m `LT` n -> p * m `LT` p * n
multLtMonoLeft {p = S Z} {m} _ ltmn@(LTESucc {right = r} y) =
  rewrite multOneLeftNeutral m in
  rewrite multOneLeftNeutral r in
  ltmn
multLtMonoLeft {p = S (S p)} _ ltmn =
  let IH = multLtMonoLeft {p = S p} (LTESucc LTEZero) ltmn in
  plusLtMono ltmn IH

multLtSelfRight : (k : Nat) -> 0 `LT` m -> 1 `LT` k -> m `LT` m * k
multLtSelfRight {m} k zeroLtM oneLtK =
  let prf = multLtMonoLeft zeroLtM oneLtK in
  replace {P = \x => Nat.LT x (m*k)} (multOneRightNeutral m) prf

multLtNonZeroArgumentsLeft : 0 `LT` m * n -> 0 `LT` m
multLtNonZeroArgumentsLeft {m = Z} x = absurd x
multLtNonZeroArgumentsLeft {m = (S k)} x = LTESucc LTEZero

multLtNonZeroArgumentsRight : 0 `LT` m * n -> 0 `LT` n
multLtNonZeroArgumentsRight {n = Z} {m} x = replace (multZeroRightZero m) x
multLtNonZeroArgumentsRight {n = (S k)} x = LTESucc LTEZero