Comment: Beeson's Constructive Tarski Geometry
Tarski and his students (Szemeilew, Gupta) gave a
first order axiomatic theory for Euclidean plane geometry
that had only Points as elements and two relations.
 ternary "betweeness" relation and quaternary "congruence" relation
  (which defines binary "same length" relation on segments).

They made the system minimal, so that the axioms were all independent
and none of them could be derived from the others (using classical logic).

Beeson has given constructive, intuitionistic logic, version of Tarski's
system -- which we formalize here in Nuprl. We use constructive
logic and do not assume that equality of Points is decidable.
Therefore, theorem stating that for
all points and satisfying some constraints P(A,B)
there exists point satisfying constraints Q(A,B,C)
may not be proved by cases where if A=B then is constructed one way
and if not(A=B) then is constructed another way.

Because of this, Beeson must add few axioms that
were derivable (using classical logic) in Tarski's system.
Also, to make all of the constructions continuous functions of their input
points, two of the axioms (the "extend" axiom and the "inner Pasch" axiom)
that construct new points are restricted to non-degenerate cases
(only segments with distinct endpoints can be extended, and
 the "inner Pasch" requires non-colinear triangle and strict betweenness).

Finally, Beeson's axioms assume that the betweenness relation and the congruence
relation are "stable" propositions about points (a proposition is stable
if (¬¬P)  ).

The formal definition of EuclideanPlane has the form 
{e:EuclideanStructure| euclidean-axioms(e)} -- follow those links (right click) for
further documentation.   ⋅

Definition: euclidean-structure
dependent record type defines the basic types and operations
of Beeson's constructive version of Tarski's geometry.
The first "field" of the record is the type "Point" and the types
of the other fields depend on ⌜self."Point"⌝.

"E" is the congruence relation ⌜ab=cd⌝ and "B" is the strict betweeness
relation ⌜a-b-c⌝"T" is the non-strict betweeness relation ⌜a_b_c⌝
but it is really defined concept because the "Tdef" field forces 
a_b_c ⇐⇒ ¬((¬(a b ∈ self."Point")) ∧ (c b ∈ self."Point")) ∧ a-b-c))⌝.

Simlarly, ⌜Colinear(a;b;c)⌝ is introduced via "colinear" and defined
by "colineardef". These definitions are in the dependent record because
they are needed to give the constrained types for the 
"extend", "inner-Pasch", "line-circle" and "middle" operators.

The fields "Estable" and "Bstable" force the congruence and betweeness
propositions to be stable (see Stable{P},  it says ⌜(¬¬P)  P⌝ ).⋅

EuclideanStructure ==
  "Point":Type
  "E":self."Point" ⟶ self."Point" ⟶ self."Point" ⟶ self."Point" ⟶ ℙ
  "B":self."Point" ⟶ self."Point" ⟶ self."Point" ⟶ ℙ
  "T":self."Point" ⟶ self."Point" ⟶ self."Point" ⟶ ℙ
  "colinear":self."Point" ⟶ self."Point" ⟶ self."Point" ⟶ ℙ
  "nontrivial":{trip:self."Point" × self."Point" × self."Point"| 
                let a,b,c trip in 
                (a b ∈ self."Point")) ∧ (self."colinear" c))} 
  "Tdef":∀[a,b,c:self."Point"].
           (self."T" ⇐⇒ ¬((¬(a b ∈ self."Point")) ∧ (c b ∈ self."Point")) ∧ (self."B" c))))
  "colineardef":∀[a,b,c:self."Point"].
                  (self."colinear" c
                  ⇐⇒ (a b ∈ self."Point"))
                      ∧ ((¬(c a ∈ self."Point"))
                        ∧ (c b ∈ self."Point"))
                        ∧ (self."B" b))
                        ∧ (self."B" b))
                        ∧ (self."B" c)))))
  "Estable":∀[a,b,c,d:self."Point"].  self."E" supposing ¬¬(self."E" d)
  "Bstable":∀[a,b,c:self."Point"].  self."B" supposing ¬¬(self."B" c)
  "extend":a:self."Point" ⟶ {b:self."Point"| ¬(a b ∈ self."Point")}  ⟶ self."Point" ⟶ self."Point" ⟶ self."Point"
  "inner-Pasch":a:self."Point"
  ⟶ b:self."Point"
  ⟶ c:{c:self."Point"| ¬(self."colinear" c)} 
  ⟶ {p:self."Point"| self."B" c} 
  ⟶ {q:self."Point"| self."T" c} 
  ⟶ self."Point"
  "line-circle":a:self."Point"
  ⟶ b:self."Point"
  ⟶ x:{x:self."Point"| self."T" b} 
  ⟶ y:{y:self."Point"| self."T" y} 
  ⟶ p:{p:self."Point"| self."E" x} 
  ⟶ {q:self."Point"| (self."E" y) ∧ (q p ∈ self."Point"))} 
  ⟶ (self."Point" × self."Point")
  "middle":a:self."Point" ⟶ b:self."Point" ⟶ c:{c:self."Point"| ¬(self."colinear" c)}  ⟶ self."Point"

Lemma: euclidean-structure_wf
EuclideanStructure ∈ 𝕌'

Definition: eu-point
Point ==  e."Point"

Lemma: eu-point_wf
[e:EuclideanStructure]. (Point ∈ Type)

Definition: eu-congruent
ab=cd ==  e."E" d

Lemma: eu-congruent_wf
[e:EuclideanStructure]. ∀[a,b,c,d:Point].  (ab=cd ∈ ℙ)

Lemma: stable__eu-congruent
e:EuclideanStructure. ∀[a,b,c,d:Point].  Stable{ab=cd}

Lemma: sq_stable__eu-congruent
e:EuclideanStructure. ∀[a,b,c,d:Point].  SqStable(ab=cd)

Definition: eu-between
a-b-c ==  e."B" c

Lemma: eu-between_wf
[e:EuclideanStructure]. ∀[a,b,c:Point].  (a-b-c ∈ ℙ)

Lemma: stable__eu-between
e:EuclideanStructure. ∀[a,b,c:Point].  Stable{a-b-c}

Lemma: sq_stable__eu-between
e:EuclideanStructure. ∀[a,b,c:Point].  SqStable(a-b-c)

Definition: eu-colinear
Colinear(a;b;c) ==  e."colinear" c

Lemma: eu-colinear_wf
[e:EuclideanStructure]. ∀[a,b,c:Point].  (Colinear(a;b;c) ∈ ℙ)

Definition: eu-nontrivial
eu-nontrivial(e) ==  e."nontrivial"

Lemma: eu-nontrivial_wf
[e:EuclideanStructure]
  (eu-nontrivial(e) ∈ {triple:Point × Point × Point| let a,b,c triple in (a b ∈ Point)) ∧ Colinear(a;b;c))} )

Definition: eu-O
==  fst(eu-nontrivial(e))

Lemma: eu-O_wf
e:EuclideanStructure. (O ∈ Point)

Definition: eu-X
==  fst(snd(eu-nontrivial(e)))

Lemma: eu-X_wf
e:EuclideanStructure. (X ∈ Point)

Definition: eu-Y
==  snd(snd(eu-nontrivial(e)))

Lemma: eu-Y_wf
[e:EuclideanStructure]. (Y ∈ Point)

