# HG changeset patch
# User Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
# Date 1400820810 -32400
# Node ID 5a81867278afb511e3ada19291961758b8f1a07d
# Parent  ce0c3af2c34ead24557435e6c2af2ab3bfa31d3c
Imporve proof for sum-sym

diff -r ce0c3af2c34e -r 5a81867278af int.agda
--- a/int.agda	Fri May 23 12:10:42 2014 +0900
+++ b/int.agda	Fri May 23 13:53:30 2014 +0900
@@ -26,22 +26,18 @@
 left-increment  n    O  = refl
 left-increment  n (S m) = cong S (left-increment n m)
 
-sum-sym : (n : Int) (m : Int) -> n + m ≡ m + n
+sum-sym : (x : Int) (y : Int) -> x + y ≡ y + x
 sum-sym    O     O  = refl
-sum-sym    O  (S m) = cong S (sum-sym O m)
-sum-sym (S n)    O  = cong S (sum-sym n O)
-sum-sym (S n) (S m) = begin
-    (S n) + (S m)  
+sum-sym    O  (S y) = cong S (sum-sym O y)
+sum-sym (S x)    O  = cong S (sum-sym x O)
+sum-sym (S x) (S y) = begin
+    (S x) + (S y)
   ≡⟨ refl ⟩
-    S ((S n) + m)
-  ≡⟨ cong S (left-increment n m)⟩
-    S (S (n + m))
-  ≡⟨ cong (\x -> S (S x)) (sum-sym n m) ⟩
-    S (S (m + n))
-  ≡⟨ sym (cong S (left-increment m n)) ⟩
-    S ((S m) + n)
-  ≡⟨ refl ⟩
-    (S m) + (S n)
+    S ((S x) + y)
+  ≡⟨ cong S (sum-sym (S x) y) ⟩
+    S (y + (S x))
+  ≡⟨ (sym (left-increment y (S x))) ⟩
+    (S y) + (S x)
   ∎
 
 sum-assoc : (x y z : Int) -> x + (y + z) ≡ (x + y) + z