cases b with
| zero => simp [nat_valuation_aux]
| succ b =>
exact nat_val_aux'_mul_eq_add p prime prime.one_lt a.succ b.succ _ _
case succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
prime : Nat.Prime p
hp : optParam (1 < p) (_ : 1 < p)
b a : ℕ
⊢ nat_valuation_aux p hp (Nat.succ a * b) = nat_valuation_aux p hp (Nat.succ a) + nat_valuation_aux p hp b
no goals