cases p
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
case zero
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
m : ℕ
hp : 1 < Nat.succ Nat.zero
⊢ nat_valuation (Nat.succ Nat.zero) m = nat_valuation_aux (Nat.succ Nat.zero) hp m

case succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
m n✝ : ℕ
hp : 1 < Nat.succ (Nat.succ n✝)
⊢ nat_valuation (Nat.succ (Nat.succ n✝)) m = nat_valuation_aux (Nat.succ (Nat.succ n✝)) hp m