---

Step * of Lemma assert-q_less

∀[a,b:ℚ].  (↑q_less(a;b) ~ a < b)
BY
{ (Auto THEN Unfold `q_less` 0 THEN (RWO "rational_set_blt<" 0 THENA Auto)) }

1
1. a : ℚ
2. b : ℚ
⊢ ↑(a <b b) ~ a < b

---

Latex:

---

Latex:
\mforall{}[a,b:\mBbbQ{}].    (\muparrow{}q\_less(a;b)  \msim{}  a  <  b)


By

---

Latex:
(Auto  THEN  Unfold  `q\_less`  0  THEN  (RWO  "rational\_set\_blt<"  0  THENA  Auto))

---

Home Index