natural-number-game
Solututions to the Natural Number Game
Name | Size | Mode | |
.. | |||
addition.lean | 896B | -rw-r--r-- |
01 02 03 04 05 06 07 08 09 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57
lemma zero_add (n : ℕ) : 0 + n = n := begin induction n, rw add_zero, refl, rw add_succ, rw n_ih, refl, end lemma add_assoc (a b c : ℕ) : (a + b) + c = a + (b + c) := begin induction c, repeat {rw add_zero}, repeat {rw add_succ}, rw c_ih, refl, end lemma succ_add (a b : ℕ) : succ a + b = succ (a + b) := begin induction b with c, repeat {rw add_zero}, repeat {rw add_succ}, rw b_ih, refl, end lemma add_comm (a b : ℕ) : a + b = b + a := begin induction b, rw add_zero, rw zero_add, refl, rw add_succ, rw succ_add, rw b_ih, refl, end theorem succ_eq_add_one (n : ℕ) : succ n = n + 1 := begin rw one_eq_succ_zero, rw add_succ, rw add_zero, refl, end lemma add_right_comm (a b c : ℕ) : a + b + c = a + c + b := begin induction c with d, repeat {rw add_zero}, repeat {rw add_succ}, rw c_ih, rw succ_add, refl, end