--- a/int.agda	Wed May 21 14:41:45 2014 +0900
+++ b/int.agda	Wed May 21 14:44:52 2014 +0900
@@ -8,9 +8,9 @@
 n + O     = n
 n + (S m) = S (n + m)
 
-plus-one : (n m : Int) -> (S n) + m ≡ S (n + m)
-plus-one  n    O  = sym refl
-plus-one  n (S m) = cong S (plus-one n m)
+left-increment : (n m : Int) -> (S n) + m ≡ S (n + m)
+left-increment  n    O  = refl
+left-increment  n (S m) = cong S (left-increment n m)
 
 double : Int -> Int
 double O = O
@@ -24,11 +24,11 @@
     (S n) + (S m)  
   ≡⟨ refl ⟩
     S ((S n) + m)
-  ≡⟨ cong S (plus-one 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 (plus-one m n)) ⟩
+  ≡⟨ sym (cong S (left-increment m n)) ⟩
     S ((S m) + n)
   ≡⟨ refl ⟩
     (S m) + (S n)