simp only [pow_succ, Nat.cast_succ, add_mul, one_mul, add_comm]
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 ^ Nat.succ k) = ↑(Nat.succ k) * m
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