add next objective

ZeroToLean/LearningLean/Basic.lean

@@ -274,3 +274,25 @@ theorem true_or_equal_true
 #check not_and_or
 
 end basicLogic
+
+namespace basicArithmetic
+#check Nat.add_zero
+#check Nat.zero_add
+#check Nat.add_one
+#check Nat.one_add
+#check Nat.add_comm
+#check Nat.add_left_comm
+#check Nat.add_right_comm
+#check Nat.add_assoc
+#check Eq.symm
+#check Eq.trans
+#check Nat.le_of_lt
+#check Nat.le_trans
+#check Nat.add_le_add_right
+#check Nat.add_le_add_left
+#check Nat.add_left_cancel
+#check Nat.add_right_cancel
+#check Nat.mul_add
+#check Nat.mul_left_comm
+#check Nat.mul_right_comm
+end basicArithmetic