Lemma: eu-colinear-def
e:EuclideanStructure
  ∀[a,b,c:Point].
    (Colinear(a;b;c)
    ⇐⇒ (a b ∈ Point)) ∧ ((¬(c a ∈ Point)) ∧ (c b ∈ Point)) ∧ c-a-b) ∧ a-c-b) ∧ a-b-c))))

Lemma: stable__colinear
e:EuclideanStructure. ∀[a,b,c:Point].  Stable{Colinear(a;b;c)}

Lemma: sq_stable__colinear
e:EuclideanStructure. ∀[a,b,c:Point].  SqStable(Colinear(a;b;c))

Lemma: eu-not-not-colinear
e:EuclideanStructure
  ∀[a,b,c:Point].
    (¬¬Colinear(a;b;c) ⇐⇒ (a b ∈ Point)) ∧ (¬¬((c a ∈ Point) ∨ (c b ∈ Point) ∨ c-a-b ∨ a-c-b ∨ a-b-c)))

Lemma: eu-not-colinear-OXY
[e:EuclideanStructure]. ((¬(O X ∈ Point)) ∧ Colinear(O;X;Y)))

Lemma: eu-not-equal-OXY
[e:EuclideanStructure]. ((¬(O X ∈ Point)) ∧ (O Y ∈ Point)) ∧ (X Y ∈ Point)))

Definition: eu-between-eq
a_b_c ==  e."T" c

Lemma: eu-between-eq_wf
[e:EuclideanStructure]. ∀[a,b,c:Point].  (a_b_c ∈ ℙ)

Lemma: eu-between-eq-def
e:EuclideanStructure. ∀[a,b,c:Point].  (a_b_c ⇐⇒ ¬((¬(a b ∈ Point)) ∧ (c b ∈ Point)) ∧ a-b-c)))

Lemma: stable__eu-between-eq
e:EuclideanStructure. ∀[a,b,c:Point].  Stable{a_b_c}

Lemma: sq_stable__eu-between-eq
e:EuclideanStructure. ∀[a,b,c:Point].  SqStable(a_b_c)

Lemma: eu-between-eq-implies-colinear
e:EuclideanStructure. ∀[a,b,c:Point].  (Colinear(a;b;c)) supposing (a_b_c and (a b ∈ Point)))

Lemma: eu-between-implies-colinear
e:EuclideanStructure. ∀[a,b,c:Point].  (Colinear(a;b;c)) supposing (a-b-c and (a b ∈ Point)))

Lemma: eu-between-eq-implies-colinear2
e:EuclideanStructure. ∀[a,b,c:Point].  (Colinear(a;b;c)) supposing (c_a_b and (a b ∈ Point)))

Definition: eu-extend
(extend ab by cd) ==  e."extend" d

Lemma: eu-extend_wf
[e:EuclideanStructure]. ∀[a:Point]. ∀[b:{b:Point| ¬(a b ∈ Point)} ]. ∀[c,d:Point].  ((extend ab by cd) ∈ Point)

Definition: eu-inner-pasch
eu-inner-pasch(e;a;b;c;p;q) ==  e."inner-Pasch" q

Lemma: eu-inner-pasch_wf
[e:EuclideanStructure]. ∀[a,b:Point]. ∀[c:{c:Point| ¬Colinear(a;b;c)} ]. ∀[p:{p:Point| a-p-c} ]. ∀[q:{q:Point| b_q_c} ]\000C.
  (eu-inner-pasch(e;a;b;c;p;q) ∈ Point)

Definition: eu-line-circle
intersect xy  with Oab  ==  e."line-circle" q

Lemma: eu-line-circle_wf
[e:EuclideanStructure]. ∀[a,b:Point]. ∀[x:{x:Point| a_x_b} ]. ∀[y:{y:Point| a_b_y} ]. ∀[p:{p:Point| ap=ax} ].
[q:{q:Point| aq=ay ∧ (q p ∈ Point))} ].
  (intersect xy  with Oab  ∈ Point × Point)

Definition: eu-middle
middle(a;b;c) ==  e."middle" c

Lemma: eu-middle_wf
[e:EuclideanStructure]. ∀[a,b:Point]. ∀[c:{c:Point| ¬Colinear(a;b;c)} ].  (middle(a;b;c) ∈ Point)

Definition: euclidean-axioms
Twelve axioms about EuclideanStructure 
give Beeson's constructive version of Tarski's axioms.
They are reflexivity, transitivity, and identity of congruence;
"segment extension"; the "five-segment axiom"; "trivial strict betweeness";
the "inner-Pasch" axiom; the "upper-dimension" axiom;
the "triangle circumscription axiom" (equivalent to the parallel postulate);
the "line-circle continuity axiom";  symmetry and "inner transitivity" of
betweeness.⋅

euclidean-axioms(e) ==
  (∀[a,b:Point].  ab=ba)
  ∧ (∀[a,b,p,q,r,s:Point].  (pq=rs) supposing (ab=rs and ab=pq))
  ∧ (∀[a,b,c:Point].  b ∈ Point supposing ab=cc)
  ∧ (∀[q:Point]. ∀[a:{a:Point| ¬(q a ∈ Point)} ]. ∀[b,c:Point].  (q_a_(extend qa by bc) ∧ a(extend qa by bc)=bc))
  ∧ (∀[a,b,c,d,A,B,C,D:Point].
       (cd=CD) supposing (bd=BD and ad=AD and bc=BC and ab=AB and A_B_C and a_b_c and (a b ∈ Point))))
  ∧ (∀[a,b:Point].  a-b-a))
  ∧ (∀[a,b:Point]. ∀[c:{c:Point| ¬Colinear(a;b;c)} ]. ∀[p:{p:Point| a-p-c} ]. ∀[q:{q:Point| b_q_c} ].
       let eu-inner-pasch(e;a;b;c;p;q) in
           p-x-b ∧ q-x-a)
  ∧ (∀[a,b,p,q,r:Point].  (Colinear(p;q;r)) supposing (ra=rb and qa=qb and pa=pb and (a b ∈ Point))))
  ∧ (∀[a,b:Point]. ∀[c:{c:Point| ¬Colinear(a;b;c)} ].  let middle(a;b;c) in ax=bx ∧ ax=cx)
  ∧ (∀[a,b:Point]. ∀[x:{x:Point| a_x_b} ]. ∀[y:{y:Point| a_b_y} ]. ∀[p:{p:Point| ap=ax} ]. ∀[q:{q:Point| 
                                                                                             aq=ay
                                                                                             ∧ (q p ∈ Point))} ].
       let uv intersect xy  with Oab  in
           afst(uv)=ab
           ∧ asnd(uv)=ab
           ∧ p_fst(uv)_q
           ∧ snd(uv)_p_q
           ∧ ¬((fst(uv)) (snd(uv)) ∈ Point) supposing ¬(x b ∈ Point))
  ∧ (∀[a,b,c:Point].  c-b-a supposing a-b-c)
  ∧ (∀[a,b,c,d:Point].  (a-b-c) supposing (b-c-d and a-b-d))

Lemma: euclidean-axioms_wf
[e:EuclideanStructure]. (euclidean-axioms(e) ∈ ℙ)

Lemma: sq_stable_euclidean-axioms
e:EuclideanStructure. SqStable(euclidean-axioms(e))

