From 82bcfdd747ac680694c69859def813355cc3efc2 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tom=C3=A1s=20Rivera?= Date: Wed, 5 Aug 2026 17:08:24 +0200 Subject: [PATCH] add next objective --- ZeroToLean/LearningLean/Basic.lean | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) diff --git a/ZeroToLean/LearningLean/Basic.lean b/ZeroToLean/LearningLean/Basic.lean index 0e80f9e..3f7948d 100644 --- a/ZeroToLean/LearningLean/Basic.lean +++ b/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