Theorem: IMOSL.Extra.Infinitesimal.mul_of_abs_le_one_right (IMOSLLean4/Extra/Infinitesimal/Basic.lean)

State before:
R : Type u_1
inst✝ : LinearOrderedRing R
ε r : R
hε : Infinitesimal ε
hr : |r| ≤ 1
k : ℕ
⊢ k • |ε * r| < 1
Tactic:
rw [abs_mul, nsmul_eq_mul, ← mul_assoc, ← nsmul_eq_mul]
State after:
R : Type u_1
inst✝ : LinearOrderedRing R
ε r : R
hε : Infinitesimal ε
hr : |r| ≤ 1
k : ℕ
⊢ k • |ε| * |r| < 1

State before:
R : Type u_1
inst✝ : LinearOrderedRing R
ε r : R
hε : Infinitesimal ε
hr : |r| ≤ 1
k : ℕ
⊢ k • |ε| * |r| < 1
Tactic:
exact mul_lt_one_of_nonneg_of_lt_one_left (nsmul_nonneg (abs_nonneg ε) k) (hε k) hr
State after:
no goals