no goals
p a b : ℕ
hab : coprime a b
⊢ ↑(factorization (a * b)) p = ↑(factorization a) p + ↑(factorization b) p
simp only [← factors_count_eq, perm_iff_count.mp (perm_factors_mul_of_coprime hab), count_append]