FKS2.Li_diff_pos_at_6_58

theorem Li_diff_pos_at_6_58 : Li 6.58 - 6.58 / log 6.58 > 0 := by  have hli2 : li 2 ≤ (1.0452 : ℝ) := (li.two_approx).2  have hll : (0.633415 : ℝ) ≤ Real.log (Real.log 6.58) := by linarith [LogTables.log_log_6_58_gt]  have hdiv : 6.58 / Real.log 6.58 ≤ (3.492506 : ℝ) := by    have hlog : (1.884034 : ℝ) ≤ Real.log 6.58 := by linarith [LogTables.log_6_58_gt]    have hlogpos : 0 < Real.log 6.58 := by linarith    rw [div_le_iff₀ hlogpos]    nlinarith  have hli : (4.537729 : ℝ) < li 6.58 := by    rw [li_eq_eulerMascheroni_add_log_log_add_tsum (show (1 : ℝ) < 6.58 by norm_num)]    linarith [hγ_lo, hll, li_series_658_lower]  have hLi : Li 6.58 = li 6.58 - li 2 := by    linarith [li.sub_Li 6.58 (show (2 : ℝ) ≤ 6.58 by norm_num)]  rw [hLi]  linarith