diff --git a/src/Data/Nat.hs b/src/Data/Nat.hs
index b1b6991..1a4001e 100644
--- a/src/Data/Nat.hs
+++ b/src/Data/Nat.hs
@@ -121,14 +121,22 @@ switch SZ     m = Refl
 switch (SS n) m = cong SS (switch n m)
 
 -- | Lemma
-succ ∷ Sℕ n → Sℕ m → S (n :+ m) :≡ (n :+ S m)
-succ SZ     m = Refl
-succ (SS n) m = cong SS (succ n m)
+succ_right ∷ Sℕ n → Sℕ m → S (n :+ m) :≡ (n :+ S m)
+succ_right SZ     m = Refl
+succ_right (SS n) m = cong SS (succ_right n m)
+
+-- | Lemma
+succ_left ∷ Sℕ n → Sℕ m → S (n :+ m) :≡ (S n :+ m)
+succ_left n m = succ_right n m ∾ switch n m
 
 -- | Relation between successor and addition
 succ_plus ∷ Sℕ n → (n :+ S Z) :≡ S n
 succ_plus n = switch n SZ ∾ plus_right_id (SS n)
 
+-- | Successor of predecessor
+succ_pred ∷ Sℕ (S n) → S (Pred n) :≡ n
+succ_pred (SS (SS n)) = Refl
+
 -- | Right identity of addition
 plus_right_id ∷ Sℕ n → (n :+ Z) :≡ n
 plus_right_id SZ     = Refl
@@ -143,5 +151,4 @@ plus_assoc (SS a) b c = cong SS (plus_assoc a b c)
 plus_commut ∷ Sℕ n → Sℕ m → (n :+ m) :≡ (m :+ n)
 plus_commut n   SZ    = plus_right_id n
 plus_commut n  (SS m) =
-  (sym (succ n m) ∾ cong SS (plus_commut n m)) ∾
-  (succ m n ∾ switch m n)
+  sym (succ_right n m) ∾ cong SS (plus_commut n m) ∾ succ_left m n