---

Step * of Lemma qexp2

∀[q:ℚ]. (q ↑ 2 = (q * q) ∈ ℚ)
BY
{ xxx(Auto THEN (RWO "exp_unroll_q" 0 THEN Auto) THEN Reduce 0 THEN RWO "qexp1" 0 THEN Auto)xxx }

---

Latex:

---

Latex:
\mforall{}[q:\mBbbQ{}].  (q  \muparrow{}  2  =  (q  *  q))


By

---

Latex:
xxx(Auto  THEN  (RWO  "exp\_unroll\_q"  0  THEN  Auto)  THEN  Reduce  0  THEN  RWO  "qexp1"  0  THEN  Auto)xxx

---

Home Index