natural-number-game

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