Definition: euclidean-plane
Beeson's axioms for constructive geometry.
The EuclideanStructure includes the basic types and
four operations with constructive content.
The four basic constructions are
1) extending segment, 
2) intersecting lines,
3) intersecting line and circle, 
4) circumscribing triangle. 

The euclidean-axioms(e)
are constraints on the euclidean structures that have no constructive
content -- they assert the congruence and betweeness properties of the
four basic constructions.


EuclideanPlane ==  {e:EuclideanStructure| euclidean-axioms(e)} 

Lemma: euclidean-plane_wf
EuclideanPlane ∈ 𝕌'

Lemma: eu-extend-property
e:EuclideanPlane
  ∀[q:Point]. ∀[a:{a:Point| ¬(q a ∈ Point)} ]. ∀[b,c:Point].  (q_a_(extend qa by bc) ∧ a(extend qa by bc)=bc)

Lemma: eu-inner-pasch-property
e:EuclideanPlane
  ∀[a,b:Point]. ∀[c:{c:Point| ¬Colinear(a;b;c)} ]. ∀[p:{p:Point| a-p-c} ]. ∀[q:{q:Point| b_q_c} ].
    (p-eu-inner-pasch(e;a;b;c;p;q)-b ∧ q-eu-inner-pasch(e;a;b;c;p;q)-a)

Lemma: eu-segments-cross
e:EuclideanPlane. ∀p,b,q,a:Point.  ((∃c:Point. ((¬Colinear(a;b;c)) ∧ a-p-c ∧ b_q_c))  (∃x:Point. (p-x-b ∧ q-x-a)))

Lemma: eu-extend-exists
e:EuclideanPlane. ∀q:Point. ∀a:{a:Point| ¬(q a ∈ Point)} . ∀b,c:Point.  ∃x:Point. (q_a_x ∧ ax=bc)

Lemma: eu-between-trans
e:EuclideanPlane. ∀[a,b,c,d:Point].  (a-b-c) supposing (b-c-d and a-b-d)

Lemma: eu-between-sym
e:EuclideanPlane. ∀[a,b,c:Point].  a-b-c supposing c-b-a

Lemma: eu-between-trans2
e:EuclideanPlane. ∀[a,b,c,d:Point].  (a-b-c) supposing (d-b-c and d-a-b)

Lemma: eu-between-implies-between-eq
e:EuclideanPlane. ∀[a,b,c:Point].  a_b_c supposing a-b-c

Lemma: eu-between-eq-implies-colinear3
e:EuclideanPlane. ∀[a,b,c:Point].  (Colinear(a;b;c)) supposing (b_c_a and (a b ∈ Point)))

Lemma: eu-congruence-identity
[e:EuclideanPlane]. ∀[a,b,c:Point].  b ∈ Point supposing ab=cc

Lemma: eu-congruence-identity2
[e:EuclideanPlane]. ∀[a,b,c,d:Point].  (a b ∈ Point) supposing (ab=cd and (c d ∈ Point))

Lemma: stable_point-eq
[e:EuclideanPlane]. ∀[p,q:Point].  Stable{p q ∈ Point}

Lemma: euclidean-point-eq
[e:EuclideanPlane]. ∀[p,q:Point].  q ∈ Point supposing ¬¬(p q ∈ Point)

Lemma: eu-between-same
[e:EuclideanPlane]. ∀[a,b:Point].  a-b-a)

Lemma: eu-between-same2
[e:EuclideanPlane]. ∀[a,b:Point].  False supposing a-b-a

Lemma: not-eu-between-same
e:EuclideanPlane. ∀[a,b:Point].  False supposing a-b-b

Lemma: not-eu-between-same2
e:EuclideanPlane. ∀[a,b:Point].  False supposing a-a-b

Lemma: eu-between-eq-same
[e:EuclideanPlane]. ∀[a,b:Point].  b ∈ Point supposing a_b_a

Lemma: eu-between-eq-same2
[e:EuclideanPlane]. ∀[a,b,c:Point].  (a b ∈ Point) supposing ((a c ∈ Point) and a_b_c)

Lemma: stable_eu-between-eq
e:EuclideanPlane. ∀[a,b,c:Point].  Stable{a_b_c}

Lemma: eu-between-eq-trivial-left
e:EuclideanPlane. ∀[a,b:Point].  a_a_b

Lemma: eu-between-eq-trivial-right
e:EuclideanPlane. ∀[a,b:Point].  a_b_b

Lemma: eu-between-eq-symmetry
e:EuclideanPlane. ∀[a,b,c:Point].  c_b_a supposing a_b_c

Lemma: eu-between-eq-inner-trans
e:EuclideanPlane. ∀[a,b,c,d:Point].  (a_b_c) supposing (b_c_d and a_b_d)

Lemma: eu-between-eq-exchange3
e:EuclideanPlane. ∀[a,b,c,d:Point].  (b_c_d) supposing (a_c_d and a_b_c)

Lemma: eu-congruent-refl
e:EuclideanPlane. ∀[a,b:Point].  ab=ab

Lemma: eu-congruent-flip
e:EuclideanPlane. ∀[a,b:Point].  ab=ba

Lemma: eu-congruent-symmetry
e:EuclideanPlane. ∀[a,b,c,d:Point].  cd=ab supposing ab=cd

Lemma: eu-congruent-transitivity
e:EuclideanPlane. ∀[a,b,c,d,x,y:Point].  (ab=xy) supposing (cd=xy and ab=cd)

Lemma: eu-congruent-left-comm
e:EuclideanPlane. ∀[a,b,c,d:Point].  ba=cd supposing ab=cd

Lemma: eu-congruent-right-comm
e:EuclideanPlane. ∀[a,b,c,d:Point].  ab=dc supposing ab=cd

Lemma: eu-congruent-comm
e:EuclideanPlane. ∀[a,b,c,d:Point].  ba=dc supposing ab=cd

Lemma: eu-congruent-trivial
e:EuclideanPlane. ∀[a,b:Point].  aa=bb

Lemma: eu-congruence-identity-sym
[e:EuclideanPlane]. ∀[a,b,c:Point].  b ∈ Point supposing cc=ab

Lemma: eu-congruence-identity3
[e:EuclideanPlane]. ∀[a,b,c,d:Point].  (a b ∈ Point) supposing (cd=ab and (c d ∈ Point))

Lemma: eu-five-segment
e:EuclideanPlane
  ∀[a,b,c,d,A,B,C,D:Point].
    (cd=CD) supposing (bd=BD and ad=AD and bc=BC and ab=AB and A_B_C and a_b_c and (a b ∈ Point)))

Lemma: eu-five-segment'
e:EuclideanPlane
  ∀[a,b,c,A,B,C:Point].
    (∀d,D:Point.  (cd=CD) supposing (bd=BD and ad=AD)) supposing 
       (bc=BC and 
       ab=AB and 
       A_B_C and 
       a_b_c and 
       (a b ∈ Point)))

Lemma: eu-three-segment
e:EuclideanPlane. ∀[a,b,c,A,B,C:Point].  (ac=AC) supposing (bc=BC and ab=AB and A_B_C and a_b_c and (a b ∈ Point)))

Lemma: eu-construction-unicity
e:EuclideanPlane. ∀[Q,A,X,Y:Point].  (X Y ∈ Point) supposing (AY=AX and Q_A_X and Q_A_Y and (Q A ∈ Point)))

