BKLNW.exp_neg_le_pow

lemma exp_neg_le_pow (n : ℕ) {x : ℝ} (hx : (n : ℝ) ≤ x) : exp (-x) ≤ exp_neg_one_ub ^ n := by  have h1 : exp (-x) ≤ exp (-(n : ℝ)) := by    have : -x ≤ -(n : ℝ) := by linarith    exact (Real.exp_le_exp).2 this  have hbase : exp (-1) ≤ exp_neg_one_ub := by    exact le_of_lt Real.exp_neg_one_lt_d9  have hpos : 0 ≤ exp (-1) := by positivity  have hExp : exp (-(n : ℝ)) = exp (-1) ^ n := by    have hmul : (n : ℝ) * (-1) = -(n : ℝ) := by ring    simpa [hmul] using (Real.exp_nat_mul (-1) n)  calc    exp (-x) ≤ exp (-(n : ℝ)) := h1    _ = exp (-1) ^ n := hExp    _ ≤ exp_neg_one_ub ^ n := by      exact pow_le_pow_left₀ hpos hbase n