Proposition 2.4 -- the coupon collector's tail bound

For every natural number $n$ with $n \ge 1$ and every real number $c$ with $c > 0$, the theorem asserts the inequality

Here the left-hand side is the bundle's custom quantity couponMissProb n t, defined as the number of functions from a $t$-element type to an $n$-element type that fail to be surjective (i.e. miss at least one of the $n$ values), counted exactly, divided by the real number $n^{t}$ — the fraction of all $n^t$ sequences of $t$ draws from $n$ coupons that do not collect every coupon. The time $t$ is the ceiling of $n \ln n + c\,n$ taken as a natural number: the smallest natural number $\ge n \ln n + c\, n$ (this "natural ceiling" would send a negative argument to $0$, but under the hypotheses $n \ge 1$ and $c > 0$ the argument $n\ln n + c\,n$ is strictly positive, so $t \ge 1$); $\ln$ denotes the natural logarithm. Note the edge behavior packed into the definition: since $n \ge 1$, the denominator $n^t$ is nonzero, so no division-by-zero junk value arises; in the boundary case $n = 1$ every function to a one-element type (with $t \ge 1$ draws) is surjective, so the left side is $0$ and the claim is that $0 \le e^{-c}$. The statement is a non-strict inequality ($\le$, not $<$), it bounds only this single deterministic ratio at the single time $t = \lceil n\ln n + c\,n\rceil$ (no quantification over other times), and it involves no Markov chain, stationarity, or mixing hypotheses — $n$ and $c$ are the only data, constrained only by $1 \le n$ and $0 < c$.