Assumptions:
TeX:
n ! > {C}^{n}
n \in \mathbb{Z}_{\ge 1} \;\mathbin{\operatorname{and}}\; C \in \left(0, \infty\right) \;\mathbin{\operatorname{and}}\; n \ge C eDefinitions:
| Fungrim symbol | Notation | Short description | 
|---|---|---|
| Factorial | Factorial | |
| Pow | Power | |
| ZZGreaterEqual | Integers greater than or equal to n | |
| OpenInterval | Open interval | |
| Infinity | Positive infinity | |
| ConstE | The constant e (2.718...) | 
Source code for this entry:
Entry(ID("25b7bd"),
    Formula(Greater(Factorial(n), Pow(C, n))),
    Variables(C, n),
    Assumptions(And(Element(n, ZZGreaterEqual(1)), Element(C, OpenInterval(0, Infinity)), GreaterEqual(n, Mul(C, ConstE)))))