---

Step * of Lemma qexp_step

∀[n:ℕ]. ∀[e:ℚ].  (e ↑ n + 1 = (e ↑ n * e) ∈ ℚ)
BY
{ xxx(Auto THEN RW (AddrC [2] (LemmaC `exp_unroll_q`)) 0 THEN Auto)xxx }

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[e:\mBbbQ{}].    (e  \muparrow{}  n  +  1  =  (e  \muparrow{}  n  *  e))


By

---

Latex:
xxx(Auto  THEN  RW  (AddrC  [2]  (LemmaC  `exp\_unroll\_q`))  0  THEN  Auto)xxx

---

Home Index