---

Step * of Lemma fact-bound

∀n:ℕ. ((n)! ≤ n^n)
BY
{ (InductionOnNat THEN Auto THEN Reduce 0 THEN Auto THEN RWO "exp_step fact_unroll_1" 0 THEN Auto) }

1
1. n : ℤ
2. 0 < n
3. (n - 1)! ≤ n - 1^n - 1
⊢ (n * (n - 1)!) ≤ (n * n^n - 1)

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  ((n)!  \mleq{}  n\^{}n)


By

---

Latex:
(InductionOnNat  THEN  Auto  THEN  Reduce  0  THEN  Auto  THEN  RWO  "exp\_step  fact\_unroll\_1"  0  THEN  Auto)

---

Home Index