---

Step * of Lemma geo-add-length-cancel-left-le

∀[e:BasicGeometry]. ∀[x,y,z:Length].  x ≤ y supposing z + x ≤ z + y
BY
{ ((Auto THEN UseWitness ⌜Ax⌝⋅)
   THEN (DVar `x' THEN DVar `y' THEN DVar `z')
   THEN Fold `member` 0
   THEN MoveToConcl (-1)
   THEN (GenConcl ⌜x = a ∈ {p:Point| O_X_p} ⌝⋅ THENA Auto)
   THEN (GenConcl ⌜y = b ∈ {p:Point| O_X_p} ⌝⋅ THENA Auto)
   THEN (GenConcl ⌜z = c ∈ {p:Point| O_X_p} ⌝⋅ THENA Auto)
   THEN All Thin
   THEN Auto
   THEN DSetVars) }

1
1. e : BasicGeometry
2. a : Point
3. O_X_a
4. b : Point
5. O_X_b
6. c : Point
7. O_X_c
8. c + a ≤ c + b
⊢ Ax ∈ a ≤ b

---

Latex:

---

Latex:
\mforall{}[e:BasicGeometry].  \mforall{}[x,y,z:Length].    x  \mleq{}  y  supposing  z  +  x  \mleq{}  z  +  y


By

---

Latex:
((Auto  THEN  UseWitness  \mkleeneopen{}Ax\mkleeneclose{}\mcdot{})
  THEN  (DVar  `x'  THEN  DVar  `y'  THEN  DVar  `z')
  THEN  Fold  `member`  0
  THEN  MoveToConcl  (-1)
  THEN  (GenConcl  \mkleeneopen{}x  =  a\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (GenConcl  \mkleeneopen{}y  =  b\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (GenConcl  \mkleeneopen{}z  =  c\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  All  Thin
  THEN  Auto
  THEN  DSetVars)

---

Home Index