---

Step * 1 of Lemma assert-q_less


1. a : ℚ
2. b : ℚ
⊢ ↑(a <b b) ~ a < b
BY
{ (RepUR ``qless grp_lt set_lt`` 0 THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  a  :  \mBbbQ{}
2.  b  :  \mBbbQ{}
\mvdash{}  \muparrow{}(a  <\msubb{}  b)  \msim{}  a  <  b


By

---

Latex:
(RepUR  ``qless  grp\_lt  set\_lt``  0  THEN  Auto)\mcdot{}

---

Home Index