---

Step * 1 1 of Lemma decidable__qless

.....equality..... 
1. a : ℚ
2. b : ℚ
⊢ (qpositive(b - a) ∨bqeq(a;b)) ∧b (¬b(qpositive(a - b) ∨bqeq(b;a))) = qpositive(b - a)
BY
{ xxx(xxxSubst' (a - b) = -(b - a) ∈ ℚ 0xxx THENA Auto)xxx }

1
1. a : ℚ
2. b : ℚ
⊢ (qpositive(b - a) ∨bqeq(a;b)) ∧b (¬b(qpositive(-(b - a)) ∨bqeq(b;a))) = qpositive(b - a)

---

Latex:

---

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


By

---

Latex:
xxx(xxxSubst'  (a  -  b)  =  -(b  -  a)  0xxx  THENA  Auto)xxx

---

Home Index