natural-number-game

Solututions to the Natural Number Game

Commit
02138a0d05235fd880e76f45f7468f2ecd8b5a9e
Parent
7cc38e35cb4e6e354f44fb2fff0e2e2762d84f6d
Author
Pablo <pablo-escobar@riseup.net>
Date

Wrote down the solutions to the addition world

Diffstat

1 file changed, 57 insertions, 0 deletions

Status File Name N° Changes Insertions Deletions
Added addition.lean 57 57 0 
diff --git a/addition.lean b/addition.lean
@@ -0,0 +1,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