cases a with
  | zero => simp [nat_valuation_aux]
  | succ a => 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 _ _
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
prime : Nat.Prime p
hp : optParam (1 < p) (_ : 1 < p)
a b : ℕ
⊢ nat_valuation_aux p hp (a * b) = nat_valuation_aux p hp a + nat_valuation_aux p hp b
no goals