apply (div_lt_iff' εpos).mpr
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
⊢ (1 - 2 ^ (-ε)) / ε < Real.log 2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
⊢ 1 - 2 ^ (-ε) < ε * Real.log 2