# HG changeset patch
# User Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
# Date 1400674294 -32400
# Node ID e191792472f8c4ee5b26e24b9a8a1b8ad939da5f
# Parent  f922e687f3a1869b9769b6f81abf6dc65c164900
Try proof mult-sym. but not completed.

diff -r f922e687f3a1 -r e191792472f8 int.agda
--- a/int.agda	Wed May 21 16:05:50 2014 +0900
+++ b/int.agda	Wed May 21 21:11:34 2014 +0900
@@ -14,6 +14,11 @@
 n + O     = n
 n + (S m) = S (n + m)
 
+left-add-zero : (n : Int) -> O + n ≡ n
+left-add-zero O     = refl
+left-add-zero (S n) = cong S (left-add-zero n)
+
+
 left-increment : (n m : Int) -> (S n) + m ≡ S (n + m)
 left-increment  n    O  = refl
 left-increment  n (S m) = cong S (left-increment n m)
@@ -51,4 +56,88 @@
 _*_ : Int -> Int -> Int
 n *    O  = O
 n * (S O) = n
-n * (S m) = n + (n * m)
\ No newline at end of file
+n * (S m) = n + (n * m)
+
+right-mult-zero : (n : Int) -> n * O ≡ O
+right-mult-zero n = refl
+
+right-mult-one : (n : Int) -> n * (S O) ≡ n
+right-mult-one n = refl
+
+right-mult-distr-one : (n m : Int) -> n * (S m) ≡ n + (n * m)
+right-mult-distr-one    O     O  = refl
+right-mult-distr-one    O  (S m) = refl
+right-mult-distr-one (S n)    O  = refl
+right-mult-distr-one (S n) (S m) = refl
+
+
+left-mult-zero : (n : Int) -> O * n ≡ O
+left-mult-zero O     = refl
+left-mult-zero (S n) = begin
+    O * (S n)
+  ≡⟨ right-mult-distr-one O n ⟩
+    O + (O * n)
+  ≡⟨ sum-sym O (O * n) ⟩
+    (O * n) + O
+  ≡⟨ refl ⟩
+    (O * n)
+  ≡⟨ left-mult-zero n ⟩
+    O
+  ∎
+
+left-mult-one : (n : Int) -> (S O) * n ≡ n
+left-mult-one    O  = refl
+left-mult-one (S n) = begin
+    (S O) * S n
+  ≡⟨ right-mult-distr-one (S O) n ⟩
+    (S O) + ((S O) * n)
+  ≡⟨ cong (_+_ (S O)) (left-mult-one n) ⟩
+    (S O) + n
+  ≡⟨ sum-sym (S O) n ⟩
+    n + (S O)
+  ≡⟨ refl ⟩
+    S n
+  ∎
+
+
+left-mult-distr-one : (n m : Int) -> (S n) * m ≡ m + (n * m)
+left-mult-distr-one    O     O  = refl
+left-mult-distr-one    O  (S m) = begin
+    (S O) * S m
+  ≡⟨ left-mult-one (S m) ⟩
+    S m
+  ≡⟨ refl ⟩
+    S m + O
+  ≡⟨ cong (_+_ (S m)) (sym (left-mult-zero (S m))) ⟩
+    S m + (O * S m)
+  ∎
+left-mult-distr-one (S n)    O  = refl
+left-mult-distr-one (S n) (S m) = begin
+    S (S n) * S m
+  ≡⟨ right-mult-distr-one (S (S n)) m ⟩
+    (S (S n)) + ((S (S n)) * m)
+  ≡⟨ cong (\x -> (S (S n)) + x) (left-mult-distr-one (S n) m) ⟩
+    S (S n) + (m + S n * m)
+  ≡⟨ {!!} ⟩
+    S m + S n * S m
+  ∎
+
+
+
+mult-sym : (n m : Int) -> n * m ≡ m * n
+mult-sym n O     = begin
+    n * O
+  ≡⟨ refl ⟩
+    O
+  ≡⟨ sym (left-mult-zero n) ⟩
+    O * n
+  ∎
+mult-sym n (S m) = begin
+    n * (S m)
+  ≡⟨ right-mult-distr-one n m ⟩
+    n + (n * m)
+  ≡⟨ cong (\x -> n + x ) (mult-sym n m) ⟩
+    n + (m * n)
+  ≡⟨ sym (left-mult-distr-one m n)  ⟩
+    (S m) * n
+  ∎