Lemma: eu-extend-equal-iff-congruent
e:EuclideanPlane
  ∀[a,b,c,d,c',d':Point].  uiff((extend ab by cd) (extend ab by c'd') ∈ Point;cd=c'd') supposing ¬(a b ∈ Point)

Lemma: eu-between-eq-outer-trans
e:EuclideanPlane. ∀[a,b,c,d:Point].  (a_c_d) supposing (b_c_d and a_b_c and (b c ∈ Point)))

Lemma: eu-between-eq-exchange4
e:EuclideanPlane. ∀[a,b,c,d:Point].  (a_b_d) supposing (a_c_d and a_b_c)

Lemma: eu-exists-middle
e:EuclideanPlane. ∀a,b:Point. ∀c:{p:Point| ¬Colinear(a;b;p)} .  ∃m:Point. ((m middle(a;b;c) ∈ Point) ∧ am=bm ∧ am=cm)

Lemma: eu-colinear-cases
e:EuclideanStructure
  ∀[a,b,c:Point].
    ∀X:ℙ
      (Stable{X}
       (((¬(a b ∈ Point)) ∧ (c a ∈ Point))  X)
       (((¬(a b ∈ Point)) ∧ (c b ∈ Point))  X)
       (((¬(a b ∈ Point)) ∧ c-a-b)  X)
       (((¬(a b ∈ Point)) ∧ a-c-b)  X)
       (((¬(a b ∈ Point)) ∧ a-b-c)  X)
       ((¬Colinear(a;b;c))  X)
       X)

Lemma: eu-colinear-implies-1
e:EuclideanPlane. ∀x,a,b:Point.  (Colinear(b;a;x)  Colinear(b;a;a))

Lemma: eu-colinear-permute
e:EuclideanPlane. ∀a,b,c:Point.  ((¬(c b ∈ Point))  Colinear(a;b;c)  Colinear(c;b;a))

Lemma: eu-colinear-cycle
e:EuclideanPlane. ∀a,b,c:Point.  ((¬(c a ∈ Point))  Colinear(a;b;c)  Colinear(c;a;b))

Lemma: eu-colinear-swap
e:EuclideanPlane. ∀a,b,c:Point.  (Colinear(a;b;c)  Colinear(b;a;c))

Lemma: not-not-inner-pasch
e:EuclideanPlane. ∀a,b,c:Point. ∀p:{p:Point| a_p_c} . ∀q:{q:Point| b_q_c} .  (¬¬(∃x:Point. (p_x_b ∧ q_x_a)))

Definition: eu-segment
Segment ==  Point × Point

Lemma: eu-segment_wf
[e:EuclideanStructure]. (Segment ∈ Type)

Definition: eu-mk-seg
ab ==  <a, b>

Lemma: eu-mk-seg_wf
[e:EuclideanStructure]. ∀[a,b:Point].  (ab ∈ Segment)

Definition: eu-seg1
s.1 ==  fst(s)

Lemma: eu-seg1_wf
[e:EuclideanStructure]. ∀[s:Segment].  (s.1 ∈ Point)

Definition: eu-seg2
s.2 ==  snd(s)

Lemma: eu-seg2_wf
[e:EuclideanStructure]. ∀[s:Segment].  (s.2 ∈ Point)

Lemma: eu_seg1_mk_seg_lemma
b,a:Top.  (ab.1 a)

Lemma: eu_seg2_mk_seg_lemma
b,a:Top.  (ab.2 b)

Definition: eu-seg-proper
proper(s) ==  ¬(s.1 s.2 ∈ Point)

Lemma: eu-seg-proper_wf
[e:EuclideanStructure]. ∀[s:Segment].  (proper(s) ∈ ℙ)

Definition: eu-proper-segment
ProperSegment ==  {s:Segment| proper(s)} 

Lemma: eu-proper-segment_wf
[e:EuclideanStructure]. (ProperSegment ∈ Type)

Definition: eu-seg-congruent
s1 ≡ s2 ==  s1.1s1.2=s2.1s2.2

Lemma: eu-seg-congruent_wf
[e:EuclideanStructure]. ∀[s1,s2:Segment].  (s1 ≡ s2 ∈ ℙ)

Lemma: sq_stable_eu-seg-congruent
e:EuclideanStructure. ∀[s1,s2:Segment].  SqStable(s1 ≡ s2)

Lemma: eu-seg-congruent_transitivity
e:EuclideanPlane. ∀[s1,s2,s3:Segment].  (s1 ≡ s3) supposing (s1 ≡ s2 and s2 ≡ s3)

Lemma: eu-seg-congruent_symmetry
e:EuclideanPlane. ∀[s1,s2:Segment].  s2 ≡ s1 supposing s1 ≡ s2

Lemma: eu-seg-congruent_weakening
e:EuclideanPlane. ∀[s1,s2:Segment].  s1 ≡ s2 supposing s1 s2 ∈ Segment

Lemma: eu-seg-congruent-equiv
e:EuclideanPlane. EquivRel(Segment;s,t.s ≡ t)

Lemma: eu-seg-congruent-equiv-proper
e:EuclideanPlane. EquivRel(ProperSegment;s,t.s ≡ t)

Definition: eu-seg-extend
==  <s.1, (extend s.1s.2 by t.1t.2)>

Lemma: eu-seg-extend_wf
[e:EuclideanPlane]. ∀[s:ProperSegment]. ∀[t:Segment].  (s t ∈ ProperSegment)

Lemma: eu-seg-extend_functionality
e:EuclideanPlane. ∀[s1,s2:ProperSegment]. ∀[t1,t2:Segment].  (s1 t1 ≡ s2 t2) supposing (t1 ≡ t2 and s1 ≡ s2)

Lemma: eu-congruent-flip-seg
e:EuclideanPlane. ∀[a,b:Point].  ab ≡ ba

Definition: eu-length
|s| ==  (extend OX by s.1s.2)

Lemma: eu-length_wf
[e:EuclideanPlane]. ∀[s:Segment].  (|s| ∈ {p:Point| O_X_p} )

Definition: eu-le
p ≤ ==  X_p_q

Lemma: eu-le_wf
[e:EuclideanPlane]. ∀[p,q:{p:Point| O_X_p} ].  (p ≤ q ∈ ℙ)

Lemma: eu-le_transitivity
e:EuclideanPlane. ∀[p,q,r:{p:Point| O_X_p} ].  (p ≤ r) supposing (q ≤ and p ≤ q)

Definition: eu-lt
p < ==  p ≤ q ∧ (p q ∈ Point))

Lemma: eu-lt_wf
[e:EuclideanPlane]. ∀[p,q:{p:Point| O_X_p} ].  (p < q ∈ ℙ)

Lemma: eu-lt_transitivity
e:EuclideanPlane. ∀[p,q,r:{p:Point| O_X_p} ].  (p < r) supposing (q < and p ≤ q)

Lemma: eu-seg-congruent-iff-length
e:EuclideanPlane. ∀[s,t:Segment].  uiff(s ≡ t;|s| |t| ∈ {p:Point| O_X_p} )

Lemma: eu-congruent-iff-length
e:EuclideanPlane. ∀[a,b,c,d:Point].  uiff(ab=cd;|ab| |cd| ∈ {p:Point| O_X_p} )

