---

Step * of Lemma exp-positive

∀[n,x:ℕ+].  0 < x^n
BY
{ (InductionOnNat THEN Reduce 0 THEN Auto THEN RWO "exp1 exp_step" 0 THEN Auto THEN D 3 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[n,x:\mBbbN{}\msupplus{}].    0  <  x\^{}n


By

---

Latex:
(InductionOnNat  THEN  Reduce  0  THEN  Auto  THEN  RWO  "exp1  exp\_step"  0  THEN  Auto  THEN  D  3  THEN  Auto)

---

Home Index