case inl
b : ℕ
hab : coprime 0 b
⊢ factors (0 * b) ~ factors 0 ++ factors b

case inr
a b : ℕ
hab : coprime a b
ha : a > 0
⊢ factors (a * b) ~ factors a ++ factors b
a b : ℕ
hab : coprime a b
⊢ factors (a * b) ~ factors a ++ factors b
rcases a.eq_zero_or_pos with (rfl | ha)
case inr.inl
a : ℕ
ha : a > 0
hab : coprime a 0
⊢ factors (a * 0) ~ factors a ++ factors 0

case inr.inr
a b : ℕ
hab : coprime a b
ha : a > 0
hb : b > 0
⊢ factors (a * b) ~ factors a ++ factors b
case inr
a b : ℕ
hab : coprime a b
ha : a > 0
⊢ factors (a * b) ~ factors a ++ factors b
rcases b.eq_zero_or_pos with (rfl | hb)
no goals
case inr.inr
a b : ℕ
hab : coprime a b
ha : a > 0
hb : b > 0
⊢ factors (a * b) ~ factors a ++ factors b
exact perm_factors_mul ha.ne' hb.ne'
no goals
case inl
b : ℕ
hab : coprime 0 b
⊢ factors (0 * b) ~ factors 0 ++ factors b
simp [(coprime_zero_left _).mp hab]
no goals
case inr.inl
a : ℕ
ha : a > 0
hab : coprime a 0
⊢ factors (a * 0) ~ factors a ++ factors 0
simp [(coprime_zero_right _).mp hab]