# HG changeset patch
# User Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
# Date 1400813831 -32400
# Node ID 812de82556a27d2dba1928e95416ceaab96780a9
# Parent  c01d313998791a3940eab574382c5960ded45f30
Proof left-mult-distr-one

diff -r c01d31399879 -r 812de82556a2 int.agda
--- a/int.agda	Fri May 23 11:38:34 2014 +0900
+++ b/int.agda	Fri May 23 11:57:11 2014 +0900
@@ -135,12 +135,15 @@
     (S m) + (S n) + (S n * m)
   ≡⟨ sym (sum-assoc (S m) (S n) (S n * m)) ⟩
     (S m) + ((S n) + ((S n) * m))
-  ≡⟨ cong (\x -> (S m) + x) refl ⟩
+  ≡⟨ sum-sym (S m) (S n + S n * m) ⟩
+     ((S n) + ((S n) * m)) + S m
+  ≡⟨ cong (\x -> x + (S m)) (sym (right-mult-distr-one (S n) m )) ⟩
+    (S n) * (S m) + (S m)
+  ≡⟨ sum-sym (S n * S m) (S m) ⟩
     S m + S n * S m
   ∎
 
 
-
 mult-sym : (n m : Int) -> n * m ≡ m * n
 mult-sym n O     = begin
     n * O