a b : ℕ
ha : a ≠ 0
⊢ factorization b ≤ factorization (b * a)
a b : ℕ
ha : a ≠ 0
⊢ factorization b ≤ factorization (a * b)
rw [mul_comm]
no goals
a b : ℕ
ha : a ≠ 0
⊢ factorization b ≤ factorization (b * a)
apply factorization_le_factorization_mul_left ha