@@ -54,7 +54,7 @@ plusnO : (m : Nat) -> m + O = m
5454plusnO O = refl
5555plusnO (S k) = eqRespS (plusnO k)
5656
57−plusn_Sm : (n : Nat) -> (m : Nat) -> (plus n (S m)) = S (plus n m)
57+plusn_Sm : (n, m : Nat) -> (plus n (S m)) = S (plus n m)
5858plusn_Sm O m = refl
5959plusn_Sm (S j) m = eqRespS (plusn_Sm _ _)
6060
@@ -73,3 +73,55 @@ plus_assoc : (n, m, p : Nat) -> n + (m + p) = (n + m) + p
7373plus_assoc O m p = refl
7474plus_assoc (S k) m p = let ih = plus_assoc k m p in eqRespS ih
7575
76+data Cmp : Nat -> Nat -> Set where
77+ cmpLT : (y : Nat) -> Cmp x (x + S y)
78+ cmpEQ : Cmp x x
79+ cmpGT : (x : Nat) -> Cmp (y + S x) y
80+
81+cmp : (n, m : Nat) -> Cmp n m
82+cmp O O = cmpEQ
83+cmp (S n) O = cmpGT _
84+cmp O (S n) = cmpLT _
85+cmp (S x) (S y) with (cmp x y)
86+ cmp (S x) (S x) | cmpEQ = cmpEQ
87+ cmp (S (y + S x)) (S y) | cmpGT _ = cmpGT _
88+ cmp (S x) (S (x + S y)) | cmpLT _ = cmpLT _
89+
90+multnO : (n : Nat) -> (n * O) = O
91+multnO O = refl
92+multnO (S k) = multnO k
93+
94+multn_Sm : (n, m : Nat) -> n * S m = n + n * m
95+multn_Sm O m = refl
96+multn_Sm (S k) m = let ih = multn_Sm k m in ?multnSmSk
97+
98+mult_commutes : (n, m : Nat) -> n * m = m * n
99+mult_commutes O m = ?mult_commO
100+mult_commutes (S k) m = let ih = mult_commutes k m in ?mult_commSk
101+
102+mult_commSk = proof {
103+ intro;
104+ intro;
105+ intro;
106+ rewrite sym ih;
107+ rewrite multn_Sm m k;
108+ trivial;
109+}
110+
111+mult_commO = proof {
112+ intro;
113+ rewrite multnO m;
114+ trivial;
115+}
116+
117+multnSmSk = proof {
118+ intro;
119+ intro;
120+ intro;
121+ rewrite plus_commutes (mult k m) m;
122+ rewrite sym (plus_assoc k (mult k m) m);
123+ rewrite ih;
124+ rewrite plus_commutes m (mult k (S m));
125+ trivial;
126+}
127+