---

Step * 1 of Lemma fact-bound


1. n : ℤ
2. 0 < n
3. (n - 1)! ≤ n - 1^n - 1
⊢ (n * (n - 1)!) ≤ (n * n^n - 1)
BY
{ (InstLemma `mul_preserves_le` [(n - 1)!;n - 1^n - 1;⌜n⌝]⋅ THEN Auto) }

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

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}
2.  0  <  n
3.  (n  -  1)!  \mleq{}  n  -  1\^{}n  -  1
\mvdash{}  (n  *  (n  -  1)!)  \mleq{}  (n  *  n\^{}n  -  1)


By

---

Latex:
(InstLemma  `mul\_preserves\_le`  [(n  -  1)!;n  -  1\^{}n  -  1;\mkleeneopen{}n\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index