exact nat_val_aux'_mul_eq_add p prime prime.one_lt a.succ b.succ _ _
case succ.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 (Nat.succ a * Nat.succ b) =
    nat_valuation_aux p hp (Nat.succ a) + nat_valuation_aux p hp (Nat.succ b)
no goals