case h
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
⊢ ↑(factorization (a * b)) p = ↑(factorization a + factorization b) p
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ factorization (a * b) = factorization a + factorization b
ext p
no goals
case h
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
⊢ ↑(factorization (a * b)) p = ↑(factorization a + factorization b) p
simp only [add_apply, ← factors_count_eq, perm_iff_count.mp (perm_factors_mul ha hb) p,
  count_append]