natural-number-game

Solututions to the Natural Number Game

NameSizeMode
..
advanced-multiplication.lean 1344B -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
theorem mul_pos (a b : ℕ) : a ≠ 0 → b ≠ 0 → a * b ≠ 0 :=
begin
  intros ha hb,
  cases b with d,
  exfalso,
  apply hb,
  refl,
  rw mul_succ,
  rw add_comm,
  intro h,
  apply ha,
  apply add_right_eq_zero,
  exact h,
end

theorem eq_zero_or_eq_zero_of_mul_eq_zero (a b : ℕ) 
                                          (h : a * b = 0) : a = 0 ∨ b = 0 :=
begin
  cases b with c,
  right,
  refl,
  rw mul_succ at h,
  cases a with d,
  left,
  refl,
  exfalso,
  rw add_succ at h,
  apply succ_ne_zero,
  exact h,
end

theorem mul_eq_zero_iff (a b : ℕ): a * b = 0 ↔ a = 0 ∨ b = 0 :=
begin
  split,
  intro h,
  apply eq_zero_or_eq_zero_of_mul_eq_zero,
  exact h,
  intro h,
  cases h with a_zero b_zero,
  rw a_zero,
  rw zero_mul,
  refl,
  rw b_zero,
  rw mul_zero,
  refl,
end

theorem mul_left_cancel (a b c : ℕ) (ha : a ≠ 0) : a * b = a * c → b = c :=
begin
  revert b,
  induction c with n,
  rw mul_zero,
  intros b h,
  cases eq_zero_or_eq_zero_of_mul_eq_zero a b h with a_zero b_zero,
  exfalso,
  apply ha,
  exact a_zero,
  exact b_zero,
  intro b,
  intro h,
  cases b with d,
  exfalso,
  rw mul_zero at h,
  rw mul_succ at h,
  symmetry at h,
  apply ha,
  exact add_left_eq_zero h,
  rw mul_succ at h,
  rw mul_succ at h,
  have p := add_right_cancel _ _ _ h,
  have q := c_ih d p,
  rw q,
  refl,
end