# HG changeset patch
# User Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
# Date 1400763228 -32400
# Node ID 8ad92d8306796911ecf8c265010f6d681409c741
# Parent  e191792472f8c4ee5b26e24b9a8a1b8ad939da5f
Proof left-mult-distr-one. but has yellow

diff -r e191792472f8 -r 8ad92d830679 int.agda
--- a/int.agda	Wed May 21 21:11:34 2014 +0900
+++ b/int.agda	Thu May 22 21:53:48 2014 +0900
@@ -18,6 +18,9 @@
 left-add-zero O     = refl
 left-add-zero (S n) = cong S (left-add-zero n)
 
+left-add-one : (n : Int) -> (S n) ≡ S O + n
+left-add-one    O  = refl
+left-add-one (S n) = cong S (left-add-one n)
 
 left-increment : (n m : Int) -> (S n) + m ≡ S (n + m)
 left-increment  n    O  = refl
@@ -118,7 +121,17 @@
     (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)
-  ≡⟨ {!!} ⟩
+  ≡⟨ cong (\x -> x + (m + S n * m)) (left-add-one (S n)) ⟩
+    (S O) + (S n) + (m + S n * m)
+  ≡⟨ sum-assoc ((S O) + (S n)) m (S n * m)  ⟩
+    (S O) + (S n) + m + S n * m
+  ≡⟨ cong (\x -> x + m + S n * m) (sum-sym (S O) (S n)) ⟩
+    (S n) + (S O) + m + S n * m
+  ≡⟨ cong (\x -> (S n) + x + (S n * m)) refl ⟩
+    (S n) + (S m) + S n * m
+  ≡⟨ cong (\x -> x + S n * m) (sum-sym (S n) (S m)) ⟩
+    (S m) + (S n) + S n * m
+  ≡⟨ cong (\x -> (S m + x)) refl ⟩
     S m + S n * S m
   ∎