convert nat_val_aux_mul_eq_add p prime prime.one_lt a b <;>
ext <;>
rw [(nat_valuation_of_one_lt p _ prime.one_lt)]
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
prime : Nat.Prime p
a b : ℕ
⊢ nat_valuation p (a * b) = nat_valuation p a + nat_valuation p b
no goals