---

Step * of Lemma qexp-positive

∀[n:ℕ]. ∀[r:ℚ].  0 < r ↑ n supposing 0 < r
BY
{ (InductionOnNat
   THEN Auto
   THEN (RWO "qexp-zero exp_unroll_q" 0 THENA Auto)
   THEN Reduce 0
   THEN Auto
   THEN BLemma `qmul-positive`
   THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(InductionOnNat
  THEN  Auto
  THEN  (RWO  "qexp-zero  exp\_unroll\_q"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  Auto
  THEN  BLemma  `qmul-positive`
  THEN  Auto)

---

Home Index