log_add_one_sub_log_le

lemma log_add_one_sub_log_le {x : ℝ} (hx : 0 < x) : nabla Real.log x ≤ x⁻¹ := by  have l1 : ContinuousOn Real.log (Icc x (x + 1)) := by    apply continuousOn_log.mono ; intro t ⟨h1, _⟩ ; simp ; linarith  have l2 t (ht : t ∈ Ioo x (x + 1)) : HasDerivAt Real.log t⁻¹ t :=    Real.hasDerivAt_log (by linarith [ht.1])  obtain ⟨t, ⟨ht1, _⟩, htx⟩ := exists_hasDerivAt_eq_slope Real.log (·⁻¹) (by linarith) l1 l2  simp only [add_sub_cancel_left, div_one] at htx  rw [nabla, ← htx, inv_le_inv₀ (by linarith) hx]  exact ht1.le