have hc : 1 < c := by
  rw [← rpow_zero (2 : ℝ)]
  apply Real.rpow_lt_rpow_of_exponent_lt (by norm_num) εpos
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
⊢ (c - 1) / c < c.log
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
ε : ℝ
εpos : 0 < ε
c : ℝ := 2 ^ ε
this : 1 - 1 / c = (c - 1) / c
hc : 1 < c
⊢ (c - 1) / c < c.log