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