From ca8f2814a04d96f21a016c4a9392a40240ce5099 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Tom=C3=A1s=20Rivera?= <tomas.riveral@icloud.com>
Date: Thu, 6 Aug 2026 11:51:44 +0200
Subject: [PATCH] did some basic arithmetic

---
 ZeroToLean/LearningLean/Basic.lean | 37 ++++++++++++++++++++++++++++--
 1 file changed, 35 insertions(+), 2 deletions(-)

diff --git a/ZeroToLean/LearningLean/Basic.lean b/ZeroToLean/LearningLean/Basic.lean
index 3f7948d..ce12d84 100644
--- a/ZeroToLean/LearningLean/Basic.lean
+++ b/ZeroToLean/LearningLean/Basic.lean
@@ -276,13 +276,46 @@ theorem true_or_equal_true
 end basicLogic
 
 namespace basicArithmetic
+variable {n: Nat}
+variable {m: Nat}
 #check Nat.add_zero
+theorem add_zero_nat
+  : n + 0 = n := by
+    trivial
+
 #check Nat.zero_add
-#check Nat.add_one
-#check Nat.one_add
+theorem zero_add_nat
+  : 0 + n = n := by
+    ring
+
 #check Nat.add_comm
+theorem add_commutative (n m : Nat)
+  : n + m = m + n := by
+    ring
+
+#check Nat.add_one
+theorem add_one_equal_succ (n: Nat)
+  : n + 1 = n.succ := by
+    trivial
+
+#check Nat.one_add
+theorem one_add_equal_succ (n: Nat)
+  : 1 + n = n.succ := by
+    calc
+      1 + n = n + 1 := add_commutative 1 n
+      _ = n.succ := add_one_equal_succ n
+
+
 #check Nat.add_left_comm
+theorem add_commutative_left (n m k: Nat)
+  : n + (m + k) = m + (n + k) := by
+    ring
+
 #check Nat.add_right_comm
+theorem add_commutative_right (n m k: Nat)
+  : n + m + k = n + k + m := by
+    ring
+
 #check Nat.add_assoc
 #check Eq.symm
 #check Eq.trans