---

Step * of Lemma r2-left-extend

∀a,b,x,y:ℝ^2.  (r2-left(x;a;b) ⇒ rv-T(2;b;x;y) ⇒ r2-left(y;a;b))
BY
{ (Unfold `r2-left` 0
   THEN Auto
   THEN (Assert ⌜|xab| ≤ |yab|⌝⋅ THENM Auto)
   THEN StableCases ⌜b ≠ y⌝⋅
   THEN Try (BLemma `stable__rleq`)
   THEN Auto
   THEN D -2
   THEN Auto
   THEN Try (((FLemma `not-real-vec-sep-iff-eq` [-1]⋅ THENA Auto) THEN RWO "-1" 0 THEN Auto))
   THEN RepeatFor 2 (D -1)
   THEN Reduce -2
   THEN D -2) }

1
1. a : ℝ^2
2. b : ℝ^2
3. x : ℝ^2
4. y : ℝ^2
5. r0 < |xab|
6. (¬b ≠ y) ⇒ (¬x ≠ y)
7. b ≠ y
8. t : ℝ
9. r0 ≤ t
10. t ≤ r1
11. req-vec(2;x;t*b + r1 - t*y)
⊢ |xab| ≤ |yab|

---

Latex:

---

Latex:
\mforall{}a,b,x,y:\mBbbR{}\^{}2.    (r2-left(x;a;b)  {}\mRightarrow{}  rv-T(2;b;x;y)  {}\mRightarrow{}  r2-left(y;a;b))


By

---

Latex:
(Unfold  `r2-left`  0
  THEN  Auto
  THEN  (Assert  \mkleeneopen{}|xab|  \mleq{}  |yab|\mkleeneclose{}\mcdot{}  THENM  Auto)
  THEN  StableCases  \mkleeneopen{}b  \mneq{}  y\mkleeneclose{}\mcdot{}
  THEN  Try  (BLemma  `stable\_\_rleq`)
  THEN  Auto
  THEN  D  -2
  THEN  Auto
  THEN  Try  (((FLemma  `not-real-vec-sep-iff-eq`  [-1]\mcdot{}  THENA  Auto)  THEN  RWO  "-1"  0  THEN  Auto))
  THEN  RepeatFor  2  (D  -1)
  THEN  Reduce  -2
  THEN  D  -2)

---

Home Index