natural-number-game

Solututions to the Natural Number Game
multiplication.lean (1493B)

 1 lemma zero_mul (m : ℕ) : 0 * m = 0 :=
 2 begin
 3   induction m,
 4   rw mul_zero,
 5   refl,
 6   rw mul_succ,
 7   rw add_zero,
 8   rw m_ih,
 9   refl,
10 end
11 
12 lemma mul_one (m : ℕ) : m * 1 = m :=
13 begin
14   rw one_eq_succ_zero,
15   rw mul_succ,
16   rw mul_zero,
17   rw zero_add,
18   refl,
19 end
20 
21 lemma one_mul (m : ℕ) : 1 * m = m :=
22 begin
23   induction m,
24   rw mul_zero,
25   refl,
26   rw mul_succ,
27   rw m_ih,
28   rw succ_eq_add_one,
29   refl,
30 end
31 
32 lemma mul_add (t a b : ℕ) : t * (a + b) = t * a + t * b :=
33 begin
34   induction b,
35   rw mul_zero,
36   repeat {rw add_zero},
37   rw add_succ,
38   repeat {rw mul_succ},
39   rw ← add_assoc,
40   rw b_ih,
41   refl,
42 end
43 
44 lemma mul_assoc (a b c : ℕ) : (a * b) * c = a * (b * c) :=
45 begin
46   induction c,
47   repeat {rw mul_zero},
48   repeat {rw mul_succ},
49   rw mul_add,
50   rw c_ih,
51   refl,
52 end
53 
54 lemma succ_mul (a b : ℕ) : succ a * b = a * b + b :=
55 begin
56   induction b,
57   repeat {rw mul_zero},
58   rw add_zero,
59   refl,
60   repeat {rw mul_succ},
61   rw b_ih,
62   repeat {rw add_succ},
63   rw add_right_comm,
64   refl,
65 end
66 
67 lemma add_mul (a b t : ℕ) : (a + b) * t = a * t + b * t :=
68 begin
69   induction b,
70   rw zero_mul,
71   repeat {rw add_zero},
72   rw add_succ,
73   repeat {rw succ_mul},
74   rw b_ih,
75   rw add_assoc,
76   refl,
77 end
78 
79 lemma mul_comm (a b : ℕ) : a * b = b * a :=
80 begin
81   induction b,
82   rw mul_zero,
83   rw zero_mul,
84   refl,
85   rw mul_succ,
86   rw succ_mul,
87   rw b_ih,
88   refl,
89 end
90 
91 lemma mul_left_comm (a b c : ℕ) : a * (b * c) = b * (a * c) :=
92 begin
93   rw ← mul_assoc,
94   rw mul_comm a b,
95   rw mul_assoc,
96   refl,
97 end