git.iko.soy/Idris-dev
on master help sign in
Merge pull request #4600 from stop-cran/lteProofs
5ce5a36Niklas Larsson
libs/contrib/Data/Nat.idr+17
compare with master
unifiedsplit
@@ -1,8 +1,25 @@
1module Data.Nat
1module Data.Nat
2
2
3%default total
3%default total
4+%access public export
4
5
5diff : Nat -> Nat -> Nat
6diff : Nat -> Nat -> Nat
6diff k Z = k
7diff k Z = k
7diff Z j = j
8diff Z j = j
8diff (S k) (S j) = diff k j
9diff (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