FKS2.exp_neg_five_twelfths_mul_le

lemma exp_neg_five_twelfths_mul_le    (t : ℝ) (ht : t ≥ 1000) :    exp (-(5 / 12 : ℝ) * t) ≤ exp (-(230 : ℝ)) * exp (-(1 / 1000 : ℝ) * t) := by  rw [← Real.exp_add]  refine (Real.exp_le_exp).2 ?_  have hcoef_nonneg : 0 ≤ ((5 / 12 : ℝ) - 1 / 1000) := by norm_num  have hmul :      ((5 / 12 : ℝ) - 1 / 1000) * 1000 ≤ ((5 / 12 : ℝ) - 1 / 1000) * t :=    mul_le_mul_of_nonneg_left ht hcoef_nonneg  have h230 : (230 : ℝ) ≤ ((5 / 12 : ℝ) - 1 / 1000) * t := by    have hnum : (230 : ℝ) ≤ ((5 / 12 : ℝ) - 1 / 1000) * 1000 := by norm_num    exact hnum.trans hmul  have hneg : -(((5 / 12 : ℝ) - 1 / 1000) * t) ≤ (-230 : ℝ) := by    exact neg_le_neg h230  calc    (-(5 / 12 : ℝ)) * t        = -(((5 / 12 : ℝ) - 1 / 1000) * t) + (-(1 / 1000 : ℝ) * t) := by          ring_nf    _ ≤ (-230 : ℝ) + (-(1 / 1000 : ℝ) * t) := by        simpa [add_comm, add_left_comm, add_assoc] using          (add_le_add_right hneg (-(1 / 1000 : ℝ) * t))