rw [Nat.factorization_mul mnez nnez]
m n : ℕ
mnez : m ≠ 0
nnez : n ≠ 0
p : ℕ
⊢ (m * n).factorization p = m.factorization p + n.factorization p
m n : ℕ
mnez : m ≠ 0
nnez : n ≠ 0
p : ℕ
⊢ (m.factorization + n.factorization) p = m.factorization p + n.factorization p