Addition, subtraction and place value to 100

Priya helps her uncle at his fruit stall in a busy market in Chennai, India. The mangoes arrive in crates. Each crate holds ten mangoes.

In the morning, one customer buys 8 mangoes and another buys 5. How many mangoes did they buy altogether? Later, Priya counts 52 mangoes on the stall and sells 27 of them. How many are left?

Priya could count every mango one by one. But there are faster ways — and they all come from a few big ideas about putting together, taking away, and tens and ones.

Adding means putting two groups together and finding how many there are altogether. If you have 3 red beads and 4 blue beads, put them together: there are 7 beads. We write $3 + 4 = 7$.

You don't have to count everything again. Start at the bigger number and count on: for $8 + 3$, say eight and count on three more: nine, ten, eleven.

Subtracting has two meanings.

• Taking away: you have 7 beads and give away 3. How many are left? $7 - 3 = 4$.
• Comparing: Amina has 12 shells and Lucas has 7. How many more does Amina have? Pair them up: 7 of Amina's shells have partners, and 5 do not. So Amina has 5 more: $12 - 7 = 5$.

Adding and taking away are like doing and undoing. If you put 3 beads in a bag and then take 3 beads out, you are back where you started.

Ten is a very friendly number. To add $8 + 5$, move 2 of the 5 dots up to fill the first ten-frame. Now there is a full ten and 3 more:

Press Make ten to watch it happen. Then change the numbers and try $9 + 4$ and $7 + 6$.

The turn-around rule. Put 3 red beads and 4 blue beads in a row. Read the row from the left and you say $3 + 4$. Walk round to the other side and read it from the left again: now you say $4 + 3$. It is the same row of beads, so it has the same number of beads. That is why $3 + 4 = 4 + 3$ — and the same is true for any two numbers.

Making ten. When adding three numbers, it doesn't matter which two we add first: $(8 + 2) + 3 = 8 + (2 + 3)$. Both mean "all the beads in three little piles". Making ten uses this to swap a hard sum, $8 + 5$, for an easy one, $10 + 3$.

Adding zero. Putting together a group with an empty group changes nothing: $a + 0 = a$.

Taking away undoes adding. A bag has 9 beads in it. Put in 4 more, then take 4 beads out. You have taken away exactly as many as you put in, so 9 are left: $(9 + 4) - 4 = 9$.

Subtraction does not turn around. $5 - 3 = 2$: take 3 beads from 5 and 2 are left. But $3 - 5$? You cannot take 5 beads from a bag with only 3. So $5 - 3$ and $3 - 5$ are not the same.

Why the tens decide. The biggest number with 4 tens is 49. The smallest number with 5 tens is 50. So every number with 4 tens is smaller than every number with 5 tens. That is why we compare the tens first.

Gideon reads every number sentence as a statement that is either true or false. What do you think?

1. "$7 = 3 + 4$" — True. The answer does not have to come after the equals sign.
2. "$3 + 4 = 4 + 3$" — True. Both sides are worth 7.
3. "$5 - 3 = 3 - 5$" — False! $5 - 3 = 2$, but we cannot take 5 away from 3.
4. "52 has 5 tens." — True. 52 is 5 tens and 2 ones.

/-- 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 := rfl

/-- `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 := rfl

/-- `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 := rfl

/-- **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).symm

/-- 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 b

/-- **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 := rfl

/-- **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 := ih

/-- 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 decide

/-- 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.
  omega

/-- 52 is five tens and two ones — not "five and two". -/
theorem fifty_two : tens 52 = 5 ∧ ones 52 = 2 := ⟨rfl, rfl⟩

/-- 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 10

/-- **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 b

/-- **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 b

The computer also checked that "tens first, then ones" picks the bigger number for all 10,000 pairs of numbers from 0 to 99, and it did every two-digit addition and subtraction with answers up to 99 using tens and ones. It found something neat: exactly as many take-aways need a ten broken as additions need ten ones traded — because each take-away undoes an addition.

"""Addition facts, take-away, and tens-and-ones, checked case by case.

Children learn the addition facts up to 10 + 10, the turn-around rule
a + b = b + a, that taking away undoes adding, and the written methods for
adding and subtracting two-digit numbers with tens and ones. A computer can
check all of these for every case in a finite range: all 121 facts
a + b with a, b from 0 to 10, every number from 0 to 99, all 10,000 pairs
of such numbers, and every two-digit addition and subtraction whose answer
stays between 0 and 99.

These are exhaustive checks of finitely many cases. They show the rules hold
in this range; why they hold for all numbers is a proof (see the lesson).

Runs unchanged in the browser (Pyodide) using only the standard library.
"""

import textwrap

def facts(limit=10):
    """All addition facts (a, b, a + b) with 0 <= a, b <= limit."""
    return [(a, b, a + b) for a in range(limit + 1) for b in range(limit + 1)]

def facts_to_learn(limit=10):
    """Facts left to learn when a + b and b + a count as one fact."""
    return sorted({(min(a, b), max(a, b)) for a, b, _ in facts(limit)})

def take_away(a, b):
    """a - b as a counting number, or None when b > a (no answer)."""
    return a - b if b <= a else None

def tens_ones(n):
    """Split 0 <= n <= 99 into (tens, ones)."""
    if not 0 <= n <= 99:
        raise ValueError("expected a number from 0 to 99")
    return divmod(n, 10)

def less_by_place_value(a, b):
    """Decide a < b by comparing tens first, then ones."""
    (ta, oa), (tb, ob) = tens_ones(a), tens_ones(b)
    return ta < tb or (ta == tb and oa < ob)

