(x : ℝ) → -9 / 4 ≤ x → Mono fun n : ℝ ↦ (1 + x / n) ^ n
(x : ℝ) → -9 / 4 < x → StrictMono fun n : ℝ ↦ (1 + x / n) ^ n
(maybe Real.tendsto_one_add_div_rpow_exp or its proof can help somehow)
(x n : ℝ) → -9 / 4 ≤ x → (1 + x / n) ^ n ≤ x.exp
(x n : ℝ) → -9 / 4 < x → x ≠ 0 → (1 + x / n) ^ n < x.exp
(these actually hold a bit further than -9/4)
(x : ℝ) → -9 / 4 ≤ x → Mono fun n : ℝ ↦ (1 + x / n) ^ n(x : ℝ) → -9 / 4 < x → StrictMono fun n : ℝ ↦ (1 + x / n) ^ n(maybe
Real.tendsto_one_add_div_rpow_expor its proof can help somehow)(x n : ℝ) → -9 / 4 ≤ x → (1 + x / n) ^ n ≤ x.exp(x n : ℝ) → -9 / 4 < x → x ≠ 0 → (1 + x / n) ^ n < x.exp(these actually hold a bit further than
-9/4)