induction n with
| zero      =>
  rw [pow_zero]
  exact val_of_one nav
| succ n ih =>
  rw [pow_succ, SurjVal.v_mul_eq_add_v nav, ih, SurjVal.v_uniformizer nav]
  simp [Nat.succ_eq_add_one, add_comm]
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
nav : SurjVal p
n : ℕ
⊢ v nav (p ^ n) = ↑n
no goals