# HG changeset patch
# User Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
# Date 1400651564 -32400
# Node ID a3cf5cb2b7d38921b3402851ce9529fac5c9daef
# Parent  6b1230883bfa7cd81c01f4c9475ce05f1d1d128e
Auto proof sum-assoc

diff -r 6b1230883bfa -r a3cf5cb2b7d3 int.agda
--- a/int.agda	Wed May 21 14:44:52 2014 +0900
+++ b/int.agda	Wed May 21 14:52:44 2014 +0900
@@ -33,3 +33,13 @@
   ≡⟨ refl ⟩
     (S m) + (S n)
   ∎
+
+sum-assoc : (x y z : Int) -> x + (y + z) ≡ (x + y) + z
+sum-assoc O O O = refl
+sum-assoc O O (S z) = cong S (sum-assoc O O z)
+sum-assoc O (S y) O = refl
+sum-assoc O (S y) (S z) = cong S (sum-assoc O (S y) z)
+sum-assoc (S x) O O = refl
+sum-assoc (S x) O (S z) = cong S (sum-assoc (S x) O z)
+sum-assoc (S x) (S y) O = refl
+sum-assoc (S x) (S y) (S z) = cong S (sum-assoc (S x) (S y) z)