---

Step * of Lemma qexp-nonneg

∀[n:ℕ]. ∀[r:ℚ].  0 ≤ r ↑ n supposing 0 ≤ r
BY
{ (InductionOnNat
   THEN Auto
   THEN (RWO "exp_zero_q exp_unroll_q" 0 THENA Auto)
   THEN Reduce 0
   THEN Auto
   THEN InstHyp [⌜r⌝] (-3)⋅
   THEN Auto
   THEN (RWO "-1<" 0 THEN Auto)
   THEN Auto
   THEN QNorm 0) }

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[r:\mBbbQ{}].    0  \mleq{}  r  \muparrow{}  n  supposing  0  \mleq{}  r


By

---

Latex:
(InductionOnNat
  THEN  Auto
  THEN  (RWO  "exp\_zero\_q  exp\_unroll\_q"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  Auto
  THEN  InstHyp  [\mkleeneopen{}r\mkleeneclose{}]  (-3)\mcdot{}
  THEN  Auto
  THEN  (RWO  "-1<"  0  THEN  Auto)
  THEN  Auto
  THEN  QNorm  0)

---

Home Index