case inl
b : ℕ
hb : b ≠ 0
⊢ factorization 0 ≤ factorization (0 * b)

case inr
a b : ℕ
hb : b ≠ 0
ha : a ≠ 0
⊢ factorization a ≤ factorization (a * b)
a b : ℕ
hb : b ≠ 0
⊢ factorization a ≤ factorization (a * b)
rcases eq_or_ne a 0 with (rfl | ha)
case inr
a b : ℕ
hb : b ≠ 0
ha : a ≠ 0
⊢ a ∣ a * b
case inr
a b : ℕ
hb : b ≠ 0
ha : a ≠ 0
⊢ factorization a ≤ factorization (a * b)
rw [factorization_le_iff_dvd ha <| mul_ne_zero ha hb]
no goals
case inr
a b : ℕ
hb : b ≠ 0
ha : a ≠ 0
⊢ a ∣ a * b
exact Dvd.intro b rfl
no goals
case inl
b : ℕ
hb : b ≠ 0
⊢ factorization 0 ≤ factorization (0 * b)
simp