simp only [succ_nsmul, pow_succ]
case succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
m : ℕ∞
p : R
nav : SurjVal p
a : R
ha : m ≤ v nav a
k : ℕ
ih : k • m ≤ v nav (a ^ k)
⊢ Nat.succ k • m ≤ v nav (a ^ Nat.succ k)
case succ
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
m : ℕ∞
p : R
nav : SurjVal p
a : R
ha : m ≤ v nav a
k : ℕ
ih : k • m ≤ v nav (a ^ k)
⊢ m + k • m ≤ v nav (a * a ^ k)