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