---

Step * of Lemma qless_is_sp_of_leq_a_qorder

No Annotations
∀[a,b:ℚ].  uiff(a < b;(a ≤ b) ∧ (¬(b ≤ a)))
BY
{ ((ProveSpecializedLemmaWReduce grp_lt_is_sp_of_leq_a) 0 [⌜parm{i}⌝;⌜<ℚ+>⌝]⋅ THEN Folds ``qless qle`` (-1) THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[a,b:\mBbbQ{}].    uiff(a  <  b;(a  \mleq{}  b)  \mwedge{}  (\mneg{}(b  \mleq{}  a)))


By

---

Latex:
((ProveSpecializedLemmaWReduce  grp\_lt\_is\_sp\_of\_leq\_a)  0  [\mkleeneopen{}parm\{i\}\mkleeneclose{};\mkleeneopen{}<\mBbbQ{}+>\mkleeneclose{}]\mcdot{}
  THEN  Folds  ``qless  qle``  (-1)
  THEN  Auto)

---

Home Index