natural-number-game

Solututions to the Natural Number Game

NameSizeMode
..
multiplication.lean 1493B -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
94
95
96
97
lemma zero_mul (m : ℕ) : 0 * m = 0 :=
begin
  induction m,
  rw mul_zero,
  refl,
  rw mul_succ,
  rw add_zero,
  rw m_ih,
  refl,
end

lemma mul_one (m : ℕ) : m * 1 = m :=
begin
  rw one_eq_succ_zero,
  rw mul_succ,
  rw mul_zero,
  rw zero_add,
  refl,
end

lemma one_mul (m : ℕ) : 1 * m = m :=
begin
  induction m,
  rw mul_zero,
  refl,
  rw mul_succ,
  rw m_ih,
  rw succ_eq_add_one,
  refl,
end

lemma mul_add (t a b : ℕ) : t * (a + b) = t * a + t * b :=
begin
  induction b,
  rw mul_zero,
  repeat {rw add_zero},
  rw add_succ,
  repeat {rw mul_succ},
  rw ← add_assoc,
  rw b_ih,
  refl,
end

lemma mul_assoc (a b c : ℕ) : (a * b) * c = a * (b * c) :=
begin
  induction c,
  repeat {rw mul_zero},
  repeat {rw mul_succ},
  rw mul_add,
  rw c_ih,
  refl,
end

lemma succ_mul (a b : ℕ) : succ a * b = a * b + b :=
begin
  induction b,
  repeat {rw mul_zero},
  rw add_zero,
  refl,
  repeat {rw mul_succ},
  rw b_ih,
  repeat {rw add_succ},
  rw add_right_comm,
  refl,
end

lemma add_mul (a b t : ℕ) : (a + b) * t = a * t + b * t :=
begin
  induction b,
  rw zero_mul,
  repeat {rw add_zero},
  rw add_succ,
  repeat {rw succ_mul},
  rw b_ih,
  rw add_assoc,
  refl,
end

lemma mul_comm (a b : ℕ) : a * b = b * a :=
begin
  induction b,
  rw mul_zero,
  rw zero_mul,
  refl,
  rw mul_succ,
  rw succ_mul,
  rw b_ih,
  refl,
end

lemma mul_left_comm (a b c : ℕ) : a * (b * c) = b * (a * c) :=
begin
  rw ← mul_assoc,
  rw mul_comm a b,
  rw mul_assoc,
  refl,
end