---

Step * 1 1 of Lemma fact-greater-exp


1. k : ℕ+@i
2. m : ℤ
⊢ ((k - 1)! * 1 * (0 + k)) ≤ ((0 + k) * ((0 + k) - 1)!)
BY
{ (RW IntNormC 0 THEN Auto) }

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}\msupplus{}@i
2.  m  :  \mBbbZ{}
\mvdash{}  ((k  -  1)!  *  1  *  (0  +  k))  \mleq{}  ((0  +  k)  *  ((0  +  k)  -  1)!)


By

---

Latex:
(RW  IntNormC  0  THEN  Auto)

---

Home Index