case inl
a : ℕ
ha : a ≠ 0
h : factors a <+~ factors 0
⊢ a ∣ 0

case inr
a b : ℕ
ha : a ≠ 0
h : factors a <+~ factors b
hb : b > 0
⊢ a ∣ b
a b : ℕ
ha : a ≠ 0
h : factors a <+~ factors b
⊢ a ∣ b
rcases b.eq_zero_or_pos with (rfl | hb)
case inr.zero
b : ℕ
hb : b > 0
ha : zero ≠ 0
h : factors zero <+~ factors b
⊢ zero ∣ b

case inr.succ.zero
b : ℕ
hb : b > 0
ha : succ zero ≠ 0
h : factors (succ zero) <+~ factors b
⊢ succ zero ∣ b

case inr.succ.succ
b : ℕ
hb : b > 0
a : ℕ
ha : succ (succ a) ≠ 0
h : factors (succ (succ a)) <+~ factors b
⊢ succ (succ a) ∣ b
case inr
a b : ℕ
ha : a ≠ 0
h : factors a <+~ factors b
hb : b > 0
⊢ a ∣ b
rcases a with (_ | _ | a)
case inr.succ.succ
b : ℕ
hb : b > 0
a : ℕ
ha : succ (succ a) ≠ 0
h : factors (succ (succ a)) <+~ factors b
⊢ b = succ (succ a) * prod (List.diff (factors b) (factors (succ (succ a))))
case inr.succ.succ
b : ℕ
hb : b > 0
a : ℕ
ha : succ (succ a) ≠ 0
h : factors (succ (succ a)) <+~ factors b
⊢ succ (succ a) ∣ b
use (@List.diff _ instBEq b.factors a.succ.succ.factors).prod
case inr.succ.succ
b : ℕ
hb : b > 0
a : ℕ
ha : succ (succ a) ≠ 0
h : factors (succ (succ a)) <+~ factors b
⊢ b = prod (factors (succ (succ a))) * prod (List.diff (factors b) (factors (succ (succ a))))
case inr.succ.succ
b : ℕ
hb : b > 0
a : ℕ
ha : succ (succ a) ≠ 0
h : factors (succ (succ a)) <+~ factors b
⊢ b = succ (succ a) * prod (List.diff (factors b) (factors (succ (succ a))))
nth_rw 1 [← Nat.prod_factors ha]
no goals
case inr.succ.succ
b : ℕ
hb : b > 0
a : ℕ
ha : succ (succ a) ≠ 0
h : factors (succ (succ a)) <+~ factors b
⊢ b = prod (factors (succ (succ a))) * prod (List.diff (factors b) (factors (succ (succ a))))
rw [← List.prod_append,
  List.Perm.prod_eq <| List.subperm_append_diff_self_of_count_le <| List.subperm_ext_iff.mp h,
  Nat.prod_factors hb.ne']
no goals
case inl
a : ℕ
ha : a ≠ 0
h : factors a <+~ factors 0
⊢ a ∣ 0
exact dvd_zero _
no goals
case inr.zero
b : ℕ
hb : b > 0
ha : zero ≠ 0
h : factors zero <+~ factors b
⊢ zero ∣ b
exact (ha rfl).elim
no goals
case inr.succ.zero
b : ℕ
hb : b > 0
ha : succ zero ≠ 0
h : factors (succ zero) <+~ factors b
⊢ succ zero ∣ b
exact one_dvd _