natural-number-game
Solututions to the Natural Number Game
Name | Size | Mode | |
.. | |||
advanced-addition.lean | 1760B | -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 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93
theorem succ_inj' {a b : mynat} (hs : succ(a) = succ(b)) : a = b := begin apply succ_inj, exact hs, end theorem succ_succ_inj {a b : mynat} (h : succ(succ(a)) = succ(succ(b))) : a = b := begin apply succ_inj, apply succ_inj, exact h, end theorem succ_eq_succ_of_eq {a b : mynat} : a = b → succ(a) = succ(b) := begin intro h, rw h, refl, end theorem succ_eq_succ_iff (a b : mynat) : succ a = succ b ↔ a = b := begin split, exact succ_inj, exact succ_eq_succ_of_eq, end theorem add_right_cancel (a t b : mynat) : a + t = b + t → a = b := begin induction t, intro h, repeat {rw add_zero at h}, exact h, intro h, repeat {rw add_succ at h}, apply t_ih, exact succ_inj h, end theorem add_left_cancel (t a b : mynat) : t + a = t + b → a = b := begin rw add_comm t, rw add_comm t, exact add_right_cancel a t b, end lemma eq_zero_of_add_right_eq_self {a b : mynat} : a + b = a → b = 0 := begin intro h, rw ← add_zero a at h, rw add_assoc at h, rw zero_add at h, apply add_left_cancel a b 0, exact h, end theorem succ_ne_zero (a : mynat) : succ a ≠ 0 := begin symmetry, exact zero_ne_succ a, end lemma add_left_eq_zero {a b : mynat} (h : a + b = 0) : b = 0 := begin cases b with d, refl, exfalso, rw add_succ at h, apply succ_ne_zero (a + d), exact h, end lemma add_right_eq_zero {a b : mynat} : a + b = 0 → a = 0 := begin rw add_comm, apply add_left_eq_zero, end lemma ne_succ_self (n : mynat) : n ≠ succ n := begin intro h, rw succ_eq_add_one at h, rw ← add_zero n at h, rw add_assoc at h, rw zero_add at h, have p := add_left_cancel n 0 1 h, rw one_eq_succ_zero at p, apply succ_ne_zero 0, symmetry, exact p, end