rw [nav.v_mul_eq_add_v, ha, ih]
case succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
m : ℕ∞
p : R
nav : SurjVal p
a : R
ha : v nav a = m
k : ℕ
ih : v nav (a ^ k) = ↑k * m
⊢ v nav (a * a ^ k) = m + ↑k * m
no goals