add new proof

src/Data/Nat.hs

@@ -142,6 +142,10 @@ plus_right_id ∷ Sℕ n → (n :+ Z) :≡ n
 plus_right_id SZ     = Refl
 plus_right_id (SS n) = cong SS (plus_right_id n)
 
+-- | Left identity of addition
+plus_left_id ∷ Sℕ n → (Z :+ n) :≡ n
+plus_left_id n = (plus_commut SZ n) ∾ (plus_right_id n)
+
 -- | Associative property of addition
 plus_assoc ∷ Sℕ a → Sℕ b → Sℕ c → (a :+ b) :+ c :≡ a :+ (b :+ c)
 plus_assoc SZ     _ _ = Refl