Let $\exp$ be the D1932: Standard natural real exponential function.
Let $!$ be the D6: Natural number factorial function.
Let $n \in \mathbb{N}$ be a D996: Natural number.

Then

(1)	\begin{equation} \exp (n) \geq \frac{n^n}{n!} \end{equation}
(2)	\begin{equation} \exp (n) = \frac{n^n}{n!} \quad \iff \quad n = 0 \end{equation}