---

Step * 1 1 1 of Lemma decidable__qless


1. a : ℚ
2. b : ℚ
⊢ (qpositive(b - a) ∨bqeq(a;b)) ∧b (¬b(qpositive(-(b - a)) ∨bqeq(b;a))) = qpositive(b - a)
BY
{ xxx(xxxAutoBoolCase ⌜qeq(a;b)⌝⋅xxx THEN xxxAutoBoolCase ⌜qeq(b;a)⌝⋅xxx)xxx }

1
1. a : ℚ
2. b : ℚ
3. a = b ∈ ℚ
4. b = a ∈ ℚ
⊢ (qpositive(b - a) ∨btt) ∧b (¬b(qpositive(-(b - a)) ∨btt)) = qpositive(b - a)

2
1. a : ℚ
2. b : ℚ
3. ¬(b = a ∈ ℚ)
4. ¬(a = b ∈ ℚ)
⊢ (qpositive(b - a) ∨bff) ∧b (¬b(qpositive(-(b - a)) ∨bff)) = qpositive(b - a)

---

Latex:

---

Latex:

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


By

---

Latex:
xxx(xxxAutoBoolCase  \mkleeneopen{}qeq(a;b)\mkleeneclose{}\mcdot{}xxx  THEN  xxxAutoBoolCase  \mkleeneopen{}qeq(b;a)\mkleeneclose{}\mcdot{}xxx)xxx

---

Home Index