induction k with
| zero => simp
| succ k ih =>
  simp only [pow_succ, Nat.cast_succ, add_mul, one_mul, add_comm]
  rw [nav.v_mul_eq_add_v, ha, ih]
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
m : ℕ∞
p : R
nav : SurjVal p
a : R
k : ℕ
ha : v nav a = m
⊢ v nav (a ^ k) = ↑k * m
no goals