Library Geometry

Section Geometry.


Parameter Point : Type.

Parameter Between : Point -> Point -> Point -> Prop.

Parameter Congruent : Point -> Point -> Point -> Point -> Prop.

Axiom cong_reflexivity: forall x y, Congruent x y y x.
Axiom cong_identity: forall x y z, Congruent x y z z -> x=y.
Axiom cong_transitivity: forall x y z u v w,
 (Congruent x y z u /\ Congruent x y v w) ->
 Congruent z u v w.

Axiom btw_identity: forall x y, Between x y x -> x=y.
Axiom btw_pasch: forall x y z u v,
 (Between x u z /\ Between y v z) ->
 exists a, (Between u a y /\ Between v a x).
Axiom btw_continuity: forall phi psi: Point -> Prop,
 (exists a, forall x y, (phi x/\psi y)->Between a x y)->
 (exists b, forall x y, (phi x/\psi y)->Between x b y).
Axiom btw_lowerdimension: exists a, exists b, exists c,
 (~ Between a b c)/\(~ Between b c a)/\(~ Between c a b).

Axiom upperdimension: forall x y z u v,
 (Congruent x u x v /\ Congruent y u y v /\ Congruent z u z v
 /\ u<>v) ->
(Between x y z \/ Between y z x \/ Between z x y).
Axiom euclid: forall x y z u v w,
 ((Between x y w /\ Congruent x y y w) /\
 (Between x u v /\ Congruent x u u v) /\
 (Between y u z /\ Congruent y u z u)) ->
Congruent y z v w.
Axiom fivesegment: forall x y z u x' y' z' u',
 (x<>y /\ Between x y z /\ Between x' y' z' /\
 Congruent x y x' y' /\ Congruent y z y' z' /\
 Congruent x u x' u' /\ Congruent y u y' u')
-> Congruent z u z' u'.
Axiom segmentconstruction: forall x y z w, exists a,
 Between w x a /\ Congruent x a y z.

Theorem cong_reflexivity2: forall A B : Point,
 Congruent A B A B.

Theorem cong_symmetry : forall A B C D,
 Congruent A B C D -> Congruent C D A B.

Theorem cong_transitivity2 : forall A B C D E F,
 Congruent A B C D -> Congruent C D E F
-> Congruent A B E F.

Theorem cong_right_commutativity : forall A B C D,
 Congruent A B C D -> Congruent A B D C.

Theorem cong_trivial_identity:
 forall A B, Congruent A A B B.

Theorem cong_reverse_identity : forall A C D,
 Congruent A A C D -> C=D.

Theorem cong_commutativity : forall A B C D,
 Congruent A B C D -> Congruent B A D C.

Theorem between_trivial : forall A B : Point,
 Between A B B.

Theorem between_symmetry : forall A B C : Point,
   Between A B C -> Between C B A.

Theorem between_trivial2: forall A B, Between A A B.

Theorem between_equality: forall A B C,
 Between A B C -> Between B A C -> A = B.

Theorem between_inner_transitivity : forall A B C D,
Between A B D -> Between B C D -> Between A B C.

Theorem between_exchange3 : forall A B C D,
Between A B C -> Between A C D -> Between B C D.


End Geometry.