induction k with
| zero => simp [zero_nsmul]
| succ k ih =>
  simp only [succ_nsmul, pow_succ]
  apply val_mul_ge_of_both_ge _ ha ih
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
m : ℕ∞
p : R
nav : SurjVal p
a : R
k : ℕ
ha : m ≤ v nav a
⊢ k • m ≤ v nav (a ^ k)
no goals