simp [nat_valuation_aux]
case zero
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
prime : Nat.Prime p
hp : optParam (1 < p) (_ : 1 < p)
b : ℕ
⊢ nat_valuation_aux p hp (Nat.zero * b) = nat_valuation_aux p hp Nat.zero + nat_valuation_aux p hp b
no goals