natural-number-game

Solututions to the Natural Number Game
advanced-multiplication.lean (1344B)

 1 theorem mul_pos (a b : ℕ) : a ≠ 0 → b ≠ 0 → a * b ≠ 0 :=
 2 begin
 3   intros ha hb,
 4   cases b with d,
 5   exfalso,
 6   apply hb,
 7   refl,
 8   rw mul_succ,
 9   rw add_comm,
10   intro h,
11   apply ha,
12   apply add_right_eq_zero,
13   exact h,
14 end
15 
16 theorem eq_zero_or_eq_zero_of_mul_eq_zero (a b : ℕ) 
17                                           (h : a * b = 0) : a = 0 ∨ b = 0 :=
18 begin
19   cases b with c,
20   right,
21   refl,
22   rw mul_succ at h,
23   cases a with d,
24   left,
25   refl,
26   exfalso,
27   rw add_succ at h,
28   apply succ_ne_zero,
29   exact h,
30 end
31 
32 theorem mul_eq_zero_iff (a b : ℕ): a * b = 0 ↔ a = 0 ∨ b = 0 :=
33 begin
34   split,
35   intro h,
36   apply eq_zero_or_eq_zero_of_mul_eq_zero,
37   exact h,
38   intro h,
39   cases h with a_zero b_zero,
40   rw a_zero,
41   rw zero_mul,
42   refl,
43   rw b_zero,
44   rw mul_zero,
45   refl,
46 end
47 
48 theorem mul_left_cancel (a b c : ℕ) (ha : a ≠ 0) : a * b = a * c → b = c :=
49 begin
50   revert b,
51   induction c with n,
52   rw mul_zero,
53   intros b h,
54   cases eq_zero_or_eq_zero_of_mul_eq_zero a b h with a_zero b_zero,
55   exfalso,
56   apply ha,
57   exact a_zero,
58   exact b_zero,
59   intro b,
60   intro h,
61   cases b with d,
62   exfalso,
63   rw mul_zero at h,
64   rw mul_succ at h,
65   symmetry at h,
66   apply ha,
67   exact add_left_eq_zero h,
68   rw mul_succ at h,
69   rw mul_succ at h,
70   have p := add_right_cancel _ _ _ h,
71   have q := c_ih d p,
72   rw q,
73   refl,
74 end