---

Step * of Lemma fact-increasing

∀[m:ℕ]. ∀[n:ℕ+].  (n < m ⇒ (n)! < (m)!)
BY
{ (InductionOnNat THEN Auto) }

1
1. m : ℤ
2. 0 < m
3. ∀[n:ℕ+]. (n < m - 1 ⇒ (n)! < (m - 1)!)
4. n : ℕ+
5. n < m@i
⊢ (n)! < (m)!

---

Latex:

---

Latex:
\mforall{}[m:\mBbbN{}].  \mforall{}[n:\mBbbN{}\msupplus{}].    (n  <  m  {}\mRightarrow{}  (n)!  <  (m)!)


By

---

Latex:
(InductionOnNat  THEN  Auto)

---

Home Index