Lemma: eu-length-flip
e:EuclideanPlane. ∀[a,b:Point].  (|ab| |ba| ∈ {p:Point| O_X_p} )

Lemma: eu-proper-extend-exists
e:EuclideanPlane. ∀q:Point. ∀a:{a:Point| ¬(q a ∈ Point)} . ∀b:Point. ∀c:{c:Point| ¬(b c ∈ Point)} .
  ∃x:Point. (q-a-x ∧ ax=bc)

Definition: eu-add-length
==  (extend Op by Xq)

Lemma: eu-add-length_wf
[e:EuclideanPlane]. ∀[x,y:{p:Point| O_X_p} ].  (x y ∈ {p:Point| O_X_p} )

Lemma: eu-add-length-comm
[e:EuclideanPlane]. ∀[x,y:{p:Point| O_X_p} ].  (x x ∈ {p:Point| O_X_p} )

Lemma: eu-add-length-zero
[e:EuclideanPlane]. ∀[x:{p:Point| O_X_p} ].  (x x ∈ {p:Point| O_X_p} )

Lemma: eu-length-null-segment
[e:EuclideanPlane]. ∀[a:Point].  (|aa| X ∈ {p:Point| O_X_p} )

Lemma: eu-le-null-segment
e:EuclideanPlane. ∀[p:{p:Point| O_X_p} ]. ∀[a:Point].  uiff(p ≤ |aa|;p |aa| ∈ {p:Point| O_X_p} )

Lemma: eu-lt-null-segment
e:EuclideanPlane. ∀[p:{p:Point| O_X_p} ]. ∀[a:Point].  uiff(p < |aa|;False)

Lemma: eu-lt-null-segment2
e:EuclideanPlane. ∀[p:{p:Point| O_X_p} ]. ∀[a,b:Point].  (False) supposing ((a b ∈ Point) and p < |ab|)

Lemma: eu-add-length-zero2
[e:EuclideanPlane]. ∀[x:{p:Point| O_X_p} ]. ∀[a:Point].  (x |aa| x ∈ {p:Point| O_X_p} )

Lemma: eu-add-length-zero3
[e:EuclideanPlane]. ∀[x:{p:Point| O_X_p} ]. ∀[a:Point].  (|aa| x ∈ {p:Point| O_X_p} )

Lemma: eu-add-length-between
[e:EuclideanPlane]. ∀[a,b,c:Point].  |ac| |ab| |bc| ∈ {p:Point| O_X_p}  supposing a_b_c

Lemma: eu-add-length-assoc
[e:EuclideanPlane]. ∀[x,y,z:{p:Point| O_X_p} ].  (x z ∈ {p:Point| O_X_p} )

Lemma: eu-add-length-cancel-left
[e:EuclideanPlane]. ∀[x,y,z:{p:Point| O_X_p} ].  y ∈ {p:Point| O_X_p}  supposing y ∈ {p:Point| O_X_p} 

Lemma: eu-add-length-cancel-right
[e:EuclideanPlane]. ∀[x,y,z:{p:Point| O_X_p} ].  y ∈ {p:Point| O_X_p}  supposing z ∈ {p:Point| O_X_p} 

Lemma: eu-le-add1
e:EuclideanPlane. ∀[p,q:{p:Point| O_X_p} ].  p ≤ q

Lemma: eu-seg-length-extend
[e:EuclideanPlane]. ∀[s:ProperSegment]. ∀[t:Segment].  (|s t| |s| |t| ∈ {p:Point| O_X_p} )

Lemma: eu-inner-five-segment
e:EuclideanPlane
  ∀[a,b,c,d,A,B,C,D:Point].  (bd=BD) supposing (cd=CD and ad=AD and bc=BC and ac=AC and A_B_C and a_b_c)

Lemma: eu-inner-five-segment'
e:EuclideanPlane
  ∀[a,b,c,A,B,C:Point].  (∀d,D:Point.  (bd=BD) supposing (cd=CD and ad=AD)) supposing (bc=BC and ac=AC and A_B_C and a_b\000C_c)

Lemma: eu-inner-three-segment
e:EuclideanPlane. ∀[a,b,c,A,B,C:Point].  (ab=AB) supposing (bc=BC and ac=AC and A_B_C and a_b_c)

Lemma: eu-congruent-between-implies-equal
e:EuclideanPlane. ∀[a,b,c,x:Point].  (b x ∈ Point) supposing (a_b_c and ab=ax and bc=xc)

Lemma: eu-congruent-between-exists
e:EuclideanPlane. ∀a,b,c,a',c':Point.
  (∃b':Point. (a'_b'_c' ∧ ab=a'b' ∧ bc=b'c')) supposing (a_b_c and ac=a'c' and (a b ∈ Point)))

Lemma: eu-congruent-preserves-between
e:EuclideanPlane. ∀[a,b,c,a',b',c':Point].  (a'_b'_c') supposing (bc=b'c' and ac=a'c' and ab=a'b' and a_b_c)

Lemma: eu-colinear-five-segment
e:EuclideanPlane
  ∀[a,b,c,d,A,B,C,D:Point].  (cd=CD) supposing (bd=BD and ad=AD and bc=BC and ab=AB and ac=AC and Colinear(a;b;c))

Lemma: eu-colinear-equidistant
e:EuclideanPlane. ∀[a,b,c,p,q:Point].  (cp=cq) supposing (ap=aq and bp=bq and Colinear(a;b;c))

Lemma: eu-between-eq-same-side
e:EuclideanPlane. ∀[A,B,C,D:Point].  ((¬A_C_D) ∧ A_D_C))) supposing ((¬(A B ∈ Point)) and A_B_C and A_B_D)

Lemma: eu-between-eq-same-side2
e:EuclideanPlane. ∀[A,B,C,D:Point].  ((¬B_C_D) ∧ B_D_C))) supposing ((¬(A B ∈ Point)) and A_B_C and A_B_D)

Lemma: eu-colinear-same-side
e:EuclideanPlane
  ∀[A,B,C,D:Point].  (Colinear(B;C;D)) supposing ((¬(B C ∈ Point)) and (A B ∈ Point)) and A_B_C and A_B_D)

Lemma: eu-colinear-same-side2
e:EuclideanPlane
  ∀[A,B,C,D:Point].  (Colinear(A;C;D)) supposing ((¬(A C ∈ Point)) and (A B ∈ Point)) and A_B_C and A_B_D)

Lemma: eu-colinear-between
e:EuclideanPlane
  ∀[A,B,C,D:Point].  (Colinear(A;C;D)) supposing ((¬(A C ∈ Point)) and (A B ∈ Point)) and A_C_B and A_D_B)

Lemma: eu-colinear-between2
e:EuclideanPlane
  ∀[A,B,C,D:Point].  (Colinear(B;C;D)) supposing ((¬(B C ∈ Point)) and (A B ∈ Point)) and A_C_B and A_D_B)

Lemma: eu-colinear-from-between
e:EuclideanPlane
  ∀[A,C,D:Point].  ((¬(A C ∈ Point))  (∃B:Point. ((¬(A B ∈ Point)) ∧ A_C_B ∧ A_D_B))  Colinear(A;C;D))

