---

Step * of Lemma qbetween-qdist

∀[a,b,r,s:ℚ].  (qdist(a;b) ≤ (s - r)) supposing (r ≤ b ≤ s and r ≤ a ≤ s)
BY
{ (Unfolds ``qbetween qdist`` 0
   THEN Auto
   THEN xxx((Unfold `qabs` 0 THEN (CallByValueReduce 0 THENA Auto))
            THEN (RWO "qminus-qsub" 0 THENA Auto)
            THEN (SplitOnConclITE THENA Auto)
            THEN (Thin (-1))
            THEN xxx((All (RWO "qle-normalize")) THEN Auto)xxx)xxx) }

1
1. a : ℚ
2. b : ℚ
3. r : ℚ
4. s : ℚ
5. 0 ≤ (a - r)
6. 0 ≤ (s - a)
7. 0 ≤ (b - r)
8. 0 ≤ (s - b)
⊢ 0 ≤ (s - r - a - b)

2
1. a : ℚ
2. b : ℚ
3. r : ℚ
4. s : ℚ
5. 0 ≤ (a - r)
6. 0 ≤ (s - a)
7. 0 ≤ (b - r)
8. 0 ≤ (s - b)
⊢ 0 ≤ (s - r - b - a)

---

Latex:

---

Latex:
\mforall{}[a,b,r,s:\mBbbQ{}].    (qdist(a;b)  \mleq{}  (s  -  r))  supposing  (r  \mleq{}  b  \mleq{}  s  and  r  \mleq{}  a  \mleq{}  s)


By

---

Latex:
(Unfolds  ``qbetween  qdist``  0
  THEN  Auto
  THEN  xxx((Unfold  `qabs`  0  THEN  (CallByValueReduce  0  THENA  Auto))
                    THEN  (RWO  "qminus-qsub"  0  THENA  Auto)
                    THEN  (SplitOnConclITE  THENA  Auto)
                    THEN  (Thin  (-1))
                    THEN  xxx((All  (RWO  "qle-normalize"))  THEN  Auto)xxx)xxx)

---

Home Index