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