# HG changeset patch
# User Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
# Date 1400814642 -32400
# Node ID ce0c3af2c34ead24557435e6c2af2ab3bfa31d3c
# Parent  812de82556a27d2dba1928e95416ceaab96780a9
Imporove proof

diff -r 812de82556a2 -r ce0c3af2c34e int.agda
--- a/int.agda	Fri May 23 11:57:11 2014 +0900
+++ b/int.agda	Fri May 23 12:10:42 2014 +0900
@@ -135,11 +135,7 @@
     (S m) + (S n) + (S n * m)
   ≡⟨ sym (sum-assoc (S m) (S n) (S n * m)) ⟩
     (S m) + ((S n) + ((S n) * m))
-  ≡⟨ 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) ⟩
+  ≡⟨ cong (\x -> (S m) + x ) (sym (right-mult-distr-one (S n) m )) ⟩
     S m + S n * S m
   ∎