---

Step * of Lemma sq_stable__r2-left-or

∀a,b,c:ℝ^2.  SqStable(r2-left(a;b;c) ∨ r2-left(a;c;b))
BY
{ ((Unfold `r2-left` 0 THEN Auto)
   THEN (Assert ⌜SqStable(r0 < ||abc||)⌝⋅ THENA Auto)
   THEN RepeatFor 2 (ParallelLast)
   THEN Try (ParallelLast)) }

---

Latex:

---

Latex:
\mforall{}a,b,c:\mBbbR{}\^{}2.    SqStable(r2-left(a;b;c)  \mvee{}  r2-left(a;c;b))


By

---

Latex:
((Unfold  `r2-left`  0  THEN  Auto)
  THEN  (Assert  \mkleeneopen{}SqStable(r0  <  ||abc||)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  RepeatFor  2  (ParallelLast)
  THEN  Try  (ParallelLast))

---

Home Index