theorem MathlibNt.SieveTheory.suzuki_lemma14_2_infinite_tail (x : ℝ) (M : ℕ) (hx : 0 ≤ x) : (x ^ M / ↑M.factorial ≤ ∑' (n : ℕ), if M ≤ n then x ^ n / ↑n.factorial else 0) ∧ (∑' (n : ℕ), if M ≤ n then x ^ n / ↑n.factorial else 0) ≤ x ^ M / ↑M.factorial * Real.exp x

Suzuki's Lemma 14.2: bounds for the infinite exponential tail.