Formal mathematics laboratory
Lumenary.AdditionSubtraction
Addition, subtraction and place value to 100
Formal library
seven_eq_three_add_fourtheoremProved here from basic factsNo axioms
seven_eq_three_add_fourLean 4Proved here from basic factsFormally verified /-- `7 = 3 + 4` is a true statement: the two sides have the same value. The answer does not have to come after the equals sign. -/ theorem seven_eq_three_add_four : 7 = 3 + 4 := rflthree_add_four_eq_four_add_threetheoremProved here from basic factsNo axioms
three_add_four_eq_four_add_threeLean 4Proved here from basic factsFormally verified /-- `3 + 4 = 4 + 3` is also true, although neither side is "the answer": both sides are 7. -/ theorem three_add_four_eq_four_add_three : 3 + 4 = 4 + 3 := rflcount_ontheoremProved here from basic factsNo axioms
count_onLean 4Proved here from basic factsFormally verified /-- Counting on one more: adding `b + 1` is adding `b` and then one more. In Lean this is how addition is *defined*, so `rfl` proves it. Everything below is built on this rule. -/ theorem count_on (a b : Nat) : a + (b + 1) = (a + b) + 1 := rfladd_zero_eqtheoremProved here from basic factsNo axioms
add_zero_eqLean 4Proved here from basic factsFormally verified /-- Adding zero changes nothing: `a + 0 = a` (also true by definition). -/ theorem add_zero_eq (a : Nat) : a + 0 = a := rflzero_add_eqtheoremProved here from basic factsNo axioms
zero_add_eqLean 4Proved here from basic factsFormally verified /-- Zero added to a number also changes nothing: `0 + a = a`. This is *not* true by definition, so we prove it by induction on `a`, counting on one step at a time. -/ theorem zero_add_eq (a : Nat) : 0 + a = a := by induction a with | zero => rfl | succ k ih => calc 0 + (k + 1) = (0 + k) + 1 := count_on 0 k _ = k + 1 := by rw [ih]succ_add_eqtheoremProved here from basic factsNo axioms
succ_add_eqLean 4Proved here from basic factsFormally verified /-- One more, then add `b`, is the same as add `b`, then one more: `(a + 1) + b = (a + b) + 1`. A helper for the turn-around rule, proved by induction on `b`. -/ theorem succ_add_eq (a b : Nat) : (a + 1) + b = (a + b) + 1 := by induction b with | zero => rfl | succ k ih => calc (a + 1) + (k + 1) = ((a + 1) + k) + 1 := count_on (a + 1) k _ = ((a + k) + 1) + 1 := by rw [ih] _ = (a + (k + 1)) + 1 := rfladd_comm_from_countingtheoremProved here from basic factsNo axioms
add_comm_from_countingLean 4Proved here from basic factsFormally verified /-- **The turn-around rule** `a + b = b + a`, proved by induction on `b` from counting on. Compare `add_comm_library`, which applies the theorem already in core Lean. -/ theorem add_comm_from_counting (a b : Nat) : a + b = b + a := by induction b with | zero => exact (zero_add_eq a).symm | succ k ih => calc a + (k + 1) = (a + k) + 1 := count_on a k _ = (k + a) + 1 := by rw [ih] _ = (k + 1) + a := (succ_add_eq k a).symmadd_comm_librarytheoremApplies a library theoremNo axioms
add_comm_libraryLean 4Applies a library theoremFormally verified /-- The turn-around rule again, this time by applying core Lean's `Nat.add_comm`. -/ theorem add_comm_library (a b : Nat) : a + b = b + a := Nat.add_comm a badd_assoc_from_countingtheoremProved here from basic factsNo axioms
add_assoc_from_countingLean 4Proved here from basic factsFormally verified /-- **Regrouping** `(a + b) + c = a + (b + c)`: when adding three numbers, it does not matter which two we add first. Proved by induction on `c` (core Lean: `Nat.add_assoc`). -/ theorem add_assoc_from_counting (a b c : Nat) : (a + b) + c = a + (b + c) := by induction c with | zero => rfl | succ k ih => calc (a + b) + (k + 1) = ((a + b) + k) + 1 := count_on (a + b) k _ = (a + (b + k)) + 1 := by rw [ih] _ = a + (b + (k + 1)) := rflmake_tentheoremProved here from basic factsNo axioms
make_tenLean 4Proved here from basic factsFormally verified /-- **Making ten**: `8 + 5 = 10 + 3`. Split 5 into 2 and 3, give the 2 to the 8 to make ten, and 3 is left. The middle step is regrouping (`add_assoc_from_counting`). -/ theorem make_ten : 8 + 5 = 10 + 3 := calc 8 + 5 = 8 + (2 + 3) := rfl _ = (8 + 2) + 3 := (add_assoc_from_counting 8 2 3).symm _ = 10 + 3 := rflsub_undoes_addtheoremProved here from basic factspropext
sub_undoes_addLean 4Proved here from basic factsFormally verified /-- **Taking away undoes adding**: `(a + b) − b = a`. Proved by induction on `b`: taking away one more from one more leaves the same as before (core Lean's `Nat.add_sub_add_right`). -/ theorem sub_undoes_add (a b : Nat) : (a + b) - b = a := by induction b with | zero => rfl | succ k ih => calc (a + (k + 1)) - (k + 1) = ((a + k) + 1) - (k + 1) := rfl _ = (a + k) - k := Nat.add_sub_add_right (a + k) 1 k _ = a := ihsub_undoes_add_librarytheoremApplies a library theorempropext
sub_undoes_add_libraryLean 4Applies a library theoremFormally verified /-- Taking away undoes adding, by applying core Lean's `Nat.add_sub_cancel`. -/ theorem sub_undoes_add_library (a b : Nat) : (a + b) - b = a := Nat.add_sub_cancel a bfact_familytheoremProved here from basic factsNo axioms
fact_familyLean 4Proved here from basic factsFormally verified /-- A fact family: the numbers 3, 4 and 7 give two addition facts and two subtraction facts. `decide` asks Lean to check all four. -/ theorem fact_family : 3 + 4 = 7 ∧ 4 + 3 = 7 ∧ 7 - 4 = 3 ∧ 7 - 3 = 4 := by decidecannot_take_five_from_threetheoremProved here from basic factspropext, Quot.sound
cannot_take_five_from_threeLean 4Proved here from basic factsFormally verified /-- We cannot take 5 away from 3 and land on a counting number: no `n` satisfies `n + 5 = 3`. So `5 − 3 = 2`, but `3 − 5` has no answer among the counting numbers — subtraction does not turn around. (Lean's built-in `3 - 5` returns `0` by convention, "take away as many as you can"; that is why we state the fact this way.) -/ theorem cannot_take_five_from_three : ¬ ∃ n : Nat, n + 5 = 3 := by intro ⟨n, h⟩ -- `n + 5 = 3` would need `n + 5` to be at most 3, but it is at least 5. omegaAxioms used: propext, Quot.soundformal/Lumenary/AdditionSubtraction.leanTry it in the Lean web editortensdefDefinitionNo axioms
tensLean 4Formally verified /-- The number of whole tens in `n` (the left digit of a two-digit number). -/ def tens (n : Nat) : Nat := n / 10onesdefDefinitionNo axioms
onesLean 4Formally verified /-- The ones left over after taking out the tens (the right digit). -/ def ones (n : Nat) : Nat := n % 10fifty_twotheoremProved here from basic factsNo axioms
fifty_twoLean 4Proved here from basic factsFormally verified /-- 52 is five tens and two ones — not "five and two". -/ theorem fifty_two : tens 52 = 5 ∧ ones 52 = 2 := ⟨rfl, rfl⟩tens_and_onestheoremApplies a library theorempropext
tens_and_onesLean 4Applies a library theoremFormally verified /-- Every number is made of its tens and ones: `10 × tens + ones = n`. This applies core Lean's `Nat.div_add_mod`. -/ theorem tens_and_ones (n : Nat) : 10 * tens n + ones n = n := Nat.div_add_mod n 10tens_ones_uniquetheoremProved here from basic factspropext, Classical.choice, Quot.sound
tens_ones_uniqueLean 4Proved here from basic factsFormally verified /-- There is only one way to write a number as tens and ones with fewer than ten ones: `10 × t + o` (with `o < 10`) has exactly `t` tens and `o` ones. The `omega` tactic decides facts like this about whole numbers, including division and remainder by a fixed number. -/ theorem tens_ones_unique (t o : Nat) (ho : o < 10) : tens (10 * t + o) = t ∧ ones (10 * t + o) = o := by unfold tens ones omegaAxioms used: propext, Classical.choice, Quot.soundformal/Lumenary/AdditionSubtraction.leanTry it in the Lean web editormore_tens_biggertheoremProved here from basic factspropext
more_tens_biggerLean 4Proved here from basic factsFormally verified /-- **More tens means bigger**, whatever the ones are: if `a` has fewer tens than `b`, then `a < b`. Even with 9 ones, `a` stays below the next ten, and that ten is at most `b` (e.g. `47 < 50 ≤ 52`). -/ theorem more_tens_bigger (a b : Nat) (h : tens a < tens b) : a < b := calc a = 10 * tens a + ones a := (tens_and_ones a).symm _ < 10 * tens a + 10 := Nat.add_lt_add_left (Nat.mod_lt a (by decide)) _ _ = 10 * (tens a + 1) := (Nat.mul_succ 10 (tens a)).symm _ ≤ 10 * tens b := Nat.mul_le_mul_left 10 h _ ≤ 10 * tens b + ones b := Nat.le_add_right _ _ _ = b := tens_and_ones bsame_tens_more_onestheoremProved here from basic factspropext
same_tens_more_onesLean 4Proved here from basic factsFormally verified /-- **Same tens, then compare the ones**: if `a` and `b` have the same tens and `a` has fewer ones, then `a < b` (e.g. `63 < 68`). -/ theorem same_tens_more_ones (a b : Nat) (ht : tens a = tens b) (ho : ones a < ones b) : a < b := calc a = 10 * tens a + ones a := (tens_and_ones a).symm _ = 10 * tens b + ones a := by rw [ht] _ < 10 * tens b + ones b := Nat.add_lt_add_left ho _ _ = b := tens_and_ones bcompare_47_52theoremProved here from basic factspropext
compare_47_52Lean 4Proved here from basic factsFormally verified /-- 47 is less than 52, because 4 tens are fewer than 5 tens. -/ theorem compare_47_52 : 47 < 52 := more_tens_bigger 47 52 (by decide)