cases p
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p m : ℕ
hp : 1 < p
⊢ nat_valuation p m = nat_valuation_aux p hp m
case zero
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
m : ℕ
hp : 1 < Nat.zero
⊢ nat_valuation Nat.zero m = nat_valuation_aux Nat.zero hp m

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