---

Step * of Lemma qless_irreflexivity_qorder

No Annotations
∀[a:ℚ]. False supposing a < a
BY
{ ((ProveSpecializedLemmaWReduce grp_lt_irreflexivity) 0 [⌜parm{i}⌝;⌜<ℚ+>⌝]⋅ THEN Fold `qless` 1 THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[a:\mBbbQ{}].  False  supposing  a  <  a


By

---

Latex:
((ProveSpecializedLemmaWReduce  grp\_lt\_irreflexivity)  0  [\mkleeneopen{}parm\{i\}\mkleeneclose{};\mkleeneopen{}<\mBbbQ{}+>\mkleeneclose{}]\mcdot{}
  THEN  Fold  `qless`  1
  THEN  Auto)

---

Home Index