did some basic arithmetic

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
+theorem zero_add_nat
-#check Nat.one_add
+  : 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