---

Step * of Lemma eu-add-length-cancel-left

∀[e:EuclideanPlane]. ∀[x,y,z:{p:Point| O_X_p} ].  x = y ∈ {p:Point| O_X_p}  supposing z + x = z + y ∈ {p:Point| O_X_p} 
BY
{ (Auto
   THEN DSetVars
   THEN MoveToConcl (-1)
   THEN RepUR ``eu-add-length`` 0
   THEN (Assert ¬(O = X ∈ Point) BY
               Auto)
   THEN (Assert ¬(O = z ∈ Point) BY
               (NotEqualFromEuBetween⋅ THEN Auto))
   THEN GeneralizeEuExtends [`a';`b']) }

1
1. e : EuclideanPlane
2. x : Point
3. O_X_x
4. y : Point
5. O_X_y
6. z : Point
7. O_X_z
8. ¬(O = X ∈ Point)
9. ¬(O = z ∈ Point)
10. a : Point@i
11. O_z_a ∧ za=Xx@i
12. b : Point@i
13. O_z_b ∧ zb=Xy@i
⊢ (a = b ∈ {p:Point| O_X_p} ) ⇒ (x = y ∈ {p:Point| O_X_p} )

---

Latex:

---

Latex:
\mforall{}[e:EuclideanPlane].  \mforall{}[x,y,z:\{p:Point|  O\_X\_p\}  ].    x  =  y  supposing  z  +  x  =  z  +  y


By

---

Latex:
(Auto
  THEN  DSetVars
  THEN  MoveToConcl  (-1)
  THEN  RepUR  ``eu-add-length``  0
  THEN  (Assert  \mneg{}(O  =  X)  BY
                          Auto)
  THEN  (Assert  \mneg{}(O  =  z)  BY
                          (NotEqualFromEuBetween\mcdot{}  THEN  Auto))
  THEN  GeneralizeEuExtends  [`a';`b'])

---

Home Index