---

Step * 1 of Lemma qabs-of-nonneg

.....equality..... 
1. q : ℚ
2. 0 ≤ q
3. ¬0 < q
⊢ q = 0 ∈ ℚ
BY
{ (RWO "qless_complement_qorder" (-1) THEN Auto)⋅ }

---

Latex:

---

Latex:
.....equality..... 
1.  q  :  \mBbbQ{}
2.  0  \mleq{}  q
3.  \mneg{}0  <  q
\mvdash{}  q  =  0


By

---

Latex:
(RWO  "qless\_complement\_qorder"  (-1)  THEN  Auto)\mcdot{}

---

Home Index