---

Step * 3 2 of Lemma qdiv-non-neg


1. a : ℚ
2. b : ℚ
3. ¬(b = 0 ∈ ℚ)
4. 0 ≤ (a/b)
5. ¬0 < b
⊢ b < 0
BY
{ xxx((InstLemma `qless_trichot_qorder` [⌜0⌝;⌜b⌝]⋅ THENM SplitOrHyps) THEN Auto)xxx }

---

Latex:

---

Latex:

1.  a  :  \mBbbQ{}
2.  b  :  \mBbbQ{}
3.  \mneg{}(b  =  0)
4.  0  \mleq{}  (a/b)
5.  \mneg{}0  <  b
\mvdash{}  b  <  0


By

---

Latex:
xxx((InstLemma  `qless\_trichot\_qorder`  [\mkleeneopen{}0\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THENM  SplitOrHyps)  THEN  Auto)xxx

---

Home Index