Lemma: eu-colinear-transitivity
e:EuclideanPlane
  ∀[A,C,B,D:Point].  (Colinear(A;B;C)  Colinear(B;C;D)  {((¬(A C ∈ Point))  Colinear(A;C;D)) ∧ Colinear(A;B;D)})

Definition: eu-colinear-set
eu-colinear-set(e;L) ==  (∀A∈L.(∀B∈L.(∀C∈L.(¬(A B ∈ Point))  Colinear(A;B;C))))

Lemma: eu-colinear-set_wf
[e:EuclideanPlane]. ∀[L:Point List].  (eu-colinear-set(e;L) ∈ ℙ)

Lemma: eu-colinear-is-colinear-set
e:EuclideanPlane. ∀A,B,C:Point.  (Colinear(A;B;C)  eu-colinear-set(e;[A; B; C]))

Lemma: eu-colinear-cons
e:EuclideanPlane. ∀L:Point List. ∀A:Point.
  (eu-colinear-set(e;[A L]) ⇐⇒ eu-colinear-set(e;L) ∧ (∀B∈L.(∀C∈L.(¬(A B ∈ Point))  Colinear(A;B;C))))

Lemma: eu-colinear-append
e:EuclideanPlane. ∀L1,L2:Point List.
  ((∃A,B:Point. ((¬(A B ∈ Point)) ∧ ((A ∈ L1) ∧ (A ∈ L2)) ∧ (B ∈ L1) ∧ (B ∈ L2)))
   eu-colinear-set(e;L1)
   eu-colinear-set(e;L2)
   eu-colinear-set(e;L1 L2))

Definition: eu-bisect-line
eu-bisect-line(e;a;b) ==  (a b ∈ Point)) ∧ (∃d:Point. (ad=db ∧ a_d_b))

Lemma: eu-bisect-line_wf
[e:EuclideanPlane]. ∀[a,b:Point].  (eu-bisect-line(e;a;b) ∈ ℙ)

Lemma: test-prove-distinct
e:EuclideanPlane. ∀A,B,C,X,Y,Z,W,U,V:Point.
  ((Colinear(A;B;X) ∨ A-X-B ∨ B-X-A)
   (A_B_C ∨ C_B_A)
   (Y_C_A ∨ A_C_Y)
   (ZW=AY ∨ ZW=YA)
   ZW=UV
   (U V ∈ Point)))

Lemma: test-colinear-sets
e:EuclideanPlane. ∀A,B,C,X,Y,Z,W,U,V:Point.
  (Colinear(A;B;X)  A_B_C  Y_C_A  (Y C ∈ Point))  Colinear(C;Y;X))

Lemma: eu-add-length-between-iff
e:EuclideanPlane. ∀[a,b,c:Point].  uiff(a_b_c;|ac| |ab| |bc| ∈ {p:Point| O_X_p} )

Lemma: eu-seg-length-test
e:EuclideanPlane. ∀[a,b,c,d,x,y:Point].  (ba=xy) supposing (dc=yx and ab=cd)

Lemma: eu-seg-length-test2
e:EuclideanPlane. ∀s1,s2:ProperSegment. ∀t1,t2,t3:Segment.  (s1 ≡ s2  t1 ≡ t2  t2 ≡ t3  s1 t1 ≡ s2 t3)

Lemma: eu-seg-length-test-ext
e:EuclideanPlane. ∀[a,b,c,d,x,y:Point].  (ba=xy) supposing (dc=yx and ab=cd)

Definition: eu-tri
Triangle(a;b;c) ==  (a b ∈ Point)) ∧ (a c ∈ Point)) ∧ (b c ∈ Point))

Lemma: eu-tri_wf
e:EuclideanPlane. ∀[a,b,c:Point].  (Triangle(a;b;c) ∈ ℙ)

Lemma: line-circle-continuity
e:EuclideanPlane. ∀a,b,p:Point. ∀q:{q:Point| ¬(q p ∈ Point)} .
  ((∃x:{x:Point| a_x_b ∧ (x b ∈ Point))} . ∃y:{y:Point| a_b_y} (ap=ax ∧ aq=ay))
   (∃y,z:Point. (ay=ab ∧ az=ab ∧ z_p_q ∧ p_y_q ∧ (y z ∈ Point)))))

Lemma: line-circle-continuity1
e:EuclideanPlane. ∀a,b,p:Point. ∀q:{q:Point| ¬(q p ∈ Point)} .
  ((∃x:{x:Point| a_x_b} . ∃y:{y:Point| a_b_y} (ap=ax ∧ aq=ay))  (∃y,z:Point. (ay=ab ∧ az=ab ∧ z_p_q ∧ p_y_q)))

Lemma: circle-circle-continuity
e:EuclideanPlane. ∀a,b,c,d,p,q,x,z:Point.
  (∃z1,z2:Point. (az1=ab ∧ az2=ab ∧ cz1=cd ∧ cz2=cd ∧ ((¬(x z ∈ Point))  (z1 z2 ∈ Point))))) supposing 
     (a_b_z and 
     a_x_b and 
     cq=cd and 
     cp=cd and 
     aq=az and 
     ap=ax and 
     (a c ∈ Point)))

Lemma: circle-circle-continuity2
e:EuclideanPlane. ∀a,b,c,d:Point.
  ((¬(a c ∈ Point))
   (∃p,q,x,z:Point. ((a_x_b ∧ a_b_z ∧ ap=ax ∧ aq=az ∧ cp=cd ∧ cq=cd) ∧ (x z ∈ Point))))
   (∃z1,z2:Point. (az1=ab ∧ az2=ab ∧ cz1=cd ∧ cz2=cd ∧ (z1 z2 ∈ Point)))))

Lemma: circle-circle-continuity1
e:EuclideanPlane. ∀a,b,c,d:Point.
  ((¬(a c ∈ Point))
   (∃p,q,x,z:Point. (a_x_b ∧ a_b_z ∧ ap=ax ∧ aq=az ∧ cp=cd ∧ cq=cd))
   (∃y:Point. (ay=ab ∧ cy=cd)))

Definition: eu-bisect-angle
eu-bisect-angle(e;a;b;c) ==
  (a b ∈ Point)) ∧ (b c ∈ Point)) ∧ (∃d:Point. ((¬(d a ∈ Point)) ∧ (d c ∈ Point)) ∧ abd dbc))

Lemma: eu-bisect-angle_wf
e:EuclideanPlane. ∀a,b,c:Point.  (eu-bisect-angle(e;a;b;c) ∈ ℙ)

Lemma: eu-5segSAS
e:EuclideanPlane. ∀a,b,c,f,g,A,B,C,F,G:Point.
  (af=AF ∧ fb=FB ∧ bc=BC ∧ ag=AG ∧ gc=GC)  fg=FG 
  supposing (Triangle(a;f;g) ∧ Triangle(A;F;G)) ∧ a_f_b ∧ a_g_c ∧ A_F_B ∧ A_G_C

Definition: eu-cong-angle
abc xyz ==
  (a b ∈ Point))
  ∧ (c b ∈ Point))
  ∧ (x y ∈ Point))
  ∧ (z y ∈ Point))
  ∧ (∃a',c',x',z':Point. (b_a_a' ∧ b_c_c' ∧ y_x_x' ∧ y_z_z' ∧ ba'=yx' ∧ bc'=yz' ∧ a'c'=x'z'))

