---

Step * 1 of Lemma exp-greater


1. x : {2...}
2. m : ℕ+
⊢ (m + 1) ≤ (x * m)
BY
{ ((NatPlusInd (-1) THEN Auto) THEN D -3 THEN Auto') }

---

Latex:

---

Latex:

1.  x  :  \{2...\}
2.  m  :  \mBbbN{}\msupplus{}
\mvdash{}  (m  +  1)  \mleq{}  (x  *  m)


By

---

Latex:
((NatPlusInd  (-1)  THEN  Auto)  THEN  D  -3  THEN  Auto')

---

Home Index