def column_add(a, b):
    """Add two numbers up to 99 by columns; return (sum, regrouped?)."""
    (ta, oa), (tb, ob) = tens_ones(a), tens_ones(b)
    ones = oa + ob
    carry = 1 if ones >= 10 else 0
    tens = ta + tb + carry
    if tens > 9:
        raise ValueError("the sum is 100 or more")
    return 10 * tens + (ones - 10 * carry), bool(carry)

def column_subtract(a, b):
    """Subtract b <= a <= 99 by columns; return (difference, regrouped?)."""
    if b > a:
        raise ValueError("cannot take a bigger number from a smaller one")
    (ta, oa), (tb, ob) = tens_ones(a), tens_ones(b)
    borrow = 1 if oa < ob else 0
    ones = oa + 10 * borrow - ob
    tens = ta - borrow - tb
    return 10 * tens + ones, bool(borrow)

def main():
    table = facts()
    learn = facts_to_learn()
    turn = sum(a + b == b + a for a, b, _ in table)
    undo = sum(take_away(s, b) == a for a, b, s in table)
    print(f"1. Addition facts from 0 + 0 to 10 + 10: {len(table)} facts")
    print(f"   a + b = b + a holds in {turn} of {len(table)}")
    print(f"   using the turn-around rule, only {len(learn)} facts to learn")
    print(f"   (a + b) - b = a holds in {undo} of {len(table)}")
    pairs = [(a, b) for a in range(11) for b in range(11)]
    both = [(a, b) for a, b in pairs
            if take_away(a, b) is not None and take_away(b, a) is not None]
    print(f"2. Does subtraction turn around? 5 - 3 = {take_away(5, 3)},")
    print("   but 3 - 5 has no answer among the counting numbers")
    print(f"   pairs from 0..10 where a - b and b - a both exist: {len(both)}")
    print("   (only a = b, and then both are 0)")
    forms = sorted(10 * t + o for t in range(10) for o in range(10))
    print("3. Tens and ones: 52 =", tens_ones(52)[0], "tens and",
          tens_ones(52)[1], "ones")
    print(f"   every number 0-99 has exactly one form: {forms == list(range(100))}")
    agree = sum(less_by_place_value(a, b) == (a < b)
                for a in range(100) for b in range(100))
    print(f"   'tens first, then ones' agrees with a < b in {agree:,} of 10,000")
    sums = [(a, b) for a in range(100) for b in range(100 - a)]
    add_ok = sum(column_add(a, b)[0] == a + b for a, b in sums)
    add_re = sum(column_add(a, b)[1] for a, b in sums)
    diffs = [(a, b) for a in range(100) for b in range(a + 1)]
    sub_ok = sum(column_subtract(a, b)[0] == a - b for a, b in diffs)
    sub_re = sum(column_subtract(a, b)[1] for a, b in diffs)
    print("4. Column methods (answers from 0 to 99):")
    print(f"   38 + 25 -> {column_add(38, 25)}   52 - 27 -> "
          f"{column_subtract(52, 27)}   (answer, regrouped?)")
    print(f"   addition: {add_ok:,} of {len(sums):,} correct, "
          f"{add_re:,} needed a regroup")
    print(f"   subtraction: {sub_ok:,} of {len(diffs):,} correct, "
          f"{sub_re:,} needed a regroup")
    print("   (the same count: each take-away undoes one of the additions)")
    print()
    print(textwrap.fill(
        "Epistemic status: exact, exhaustive checks of finitely many cases "
        "(121 facts, 100 numbers, 10,000 comparisons, 5,050 sums and 5,050 "
        "differences). They show the rules work in this range and nothing "
        "beyond it; the proofs in the lesson explain why they hold for all "
        "whole numbers.",
        width=78,
    ))

if __name__ == "__main__":
    main()

Use whatever helps: your fingers, counting on, making ten, or tens and ones. Hints are there whenever you want them.

• In Mesopotamia, about 4,000 years ago, Babylonian scribes wrote numbers with place value in base sixty.
• In China, counting rods were laid out in columns for ones, tens, hundreds, …, with an empty space for zero. Rod arithmetic is described in old texts such as the Sunzi Suanjing, written roughly 1,600 years ago.
• The Maya of Central America wrote numbers with place value, counting mostly in twenties, and used a sign for zero.
• In ancient Egypt, hieroglyphic numerals were not place value: one symbol for one, another for ten, another for a hundred, repeated as often as needed.
• The base-ten digits used across much of the world today, with place value and zero, were developed in India. They became known in the Islamic world through writers such as al-Khwārizmī in Baghdad (9th century), and in Europe partly through Fibonacci's Liber Abaci (1202).
• The signs $+$ and $-$ appeared in print in a German arithmetic book by Johannes Widmann in 1489. The equals sign was invented by the Welsh mathematician Robert Recorde in The Whetstone of Witte (1557), who chose two parallel lines "bicause noe .2. thynges, can be moare equalle".

• Hung-Hsi Wu, Understanding Numbers in Elementary School Mathematics (2011) — addition, subtraction and place value developed carefully for teachers.
• Liping Ma, Knowing and Teaching Elementary Mathematics (1999) — includes a famous chapter on teaching subtraction with regrouping.
• Thomas P. Carpenter, Megan Loef Franke and Linda Levi, Thinking Mathematically: Integrating Arithmetic and Algebra in Elementary School (2003) — on children's ideas about the equals sign and true/false number sentences.
• Karl Menninger, Number Words and Number Symbols: A Cultural History of Numbers (1958; English translation 1969).