Lemma: eu-cong-angle_wf
[e:EuclideanPlane]. ∀[a,b,c,x,y,z:Point].  (abc xyz ∈ ℙ)

Lemma: eu-cong-angle-symm
e:EuclideanPlane. ∀a,b,c:Point.  abc cba supposing (a b ∈ Point)) ∧ (c b ∈ Point))

Lemma: eu-cong-angle-symm2
e:EuclideanPlane. ∀a,b,c,x,y,z:Point.  (xyz abc  abc xyz)

Definition: eu-cong-tri
Cong3(abc,a'b'c') ==  ab=a'b' ∧ bc=b'c' ∧ ca=c'a'

Lemma: eu-cong-tri_wf
[e:EuclideanPlane]. ∀[a,b,c,a',b',c':Point].  (Cong3(abc,a'b'c') ∈ ℙ)

Definition: eu-out
out(p ab) ==  (p a ∈ Point)) ∧ (p b ∈ Point)) ∧ ((¬p_a_b) ∧ p_b_a)))

Lemma: eu-out_wf
[e:EuclideanPlane]. ∀[p,a,b:Point].  (out(p ab) ∈ ℙ)

Lemma: eu-out-refl
e:EuclideanPlane. ∀a,b,c:Point.  (out(a bc)  out(a cb))

Definition: eu-five-seg-compressed
FSC(a;b;c;d  a';b';c';d') ==  Colinear(a;b;c) ∧ Cong3(abc,a'b'c') ∧ ad=a'd' ∧ bd=b'd'

Lemma: eu-five-seg-compressed_wf
[e:EuclideanPlane]. ∀[a,b,c,d,a',b',c',d':Point].  (FSC(a;b;c;d  a';b';c';d') ∈ ℙ)

Lemma: eu-fsc-ap
e:EuclideanPlane. ∀a,b,c,d,a',b',c',d':Point.  (FSC(a;b;c;d  a';b';c';d')  (a b ∈ Point))  cd=c'd')

Definition: eu-midpoint
a=m=b ==  a_m_b ∧ am=mb

Lemma: eu-midpoint_wf
[e:EuclideanPlane]. ∀[m,a,b:Point].  (a=m=b ∈ ℙ)

Lemma: eu-midpoint-trivial
e:EuclideanPlane. ∀a,b:Point.  (a=b=a  (a b ∈ Point))

Definition: eu-perpendicular
Per(a;b;c) ==  ∃c':Point. (c=b=c' ∧ ac=ac')

Lemma: eu-perpendicular_wf
[e:EuclideanPlane]. ∀[a,b,c:Point].  (Per(a;b;c) ∈ ℙ)

Definition: eu-perp-in
ab  ⊥cd ==  Colinear(a;b;x) ∧ Colinear(c;d;x) ∧ (∀u,v:Point.  (Colinear(a;b;u)  Colinear(c;d;v)  Per(u;x;v)))

Lemma: eu-perp-in_wf
[e:EuclideanPlane]. ∀[x,a,b,c,d:Point].  (ab  ⊥cd ∈ ℙ)

Definition: eu-perp
ab ⊥ cd ==  ∃x:Point. ab  ⊥cd

Lemma: eu-perp_wf
[e:EuclideanPlane]. ∀[a,b,c,d:Point].  (ab ⊥ cd ∈ ℙ)

Definition: eu-le-pt
ab≤cd ==  ∃y:Point. (c_y_d ∧ ab=cy)

Lemma: eu-le-pt_wf
[e:EuclideanStructure]. ∀[a,b,c,d:Point].  (ab≤cd ∈ ℙ)

Lemma: eu-perp-three
e:EuclideanPlane. ∀x,a,b,c:Point.  (ba  ⊥ca  (x a ∈ Point))

Lemma: eu-be-neq
e:EuclideanPlane. ∀a,b,c:Point.  ((¬(a b ∈ Point))  a_b_c  (a c ∈ Point)))

Lemma: eu-conga-to-cong3
E:EuclideanPlane. ∀a,b,c,d,e,f:Point.
  (abc def  (∃a',c',d',f':Point. (out(b a'a) ∧ out(b cc') ∧ out(e d'd) ∧ out(e ff') ∧ Cong3(a'bc',d'ef'))))

Lemma: eu-between-eq-seg-eq
e:EuclideanPlane. ∀a,b,c,a',b',c':Point.  (a_b_c  a'_b'_c'  ab=a'b'  ac=a'c'  bc=b'c')

Lemma: eu-eqt
e:EuclideanPlane. ∀a,b,c:{p:Point| O_X_p} .
  (((a b ∈ {p:Point| O_X_p} ) ∧ (b c ∈ {p:Point| O_X_p} ))  (a c ∈ {p:Point| O_X_p} ))

Lemma: eu-eq-x-implies-eq
e:EuclideanPlane. ∀a,b:Point.  ((X |ab| ∈ {p:Point| O_X_p}  (a b ∈ Point))

Lemma: eu-sum-eq-x
e:EuclideanPlane. ∀a,b,c,d:Point.  ((X |ab| |cd| ∈ {p:Point| O_X_p}  ((a b ∈ Point) ∧ (c d ∈ Point)))

Lemma: eu-ab-eq-x
e:EuclideanPlane. ∀a,b:Point.  ((a b ∈ Point)  (X |ab| ∈ {p:Point| O_X_p} ))

Lemma: eu-colinear-switch
e:EuclideanPlane. ∀a,b,c:Point.  (Colinear(a;b;c)  (a c ∈ Point))  Colinear(a;c;b))

Lemma: eu-colinear-switch2
e:EuclideanPlane. ∀a,b,c:Point.  (Colinear(a;b;c)  Colinear(b;a;c))

Lemma: eu-colinear-switch3
e:EuclideanPlane. ∀a,b,c:Point.  ((¬(c b ∈ Point))  Colinear(a;b;c)  Colinear(c;b;a))

Lemma: eu-colinear-trivial
e:EuclideanPlane. ∀a,b:Point.  ((¬(a b ∈ Point))  (Colinear(a;b;b) ∧ Colinear(b;a;b)))

Lemma: eu-cong3-to-conga-aux
e:EuclideanPlane. ∀b,a,a',a0,e0,d,d',d0:Point.
  (out(b aa')  out(e0 dd')  b_a_a0  e0_d_d0  ba'=e0d'  aa0=e0d  dd0=ba  (ba0=e0d0 ∧ a'a0=d'd0))

Lemma: eu-cong3-to-conga
e:EuclideanPlane. ∀a,b,c,d,E,f:Point.
  ((∃a',c',d',f':Point. (out(b a'a) ∧ out(b c'c) ∧ out(E d'd) ∧ out(E f'f) ∧ Cong3(a'bc',d'Ef')))  abc dEf)

Lemma: eu-be-compress
e:EuclideanPlane. ∀a,b,c:Point.  (a_b_c  a_c_b  (b c ∈ Point))

Lemma: eu-inner-pasch-ex
e:EuclideanPlane. ∀a,b:Point. ∀c:{c:Point| ¬Colinear(a;b;c)} . ∀p:{p:Point| a-p-c} . ∀q:{q:Point| b_q_c} .
  ∃x:Point. (p-x-b ∧ q-x-a ∧ (x eu-inner-pasch(e;a;b;c;p;q) ∈ Point))

Lemma: eu-be-end-eq
e:EuclideanPlane. ∀a,b,c:Point.  (a_b_c  ab=ac  (b c ∈ Point))

Lemma: eu-between-eq-middle
e:EuclideanPlane. ∀a,b,c,d:Point.  ((¬(a d ∈ Point))  a_b_d  a_c_d  ((¬b_c_d) ∧ c_b_d))))

