case intro
n a : ℕ
h' : n * a ≠ 0
⊢ factors n <+ factors (n * a)
n k : ℕ
h : n ∣ k
h' : k ≠ 0
⊢ factors n <+ factors k
obtain ⟨a, rfl⟩ := h
no goals
case intro
n a : ℕ
h' : n * a ≠ 0
⊢ factors n <+ factors (n * a)
exact factors_sublist_right (right_ne_zero_of_mul h')