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