Lemma: eu-eq-implies-col
e:EuclideanPlane. ∀a,b,c:Point.  ((¬(a b ∈ Point))  (b c ∈ Point)  Colinear(a;b;c))

Lemma: eu-col-connect
e:EuclideanPlane. ∀a,b,c,d:Point.  (Colinear(a;b;c)  Colinear(c;b;d)  Colinear(a;b;d))

Lemma: p8eu
e:EuclideanPlane. ∀a,b,c,x,y,z:Point.
  Cong3(abc,xyz)  (abc xyz ∧ bac yxz ∧ bca yzx) supposing Triangle(a;b;c) ∧ Triangle(x;y;z)

Lemma: eu-bisect-angle
e:EuclideanPlane. ∀a,b,c:Point.
  ((¬(a b ∈ Point))  (b c ∈ Point))  (∃d:Point. ((¬(d a ∈ Point)) ∧ (d c ∈ Point)) ∧ abd dbc)))

Lemma: eu-sas
e:EuclideanPlane. ∀a,b,c,A,B,C:Point.
  ((ab=AB ∧ ac=AC) ∧ bac BAC)  bc=BC supposing Triangle(a;b;c) ∧ Triangle(A;B;C)

Lemma: p5eu
e:EuclideanPlane. ∀a,b,c:Point.  ((ab=ac ∧ Triangle(a;b;c))  (∃j,k:Point. jbc kcb))

Lemma: p4eu
e:EuclideanPlane. ∀a,b,c,A,B,C:Point.
  (ab=AB ∧ ac=AC ∧ bac BAC)  (bc=BC ∧ abc ABC ∧ bca BCA ∧ Cong3(abc,ABC)) 
  supposing Triangle(a;b;c) ∧ Triangle(A;B;C)

Comment: Editor aliases for Constructive Geometry

All theorems of constructive geometry have the form
⌜∀e:EuclideanPlane. [prop]⌝
(to enter that type "all" and then "eu-pl" in the [type] slot).
  
To edit formulas about geometry use the following editor aliases:

eu-pt  ⌜eu-point([term])⌝ --then fill in e  (your EuclideanPlane) and it will
                             display as ⌜Point⌝
eu-cong  ⌜ab=cd⌝    --- first slot is (your EuclideanPlane) then a, b, c, d.

eu-bt  ⌜a-b-c⌝  -- this is strict betweeness,  first slot is e.
eu-be  ⌜a_b_c⌝  -- non-strict betweeness ( ⌜b ∈ Point⌝ and ⌜c ∈ Point⌝ are allowed).



Comment: Tactics for Constructive Geometry

All theorems of constructive geometry have the form
⌜∀e:EuclideanPlane. [prop]⌝

To prove theorem like
  ⌜∀e:EuclideanPlane. ∀a,b:Point.  (P (a; b)  (∃c:Point. (a; b; c)))⌝
one typically starts with 
Auto and then "construct" the desired point by instantiating
lemmas (that have already been proved to construct points)
or invoking the basic constructions.

To invove the construction that extends the segments AB by the segment CD,
use the tactic 
  Prolong ⌜A⌝ ⌜B⌝ `x' ⌜C⌝ ⌜D⌝
The points A, B, C, will usually be variables (of type ⌜Point⌝but
the can be expressions, too, so they are Nuprl terms 
(type control-o to get a ⌜[term]⌝ slot). The `x' is ML variable.
It is used to name the new endpoint of the extended segment.

We have added "circle-circle-continutity" as theorem
(it is unproved, so far, but does follow from the axioms, so it is safe
to use it in proofs). It lets you construct the intersection point(s) of
two cicles that overlap.
To invoke that use either  
  CircleCircle1 ⌜a⌝;⌜b⌝ ⌜c⌝ ⌜d⌝ `x'
 or
  CircleCircle2 ⌜a⌝;⌜b⌝ ⌜c⌝ ⌜d⌝ `x' `y'
(for more information about these, see: Error :circle-circle-tactics).

"line-circle-continuity" is one of our axioms.
It lets you construct the intersection point(s) of line and circle
(that overlap).
Use 
   CircleLine1 ⌜a⌝;⌜b⌝ ⌜u⌝ ⌜v⌝ `x' `y'
 or
  CircleLine2 ⌜a⌝;⌜b⌝ ⌜u⌝ ⌜v⌝ `x' `y'
(see Error :line-circle-tactics for more information).

To construct the "crossing point" for segments ab and cd  (and name it x),
 use SegmentsCross ⌜a⌝ ⌜b⌝ ⌜c⌝ ⌜d⌝ `x'

 
 .



Lemma: euclid-P1
e:EuclideanPlane. ∀A,B:Point.  ∃C:Point. (AC=AB ∧ BC=AB ∧ AC=BC) supposing ¬(A B ∈ Point)

Lemma: euclid-P1-ext
e:EuclideanPlane. ∀A,B:Point.  ∃C:Point. (AC=AB ∧ BC=AB ∧ AC=BC) supposing ¬(A B ∈ Point)

Lemma: euclid-P2
e:EuclideanPlane. ∀A,B,C:Point.  ∃L:Point. AL=BC supposing ¬(A B ∈ Point)

Comment: proposition 3
In proposition3, segment AB is "longer than" line C.
We use segment C1C2 for C, but we still have to define
what it means for AB to be longer than C1C2.

We can use the lengths ⌜|AB|⌝ and ⌜|C1C2|⌝
(which are points in ⌜{p:Point| O_X_p} ⌝ )
but we need to define the  "lt" (less-than) relation on them.

For and in ⌜{p:Point| O_X_p} ⌝ we say ⌜p ≤ q⌝ if
 ⌜X_p_q⌝ and ⌜p < q⌝  if ⌜p ≤ q ∧ (p q ∈ Point))⌝⋅

Lemma: euclid-P3
e:EuclideanPlane. ∀A,B,C1,C2:Point.  ∃E:Point. (A_E_B ∧ AE=C1C2) supposing (C1 C2 ∈ Point)) ∧ |C1C2| < |AB|

Lemma: euclid-P3-ext
e:EuclideanPlane. ∀A,B,C1,C2:Point.  ∃E:Point. (A_E_B ∧ AE=C1C2) supposing (C1 C2 ∈ Point)) ∧ |C1C2| < |AB|

Lemma: e1
e:EuclideanPlane. ∀A,B:Point.  ∃C:Point. (AC=AB ∧ BC=AB ∧ AC=BC) supposing ¬(A B ∈ Point)

Lemma: p4eu
e:EuclideanPlane. ∀a,b,c,A,B,C:Point.
  (ab=AB ∧ ac=AC ∧ bac BAC)  (bc=BC ∧ abc ABC ∧ bca BCA ∧ Cong3(abc,ABC)) 
  supposing Triangle(a;b;c) ∧ Triangle(A;B;C)



Home Index