---

Step * 1 1 1 2 of Lemma decidable__qless


1. a : ℚ
2. b : ℚ
3. ¬(b = a ∈ ℚ)
4. ¬(a = b ∈ ℚ)
⊢ (qpositive(b - a) ∨bff) ∧b (¬b(qpositive(-(b - a)) ∨bff)) = qpositive(b - a)
BY
{ (AutoBoolCase ⌜qpositive(b - a)⌝⋅ THEN AutoBoolCase ⌜qpositive(-(b - a))⌝⋅) }

1
1. a : ℚ
2. b : ℚ
3. ¬(b = a ∈ ℚ)
4. ¬(a = b ∈ ℚ)
5. 0 < b - a
6. 0 < -(b - a)
⊢ ff = tt

---

Latex:

---

Latex:

1.  a  :  \mBbbQ{}
2.  b  :  \mBbbQ{}
3.  \mneg{}(b  =  a)
4.  \mneg{}(a  =  b)
\mvdash{}  (qpositive(b  -  a)  \mvee{}\msubb{}ff)  \mwedge{}\msubb{}  (\mneg{}\msubb{}(qpositive(-(b  -  a))  \mvee{}\msubb{}ff))  =  qpositive(b  -  a)


By

---

Latex:
(AutoBoolCase  \mkleeneopen{}qpositive(b  -  a)\mkleeneclose{}\mcdot{}  THEN  AutoBoolCase  \mkleeneopen{}qpositive(-(b  -  a))\mkleeneclose{}\mcdot{})

---

Home Index