---

Step * of Lemma geo-add-length-lt-cancel-for-double

∀e:EuclideanPlane. ∀a,b:{a:Point| O_X_a} .  (a + a < b + b ⇒ a < b)
BY
{ (Auto
   THEN (InstLemma `geo-sep-iff-or-lt` [⌜e⌝;⌜a + a⌝;⌜b + b⌝]⋅ THENA Auto)
   THEN ((RepeatFor 2 (D -1) THENA Auto) THEN Thin (-2))
   THEN (InstLemma `geo-sep-or` [⌜e⌝;⌜a + a⌝;⌜b + b⌝;⌜a + b⌝]⋅ THENA Auto)
   THEN D -1) }

1
1. e : EuclideanPlane
2. a : {a:Point| O_X_a} 
3. b : {a:Point| O_X_a} 
4. a + a < b + b
5. a + a ≠ b + b
6. a + a ≠ a + b
⊢ a < b

2
1. e : EuclideanPlane
2. a : {a:Point| O_X_a} 
3. b : {a:Point| O_X_a} 
4. a + a < b + b
5. a + a ≠ b + b
6. b + b ≠ a + b
⊢ a < b

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a,b:\{a:Point|  O\_X\_a\}  .    (a  +  a  <  b  +  b  {}\mRightarrow{}  a  <  b)


By

---

Latex:
(Auto
  THEN  (InstLemma  `geo-sep-iff-or-lt`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a  +  a\mkleeneclose{};\mkleeneopen{}b  +  b\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  ((RepeatFor  2  (D  -1)  THENA  Auto)  THEN  Thin  (-2))
  THEN  (InstLemma  `geo-sep-or`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a  +  a\mkleeneclose{};\mkleeneopen{}b  +  b\mkleeneclose{};\mkleeneopen{}a  +  b\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  -1)

---

Home Index