Proof left-mult-distr-one. but has yellow
author Yasutaka Higa Thu, 22 May 2014 21:53:48 +0900 e191792472f8 c01d31399879 int.agda 1 files changed, 14 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
```--- 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-one : (n : Int) -> (S n) ≡ S O + 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
∎
```