simp [nat_valuation]
case succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
q : ℕ
hp : 1 < Nat.succ (Nat.succ q)
n✝ : ℕ
⊢ nat_valuation (Nat.succ (Nat.succ q)) (Nat.succ n✝) = nat_valuation_aux (Nat.succ (Nat.succ q)) hp (Nat.succ n✝)
no goals