rw [sub_lt_iff_lt_add, add_comm, ← sub_lt_iff_lt_add]
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
hx : x ≤ 1 - Real.log 2 * ε
εpos : 0 < ε
⊢ 1 - Real.log 2 * ε < 2 ^ (-ε)
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x ε : ℝ
hx : x ≤ 1 - Real.log 2 * ε
εpos : 0 < ε
⊢ 1 - 2 ^ (-ε) < Real.log 2 * ε