@@ -1,8 +1,25 @@
11module Data.Nat
22
33%default total
4+%access public export
45
56diff : Nat -> Nat -> Nat
67diff k Z = k
78diff Z j = j
89diff (S k) (S j) = diff k j
10+
11+ltePlus : LTE m1 n1 -> LTE m2 n2 -> LTE (m1 + m2) (n1 + n2)
12+ltePlus {n1=Z} LTEZero lte = lte
13+ltePlus {n1=S k} LTEZero lte = lteSuccRight $ ltePlus {n1=k} LTEZero lte
14+ltePlus (LTESucc lte1) lte2 = LTESucc $ ltePlus lte1 lte2
15+
16+lteCongPlus : (k : Nat) -> LTE m n -> LTE (m + k) (n + k)
17+lteCongPlus k lte = ltePlus lte lteRefl
18+
19+lteMult : LTE m1 n1 -> LTE m2 n2 -> LTE (m1 * m2) (n1 * n2)
20+lteMult LTEZero _ = LTEZero
21+lteMult {m1=S k} (LTESucc _) LTEZero = rewrite multZeroRightZero k in LTEZero
22+lteMult (LTESucc lte1) (LTESucc lte2) = LTESucc $ ltePlus lte2 $ lteMult lte1 $ LTESucc lte2
23+
24+lteCongMult : (k : Nat) -> LTE m n -> LTE (m * k) (n * k)
25+lteCongMult k lte = lteMult lte lteRefl