rw [pow_succ, SurjVal.v_mul_eq_add_v nav, ih, SurjVal.v_uniformizer nav]
case succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
n : ℕ
ih : v nav (p ^ n) = ↑n
⊢ v nav (p ^ Nat.succ n) = ↑(Nat.succ n)
case succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
n : ℕ
ih : v nav (p ^ n) = ↑n
⊢ 1 + ↑n = ↑(Nat.succ n)