Require Import GeoCoq.Tarski_dev.Ch12_parallel_inter_dec.
Require Import Morphisms.
Require Import GeoCoq.Axioms.hilbert_axioms.
Require Import GeoCoq.Axioms.parallel_postulates.
Require Import GeoCoq.Meta_theory.Parallel_postulates.tarski_playfair.
Require Import GeoCoq.Meta_theory.Parallel_postulates.SPP_ID.
Require Import GeoCoq.Meta_theory.Dimension_axioms.upper_dim_3.
Require Import GeoCoq.Meta_theory.Parallel_postulates.parallel_postulates.

Require Export GeoCoq.Utils.triples.

Section T.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

(** We need a notion of line. *)

Definition Line := @Couple Tpoint.
Definition Lin := build_couple Tpoint.

Definition IncidentL := fun A l => Col A (P1 l) (P2 l).

(** * Group I Combination *)

(** For every pair of distinct points there is a line containing them. *)

Lemma axiom_line_existence : forall A B, A<>B -> exists l, IncidentL A l /\ IncidentL B l.
Proof.
(* Goal: forall (l : @Couple (@Tpoint Tn)) (P : @Tpoint Tn) (m1 m2 : @Couple (@Tpoint Tn)) (_ : not (@IncidentL Tn P l)) (_ : Para l m1) (_ : @IncidentL Tn P m1) (_ : Para l m2) (_ : @IncidentL Tn P m2), @EqL Tn m1 m2 *)
intros.
(* Goal: @ex (@Couple (@Tpoint Tn)) (fun l : @Couple (@Tpoint Tn) => and (IncidentL A l) (IncidentL B l)) *)
exists (Lin A B H).
(* Goal: forall (M : @Tpoint Tn) (l : @Couple (@Tpoint Tn)) (_ : @Col Tn M (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l)), IncidentL M l *)
unfold IncidentL.
(* Goal: @CongA Tn A B C A' B' C' *)
intuition.
Qed.

(** We need a notion of equality over lines. *)

Definition EqL : relation Line := fun l m => forall X, IncidentL X l <-> IncidentL X m.

Infix "=l=" := EqL (at level 70):type_scope.

Lemma incident_eq : forall A B l, forall H : A<>B,
 IncidentL A l -> IncidentL B l ->
 (Lin A B H) =l= l.
Proof.
(* Goal: forall (l : @Couple (@Tpoint Tn)) (P : @Tpoint Tn) (m1 m2 : @Couple (@Tpoint Tn)) (_ : not (@IncidentL Tn P l)) (_ : Para l m1) (_ : @IncidentL Tn P m1) (_ : Para l m2) (_ : @IncidentL Tn P m2), @EqL Tn m1 m2 *)
intros.
(* Goal: forall (l m : Line) (_ : EqL l m), EqL m l *)
unfold EqL.
(* Goal: forall (l : @Couple (@Tpoint Tn)) (P : @Tpoint Tn) (m1 m2 : @Couple (@Tpoint Tn)) (_ : not (@IncidentL Tn P l)) (_ : Para l m1) (_ : @IncidentL Tn P m1) (_ : Para l m2) (_ : @IncidentL Tn P m2), @EqL Tn m1 m2 *)
intros.
(* Goal: @OS Tn A B P Q *)
unfold IncidentL in *.
(* Goal: iff (@Col Tn X (@P1 (@Tpoint Tn) (Lin A B H)) (@P2 (@Tpoint Tn) (Lin A B H))) (@Col Tn X (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l)) *)
replace (P1 (Lin A B H)) with A; trivial.
(* Goal: iff (@Col Tn X A (@P2 (@Tpoint Tn) (Lin A B H))) (@Col Tn X (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l)) *)
replace (P2 (Lin A B H)) with B; trivial.
(* Goal: iff (@Col Tn X A B) (@Col Tn X (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l)) *)
split;intro.
(* Goal: @Col Tn A B C *)
assert (T:=Cond l).
(* Goal: @Col Tn X (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l) *)
(* Goal: @Col Tn X A B *)
elim (eq_dec_points X B); intro.
(* Goal: @Col Tn X (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l) *)
(* Goal: @Col Tn X (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l) *)
(* Goal: @Col Tn X A B *)
subst X.
(* Goal: not (@eq (@Tpoint Tn) A P) *)
(* Goal: or (@Bet Tn P A B) (@Bet Tn P B A) *)
auto.
(* Goal: @Col Tn X (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l) *)
(* Goal: @Col Tn X A B *)
assert (Col (P1 l) A B).
(* Goal: @Col Tn (@P1 (@Tpoint Tn) l) A B *)
(* Goal: @Col Tn X (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l) *)
(* Goal: @Col Tn X A B *)
apply col_transitivity_1 with (P2 l); Col.
(* Goal: @Col Tn X (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l) *)
(* Goal: @Col Tn X A B *)
assert (Col (P2 l) A B).
(* Goal: @Col Tn (@P2 (@Tpoint Tn) l) A B *)
(* Goal: @Col Tn X (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l) *)
(* Goal: @Col Tn X A B *)
apply (col_transitivity_2 (P1 l)); Col.
(* Goal: @Col Tn X (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l) *)
(* Goal: @Col Tn X A B *)
apply (col3 A B); Col.

(* Goal: @Col Tn X A B *)
assert (U:=Cond l).
(* Goal: @Col Tn A B C *)
apply (col3 (P1 l) (P2 l)); Col.
Qed.

(** Our equality is an equivalence relation. *)

Lemma eq_transitivity : forall l m n, l =l= m -> m =l= n -> l =l= n.
Proof.
(* Goal: forall (l m n : Line) (_ : EqL l m) (_ : EqL m n), EqL l n *)
unfold EqL,IncidentL.
(* Goal: forall (l : @Couple (@Tpoint Tn)) (P : @Tpoint Tn) (m1 m2 : @Couple (@Tpoint Tn)) (_ : not (@IncidentL Tn P l)) (_ : Para l m1) (_ : @IncidentL Tn P m1) (_ : Para l m2) (_ : @IncidentL Tn P m2), @EqL Tn m1 m2 *)
intros.
(* Goal: iff (IncidentP X q) (IncidentP X p) *)
assert (T:=H X).
(* Goal: iff (@Col Tn X (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l)) (@Col Tn X (@P1 (@Tpoint Tn) n) (@P2 (@Tpoint Tn) n)) *)
assert (V:= H0 X).
(* Goal: @CongA Tn A B C A' B' C' *)
split;intro;intuition.
Qed.

Lemma eq_reflexivity : forall l, l =l= l.
Proof.
(* Goal: forall (l : @Couple (@Tpoint Tn)) (P : @Tpoint Tn) (m1 m2 : @Couple (@Tpoint Tn)) (_ : not (@IncidentL Tn P l)) (_ : Para l m1) (_ : @IncidentL Tn P m1) (_ : Para l m2) (_ : @IncidentL Tn P m2), @EqL Tn m1 m2 *)
intros.
(* Goal: forall (l m : Line) (_ : EqL l m), EqL m l *)
unfold EqL.
(* Goal: @CongA Tn A B C A' B' C' *)
intuition.
Qed.

Lemma eq_symmetry : forall l m, l =l= m -> m =l= l.
Proof.
(* Goal: forall (l m : Line) (_ : EqL l m), EqL m l *)
unfold EqL.
(* Goal: forall (l : @Couple (@Tpoint Tn)) (P : @Tpoint Tn) (m1 m2 : @Couple (@Tpoint Tn)) (_ : not (@IncidentL Tn P l)) (_ : Para l m1) (_ : @IncidentL Tn P m1) (_ : Para l m2) (_ : @IncidentL Tn P m2), @EqL Tn m1 m2 *)
intros.
(* Goal: iff (IncidentP X q) (IncidentP X p) *)
assert (T:=H X).
(* Goal: @CongA Tn A B C A' B' C' *)
intuition.
Qed.

Instance EqL_Equiv : Equivalence EqL.
Proof.
(* Goal: @Hilbert_euclidean_ID (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) Hilbert_euclidean_follows_from_Tarski_euclidean *)
split.
(* Goal: @Reflexive Plane EqP *)
(* Goal: @Symmetric Plane EqP *)
(* Goal: @Transitive Plane EqP *)
unfold Reflexive.
(* Goal: forall x : Line, EqL x x *)
(* Goal: @Symmetric Line EqL *)
(* Goal: @Transitive Line EqL *)
apply eq_reflexivity.
(* Goal: @Symmetric Plane EqP *)
(* Goal: @Transitive Plane EqP *)
unfold Symmetric.
(* Goal: forall (x y : Line) (_ : EqL x y), EqL y x *)
(* Goal: @Transitive Line EqL *)
apply eq_symmetry.
(* Goal: @Transitive Plane EqP *)
unfold Transitive.
(* Goal: forall (x y z : Line) (_ : EqL x y) (_ : EqL y z), EqL x z *)
apply eq_transitivity.
Defined.


(** The equality is compatible with IncidentL *)

Lemma eq_incident : forall A l m, l =l= m ->
 (IncidentL A l <-> IncidentL A m).
Proof.
(* Goal: forall (l : @Couple (@Tpoint Tn)) (P : @Tpoint Tn) (m1 m2 : @Couple (@Tpoint Tn)) (_ : not (@IncidentL Tn P l)) (_ : Para l m1) (_ : @IncidentL Tn P m1) (_ : Para l m2) (_ : @IncidentL Tn P m2), @EqL Tn m1 m2 *)
intros.
split;intros;
unfold EqL in *;
assert (T:= H A);
(* Goal: @CongA Tn A B C A' B' C' *)
intuition.
Qed.

Instance incident_Proper (A:Tpoint) :
Proper (EqL ==>iff) (IncidentL A).
Proof.
(* Goal: @Proper (forall _ : Plane, Prop) (@respectful Plane Prop EqP iff) (IncidentP A) *)
intros a b H .
(* Goal: iff (IncidentL A a) (IncidentL A b) *)
apply eq_incident.
(* Goal: @OS Tn (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l) A B *)
assumption.
Defined.

Lemma axiom_Incid_morphism :
 forall P l m, IncidentL P l -> EqL l m -> IncidentL P m.
Proof.
(* Goal: forall (l : @Couple (@Tpoint Tn)) (P : @Tpoint Tn) (m1 m2 : @Couple (@Tpoint Tn)) (_ : not (@IncidentL Tn P l)) (_ : Para l m1) (_ : @IncidentL Tn P m1) (_ : Para l m2) (_ : @IncidentL Tn P m2), @EqL Tn m1 m2 *)
intros.
(* Goal: IncidentL P m *)
destruct (eq_incident P l m H0).
(* Goal: @CongA Tn A B C A' B' C' *)
intuition.
Qed.

Lemma axiom_Incid_dec : forall P l, IncidentL P l \/ ~IncidentL P l.
Proof.
(* Goal: forall (l : @Couple (@Tpoint Tn)) (P : @Tpoint Tn) (m1 m2 : @Couple (@Tpoint Tn)) (_ : not (@IncidentL Tn P l)) (_ : Para l m1) (_ : @IncidentL Tn P m1) (_ : Para l m2) (_ : @IncidentL Tn P m2), @EqL Tn m1 m2 *)
intros.
(* Goal: forall (M : @Tpoint Tn) (l : @Couple (@Tpoint Tn)) (_ : @Col Tn M (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l)), IncidentL M l *)
unfold IncidentL.
(* Goal: or (@Col Tn P (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l)) (not (@Col Tn P (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l))) *)
apply col_dec.
Qed.

(** There is only one line going through two points. *)

Lemma axiom_line_uniqueness : forall A B l m, A <> B ->
 IncidentL A l -> IncidentL B l -> IncidentL A m -> IncidentL B m ->
 l =l= m.
Proof.
(* Goal: forall (l : @Couple (@Tpoint Tn)) (P : @Tpoint Tn) (m1 m2 : @Couple (@Tpoint Tn)) (_ : not (@IncidentL Tn P l)) (_ : Para l m1) (_ : @IncidentL Tn P m1) (_ : Para l m2) (_ : @IncidentL Tn P m2), @EqL Tn m1 m2 *)
intros.
(* Goal: EqL l m *)
assert ((Lin A B H) =l= l).
(* Goal: @OS Tn (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l) A B *)
eapply incident_eq;assumption.
(* Goal: EqL l m *)
assert ((Lin A B H) =l= m).
(* Goal: @OS Tn (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l) A B *)
eapply incident_eq;assumption.
(* Goal: EqL l m *)
rewrite <- H4.
(* Goal: @OS Tn (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l) A B *)
assumption.
Qed.

(** Every line contains at least two points. *)

Lemma axiom_two_points_on_line : forall l,
  { A : Tpoint & { B | IncidentL B l /\ IncidentL A l /\ A <> B}}.
Proof.
(* Goal: forall (l : @Couple (@Tpoint Tn)) (P : @Tpoint Tn) (m1 m2 : @Couple (@Tpoint Tn)) (_ : not (@IncidentL Tn P l)) (_ : Para l m1) (_ : @IncidentL Tn P m1) (_ : Para l m2) (_ : @IncidentL Tn P m2), @EqL Tn m1 m2 *)
intros.
(* Goal: @sigT (@Tpoint Tn) (fun A : @Tpoint Tn => @sig (@Tpoint Tn) (fun B : @Tpoint Tn => and (IncidentL B l) (and (IncidentL A l) (not (@eq (@Tpoint Tn) A B))))) *)
exists (P1 l).
(* Goal: @sig (@Tpoint Tn) (fun B : @Tpoint Tn => and (IncidentL B l) (and (IncidentL (@P1 (@Tpoint Tn) l) l) (not (@eq (@Tpoint Tn) (@P1 (@Tpoint Tn) l) B)))) *)
exists (P2 l).
(* Goal: forall (M : @Tpoint Tn) (l : @Couple (@Tpoint Tn)) (_ : @Col Tn M (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l)), IncidentL M l *)
unfold IncidentL.
(* Goal: and (@Col Tn (@P2 (@Tpoint Tn) l) (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l)) (and (@Col Tn (@P1 (@Tpoint Tn) l) (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l)) (not (@eq (@Tpoint Tn) (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l)))) *)
repeat split;Col.
(* Goal: not (@eq (@Tpoint Tn) (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l)) *)
exact (Cond l).
Qed.

(** Definition of the collinearity predicate.
 We say that three points are collinear if they belongs to the same line. *)

Definition Col_H := fun A B C =>
  exists l, IncidentL A l /\ IncidentL B l /\ IncidentL C l.

(** We show that the notion of collinearity we just defined is equivalent to the
 notion of collinearity of Tarski. *)

Lemma cols_coincide_1 : forall A B C, Col_H A B C -> Col A B C.
Proof.
(* Goal: forall (l : @Couple (@Tpoint Tn)) (P : @Tpoint Tn) (m1 m2 : @Couple (@Tpoint Tn)) (_ : not (@IncidentL Tn P l)) (_ : Para l m1) (_ : @IncidentL Tn P m1) (_ : Para l m2) (_ : @IncidentL Tn P m2), @EqL Tn m1 m2 *)
intros.
(* Goal: @Col Tn A B C *)
unfold Col_H in H.
(* Goal: @Col Tn A B C *)
DecompExAnd H l.
(* Goal: @OS Tn A B P Q *)
unfold IncidentL in *.
(* Goal: @Col Tn A B C *)
assert (T:=Cond l).
(* Goal: @Col Tn A B C *)
apply (col3 (P1 l) (P2 l)); Col.
Qed.

Lemma cols_coincide_2 : forall A B C, Col A B C -> Col_H A B C.
Proof.
(* Goal: forall (l : @Couple (@Tpoint Tn)) (P : @Tpoint Tn) (m1 m2 : @Couple (@Tpoint Tn)) (_ : not (@IncidentL Tn P l)) (_ : Para l m1) (_ : @IncidentL Tn P m1) (_ : Para l m2) (_ : @IncidentL Tn P m2), @EqL Tn m1 m2 *)
intros.
(* Goal: Col_H A B C *)
unfold Col_H.
(* Goal: @ex (@Couple (@Tpoint Tn)) (fun l : @Couple (@Tpoint Tn) => and (IncidentL A l) (and (IncidentL B l) (IncidentL C l))) *)
elim (eq_dec_points A B); intro.
(* Goal: or (@Bet Tn P A B) (@Bet Tn P B A) *)
subst B.
(* Goal: @ex (@Couple (@Tpoint Tn)) (fun l : @Couple (@Tpoint Tn) => and (IncidentL A l) (and (IncidentL A l) (IncidentL C l))) *)
(* Goal: @ex (@Couple (@Tpoint Tn)) (fun l : @Couple (@Tpoint Tn) => and (IncidentL A l) (and (IncidentL B l) (IncidentL C l))) *)
elim (eq_dec_points A C); intro.
(* Goal: @ex (@Couple (@Tpoint Tn)) (fun l : @Couple (@Tpoint Tn) => and (IncidentL A l) (and (IncidentL A l) (IncidentL C l))) *)
(* Goal: @ex (@Couple (@Tpoint Tn)) (fun l : @Couple (@Tpoint Tn) => and (IncidentL A l) (and (IncidentL A l) (IncidentL C l))) *)
(* Goal: @ex (@Couple (@Tpoint Tn)) (fun l : @Couple (@Tpoint Tn) => and (IncidentL A l) (and (IncidentL B l) (IncidentL C l))) *)
subst C.
(* Goal: @ex (@Couple (@Tpoint Tn)) (fun l : @Couple (@Tpoint Tn) => and (IncidentL A l) (and (IncidentL A l) (IncidentL A l))) *)
(* Goal: @ex (@Couple (@Tpoint Tn)) (fun l : @Couple (@Tpoint Tn) => and (IncidentL A l) (and (IncidentL A l) (IncidentL C l))) *)
(* Goal: @ex (@Couple (@Tpoint Tn)) (fun l : @Couple (@Tpoint Tn) => and (IncidentL A l) (and (IncidentL B l) (IncidentL C l))) *)
assert (exists B, A<>B).
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => not (@eq (@Tpoint Tn) A B)) *)
(* Goal: @ex (@Couple (@Tpoint Tn)) (fun l : @Couple (@Tpoint Tn) => and (IncidentL A l) (and (IncidentL A l) (IncidentL A l))) *)
(* Goal: @ex (@Couple (@Tpoint Tn)) (fun l : @Couple (@Tpoint Tn) => and (IncidentL A l) (and (IncidentL A l) (IncidentL C l))) *)
(* Goal: @ex (@Couple (@Tpoint Tn)) (fun l : @Couple (@Tpoint Tn) => and (IncidentL A l) (and (IncidentL B l) (IncidentL C l))) *)
eapply another_point.
(* Goal: @ex (@Couple (@Tpoint Tn)) (fun l : @Couple (@Tpoint Tn) => and (IncidentL A l) (and (IncidentL A l) (IncidentL A l))) *)
(* Goal: @ex (@Couple (@Tpoint Tn)) (fun l : @Couple (@Tpoint Tn) => and (IncidentL A l) (and (IncidentL A l) (IncidentL C l))) *)
(* Goal: @ex (@Couple (@Tpoint Tn)) (fun l : @Couple (@Tpoint Tn) => and (IncidentL A l) (and (IncidentL B l) (IncidentL C l))) *)
DecompEx H0 B.
(* Goal: @ex (@Couple (@Tpoint Tn)) (fun l : @Couple (@Tpoint Tn) => and (IncidentL A l) (and (IncidentL A l) (IncidentL A l))) *)
(* Goal: @ex (@Couple (@Tpoint Tn)) (fun l : @Couple (@Tpoint Tn) => and (IncidentL A l) (and (IncidentL A l) (IncidentL C l))) *)
(* Goal: @ex (@Couple (@Tpoint Tn)) (fun l : @Couple (@Tpoint Tn) => and (IncidentL A l) (and (IncidentL B l) (IncidentL C l))) *)
exists (Lin A B H1).
(* Goal: @CongA Tn A B C A' B' C' *)
unfold IncidentL;intuition.
(* Goal: @ex (@Couple (@Tpoint Tn)) (fun l : @Couple (@Tpoint Tn) => and (IncidentL A l) (and (IncidentL A l) (IncidentL C l))) *)
(* Goal: @ex (@Couple (@Tpoint Tn)) (fun l : @Couple (@Tpoint Tn) => and (IncidentL A l) (and (IncidentL B l) (IncidentL C l))) *)
exists (Lin A C H0).
(* Goal: @CongA Tn A B C A' B' C' *)
unfold IncidentL;intuition.
(* Goal: @ex (@Couple (@Tpoint Tn)) (fun l : @Couple (@Tpoint Tn) => and (IncidentL A l) (and (IncidentL B l) (IncidentL C l))) *)
exists (Lin A B H0).
(* Goal: @CongA Tn A B C A' B' C' *)
unfold IncidentL;intuition.
Qed.

Lemma cols_coincide : forall A B C, Col A B C <-> Col_H A B C.
Proof.
(* Goal: forall (l : @Couple (@Tpoint Tn)) (P : @Tpoint Tn) (m1 m2 : @Couple (@Tpoint Tn)) (_ : not (@IncidentL Tn P l)) (_ : Para l m1) (_ : @IncidentL Tn P m1) (_ : Para l m2) (_ : @IncidentL Tn P m2), @EqL Tn m1 m2 *)
intros.
(* Goal: @Hilbert_euclidean_ID (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) Hilbert_euclidean_follows_from_Tarski_euclidean *)
split.
(* Goal: Col_H A x C *)
(* Goal: not (Between_H x A C) *)
(* Goal: @Cong Tn P Q A x *)
apply cols_coincide_2.
(* Goal: @Col Tn A B C *)
apply cols_coincide_1.
Qed.

Lemma ncols_coincide : forall A B C, ~ Col A B C <-> ~ Col_H A B C.
Proof.
(* Goal: forall (l : @Couple (@Tpoint Tn)) (P : @Tpoint Tn) (m1 m2 : @Couple (@Tpoint Tn)) (_ : not (@IncidentL Tn P l)) (_ : Para l m1) (_ : @IncidentL Tn P m1) (_ : Para l m2) (_ : @IncidentL Tn P m2), @EqL Tn m1 m2 *)
intros.
(* Goal: iff (not (@Col Tn A B C)) (not (Col_H A B C)) *)
split; intros HNCol HCol; apply HNCol, cols_coincide, HCol.
Qed.

(** There exists three non collinear points. *)

Lemma lower_dim' : PA <> PB /\ PB <> PC /\ PA <> PC /\ ~ Col_H PA PB PC.
Proof.
(* Goal: and (not (@eq (@Tpoint Tn) (@PA Tn) (@PB Tn))) (and (not (@eq (@Tpoint Tn) (@PB Tn) (@PC Tn))) (and (not (@eq (@Tpoint Tn) (@PA Tn) (@PC Tn))) (not (Col_H (@PA Tn) (@PB Tn) (@PC Tn))))) *)
assert (HNCol : ~ Col PA PB PC) by (apply lower_dim).
(* Goal: @CongA Tn A B C C B A *)
assert_diffs.
(* Goal: @Coplanar Tn A B C D *)
apply ncols_coincide in HNCol.
(* Goal: not (@eq (@Tpoint Tn) A P) *)
(* Goal: or (@Bet Tn P A B) (@Bet Tn P B A) *)
repeat split; auto.
Qed.

(** We need a notion of plane. *)

Record Plane := Plan {M1; M2; M3; NCol : ~ Col_H M1 M2 M3}.

Definition IncidentP := fun A p => Coplanar (M1 p) (M2 p) (M3 p) A.

(** For every triplet of non collinear points there is a plane containing them. *)

Lemma axiom_plane_existence : forall A B C, ~ Col_H A B C ->
  exists p, IncidentP A p /\ IncidentP B p /\ IncidentP C p.
Proof.
(* Goal: forall (A B C : @Tpoint Tn) (_ : not (Col_H A B C)), @ex Plane (fun p : Plane => and (IncidentP A p) (and (IncidentP B p) (IncidentP C p))) *)
intros A B C HNCol.
(* Goal: @ex Plane (fun p : Plane => and (IncidentP A p) (and (IncidentP B p) (and (IncidentP C p) (IncidentP D p)))) *)
exists (Plan A B C HNCol).
(* Goal: and (IncidentP A (Plan A B C HNCol)) (and (IncidentP B (Plan A B C HNCol)) (and (IncidentP C (Plan A B C HNCol)) (IncidentP D (Plan A B C HNCol)))) *)
unfold IncidentP; simpl; repeat split; Cop.
Qed.

(** We need a notion of equality over planes. *)

Definition EqP : relation Plane := fun p q => forall X, IncidentP X p <-> IncidentP X q.

Infix "=p=" := EqP (at level 70):type_scope.

Lemma incidentp_eqp : forall A B C p, forall H : ~ Col_H A B C,
 IncidentP A p -> IncidentP B p -> IncidentP C p ->
 (Plan A B C H) =p= p.
Proof.
(* Goal: forall (A B C : @Tpoint Tn) (p : Plane) (H : not (Col_H A B C)) (_ : IncidentP A p) (_ : IncidentP B p) (_ : IncidentP C p), EqP (Plan A B C H) p *)
intros A B C p HNCol HA HB HC X.
(* Goal: iff (IncidentP X (Plan A B C HNCol)) (IncidentP X p) *)
unfold IncidentP in *; simpl.
(* Goal: iff (@Coplanar Tn A B C X) (@Coplanar Tn (M1 p) (M2 p) (M3 p) X) *)
assert (Hp := NCol p).
(* Goal: iff (@Coplanar Tn A B C X) (@Coplanar Tn (M1 p) (M2 p) (M3 p) X) *)
apply ncols_coincide in Hp.
(* Goal: @Coplanar Tn A B C D *)
apply ncols_coincide in HNCol.
split; intro; [apply coplanar_pseudo_trans with A B C; trivial|];
apply coplanar_pseudo_trans with (M1 p) (M2 p) (M3 p); Cop.
Qed.

(** Our equality is an equivalence relation. *)

Lemma eqp_transitivity : forall p q r, p =p= q -> q =p= r -> p =p= r.
Proof.
(* Goal: forall (p q r : Plane) (_ : EqP p q) (_ : EqP q r), EqP p r *)
intros p q r H1 H2 X.
(* Goal: iff (IncidentP X p) (IncidentP X r) *)
rewrite (H1 X); apply H2.
Qed.

Lemma eqp_reflexivity : forall p, p =p= p.
Proof.
(* Goal: forall (l : @Couple (@Tpoint Tn)) (P : @Tpoint Tn) (m1 m2 : @Couple (@Tpoint Tn)) (_ : not (@IncidentL Tn P l)) (_ : Para l m1) (_ : @IncidentL Tn P m1) (_ : Para l m2) (_ : @IncidentL Tn P m2), @EqL Tn m1 m2 *)
intros.
(* Goal: forall (p q : Plane) (_ : EqP p q), EqP q p *)
unfold EqP.
(* Goal: @CongA Tn A B C A' B' C' *)
intuition.
Qed.

Lemma eqp_symmetry : forall p q, p =p= q -> q =p= p.
Proof.
(* Goal: forall (p q : Plane) (_ : EqP p q), EqP q p *)
unfold EqP.
(* Goal: forall (p q : Plane) (_ : forall X : @Tpoint Tn, iff (IncidentP X p) (IncidentP X q)) (X : @Tpoint Tn), iff (IncidentP X q) (IncidentP X p) *)
intros p q H X.
(* Goal: iff (IncidentP X q) (IncidentP X p) *)
assert (T := H X).
(* Goal: @CongA Tn A B C A' B' C' *)
intuition.
Qed.

(** * Group II Order *)
Instance EqP_Equiv : Equivalence EqP.
Proof.
(* Goal: @Hilbert_euclidean_ID (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) Hilbert_euclidean_follows_from_Tarski_euclidean *)
split.
(* Goal: @Reflexive Plane EqP *)
(* Goal: @Symmetric Plane EqP *)
(* Goal: @Transitive Plane EqP *)
unfold Reflexive.
(* Goal: forall x : Plane, EqP x x *)
(* Goal: @Symmetric Plane EqP *)
(* Goal: @Transitive Plane EqP *)
apply eqp_reflexivity.
(* Goal: @Symmetric Plane EqP *)
(* Goal: @Transitive Plane EqP *)
unfold Symmetric.
(* Goal: forall (x y : Plane) (_ : EqP x y), EqP y x *)
(* Goal: @Transitive Plane EqP *)
apply eqp_symmetry.
(* Goal: @Transitive Plane EqP *)
unfold Transitive.
(* Goal: forall (x y z : Plane) (_ : EqP x y) (_ : EqP y z), EqP x z *)
apply eqp_transitivity.
Defined.


(** The equality is compatible with IncidentL *)

Lemma eqp_incidentp : forall A p q, p =p= q ->
 (IncidentP A p <-> IncidentP A q).
Proof.
(* Goal: forall (A : @Tpoint Tn) (p q : Plane) (_ : EqP p q), iff (IncidentP A p) (IncidentP A q) *)
intros A p q H.
(* Goal: iff (IncidentP A p) (IncidentP A q) *)
exact (H A).
Qed.

Instance incidentp_Proper (A:Tpoint) :
Proper (EqP ==>iff) (IncidentP A).
Proof.
(* Goal: @Proper (forall _ : Plane, Prop) (@respectful Plane Prop EqP iff) (IncidentP A) *)
intros a b H.
(* Goal: iff (IncidentP A a) (IncidentP A b) *)
apply eqp_incidentp.
(* Goal: @OS Tn (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l) A B *)
assumption.
Defined.

Lemma axiom_Incidp_morphism :
 forall M p q, IncidentP M p -> EqP p q -> IncidentP M q.
Proof.
(* Goal: forall (M : @Tpoint Tn) (p q : Plane) (_ : IncidentP M p) (_ : EqP p q), IncidentP M q *)
intros M p q Hp H.
(* Goal: IncidentP M q *)
destruct (eqp_incidentp M p q H).
(* Goal: @CongA Tn A B C A' B' C' *)
intuition.
Qed.

Lemma axiom_Incidp_dec : forall M p, IncidentP M p \/ ~ IncidentP M p.
Proof.
(* Goal: forall (l : @Couple (@Tpoint Tn)) (P : @Tpoint Tn) (m1 m2 : @Couple (@Tpoint Tn)) (_ : not (@IncidentL Tn P l)) (_ : Para l m1) (_ : @IncidentL Tn P m1) (_ : Para l m2) (_ : @IncidentL Tn P m2), @EqL Tn m1 m2 *)
intros.
(* Goal: or (IncidentP M p) (not (IncidentP M p)) *)
apply cop_dec.
Qed.

(** There is only one plane going through three non collinear points. *)

Lemma axiom_plane_uniqueness : forall A B C p q, ~ Col_H A B C ->
 IncidentP A p -> IncidentP B p -> IncidentP C p ->
 IncidentP A q -> IncidentP B q -> IncidentP C q ->
 p =p= q.
Proof.
(* Goal: forall (l : @Couple (@Tpoint Tn)) (P : @Tpoint Tn) (m1 m2 : @Couple (@Tpoint Tn)) (_ : not (@IncidentL Tn P l)) (_ : Para l m1) (_ : @IncidentL Tn P m1) (_ : Para l m2) (_ : @IncidentL Tn P m2), @EqL Tn m1 m2 *)
intros A B C p q H; intros.
(* Goal: EqP p q *)
assert (Heq : (Plan A B C H) =p= p).
(* Goal: @OS Tn (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l) A B *)
apply incidentp_eqp;assumption.
(* Goal: EqP p q *)
assert ((Plan A B C H) =p= q).
(* Goal: @OS Tn (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l) A B *)
apply incidentp_eqp;assumption.
(* Goal: IncidentP X p *)
rewrite <- Heq.
(* Goal: @OS Tn (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l) A B *)
assumption.
Qed.

(** Every plane contains at least one point. *)

Lemma axiom_one_point_on_plane : forall p,
  { A | IncidentP A p }.
Proof.
(* Goal: forall p : Plane, @sig (@Tpoint Tn) (fun A : @Tpoint Tn => IncidentP A p) *)
intro p.
(* Goal: @sig (@Tpoint Tn) (fun A : @Tpoint Tn => IncidentP A p) *)
exists (M1 p).
(* Goal: IncidentP (M1 p) p *)
unfold IncidentP; Cop.
Qed.

(** Definition of a line belonging to a plane.
  We say that a line belongs to a plane if every point of the line belongs to the plane. *)

Definition  IncidentLP := fun l p => forall A, IncidentL A l -> IncidentP A p.

(** If two distinct points of a line belong to a plane, then the line belongs to the plane. *)

Lemma axiom_line_on_plane : forall A B l p, A <> B ->
 IncidentL A l -> IncidentL B l -> IncidentP A p -> IncidentP B p ->
 IncidentLP l p.
Proof.
(* Goal: forall (A B : @Tpoint Tn) (l : @Couple (@Tpoint Tn)) (p : Plane) (_ : not (@eq (@Tpoint Tn) A B)) (_ : IncidentL A l) (_ : IncidentL B l) (_ : IncidentP A p) (_ : IncidentP B p), IncidentLP l p *)
intros A B l p HAB HAl HBl HAp HBp X HXl.
(* Goal: IncidentP X p *)
destruct (ex_ncol_cop (M1 p) (M2 p) (M3 p) A B HAB) as [C [HCp HNCol]].
(* Goal: @Coplanar Tn A B C D *)
apply ncols_coincide in HNCol.
(* Goal: IncidentP X p *)
assert (Heq : (Plan A B C HNCol) =p= p).
(* Goal: not (@eq (@Tpoint Tn) A P) *)
(* Goal: or (@Bet Tn P A B) (@Bet Tn P B A) *)
apply incidentp_eqp; auto.
(* Goal: IncidentP X p *)
rewrite <- Heq.
(* Goal: IncidentP X (Plan A B C HNCol) *)
unfold IncidentP; simpl.
(* Goal: @Hilbert_euclidean_ID (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) Hilbert_euclidean_follows_from_Tarski_euclidean *)
exists X; left; split.
(* Goal: @OS Tn (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l) A B *)
apply cols_coincide_1; exists l; repeat split; assumption.
(* Goal: @Col Tn P O X *)
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@CongA Tn A B C X O Y) (same_side' P Y O X)) *)
Col.
Qed.

(** * Group II Order *)

(** Definition of the Between predicate of Hilbert.
    Note that it is different from the Between of Tarski.
    The Between of Hilbert is strict. *)

Definition Between_H := fun A B C =>
  Bet A B C /\ A <> B /\ B <> C /\ A <> C.

Lemma axiom_between_col :
 forall A B C, Between_H A B C -> Col_H A B C.
Proof.
(* Goal: forall (l : @Couple (@Tpoint Tn)) (P : @Tpoint Tn) (m1 m2 : @Couple (@Tpoint Tn)) (_ : not (@IncidentL Tn P l)) (_ : Para l m1) (_ : @IncidentL Tn P m1) (_ : Para l m2) (_ : @IncidentL Tn P m2), @EqL Tn m1 m2 *)
intros.
(* Goal: Col_H A B C *)
unfold Col_H, Between_H in *.
(* Goal: @ex (@Couple (@Tpoint Tn)) (fun l : @Couple (@Tpoint Tn) => and (IncidentL A l) (and (IncidentL B l) (IncidentL C l))) *)
DecompAndAll.
(* Goal: @ex (@Couple (@Tpoint Tn)) (fun l : @Couple (@Tpoint Tn) => and (IncidentL A l) (and (IncidentL B l) (IncidentL C l))) *)
exists (Lin A B H2).
(* Goal: forall (M : @Tpoint Tn) (l : @Couple (@Tpoint Tn)) (_ : @Col Tn M (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l)), IncidentL M l *)
unfold IncidentL.
(* Goal: @CongA Tn A B C A' B' C' *)
intuition.
Qed.

Lemma axiom_between_diff :
 forall A B C, Between_H A B C -> A<>C.
Proof.
(* Goal: forall (l : @Couple (@Tpoint Tn)) (P : @Tpoint Tn) (m1 m2 : @Couple (@Tpoint Tn)) (_ : not (@IncidentL Tn P l)) (_ : Para l m1) (_ : @IncidentL Tn P m1) (_ : Para l m2) (_ : @IncidentL Tn P m2), @EqL Tn m1 m2 *)
intros.
(* Goal: and (@Col Tn T (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l)) (@Bet Tn A T B) *)
(* Goal: forall _ : and (not (@Col Tn A (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l))) (and (not (@Col Tn B (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l))) (@ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l)) (@Bet Tn A T B)))), and (not (IncidentL A l)) (and (not (IncidentL B l)) (@ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (IncidentL I l) (Between_H A I B)))) *)
unfold Between_H in *.
(* Goal: @CongA Tn A B C A' B' C' *)
intuition.
Qed.

(** If B is between A and C, it is also between C and A. *)

Lemma axiom_between_comm : forall A B C, Between_H A B C -> Between_H C B A.
Proof.
(* Goal: Between_H A B C *)
unfold Between_H in |- *.
(* Goal: forall (l : @Couple (@Tpoint Tn)) (P : @Tpoint Tn) (m1 m2 : @Couple (@Tpoint Tn)) (_ : not (@IncidentL Tn P l)) (_ : Para l m1) (_ : @IncidentL Tn P m1) (_ : Para l m2) (_ : @IncidentL Tn P m2), @EqL Tn m1 m2 *)
intros.
(* Goal: @CongA Tn A B C A' B' C' *)
intuition.
Qed.



Lemma axiom_between_out :
 forall A B, A <> B -> exists C, Between_H A B C.
Proof.
(* Goal: forall (l : @Couple (@Tpoint Tn)) (P : @Tpoint Tn) (m1 m2 : @Couple (@Tpoint Tn)) (_ : not (@IncidentL Tn P l)) (_ : Para l m1) (_ : @IncidentL Tn P m1) (_ : Para l m2) (_ : @IncidentL Tn P m2), @EqL Tn m1 m2 *)
intros.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => Between_H A B C) *)
prolong A B C A B.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => not (@Col Tn C (@P1 (@Tpoint Tn) (Lin A B HH)) (@P2 (@Tpoint Tn) (Lin A B HH)))) *)
exists C.
(* Goal: Between_H A B C *)
unfold Between_H.
repeat split;
auto;
intro;
treat_equalities;
(* Goal: not (@eq (@Tpoint Tn) A P) *)
(* Goal: or (@Bet Tn P A B) (@Bet Tn P B A) *)
tauto.
Qed.

Lemma axiom_between_only_one :
 forall A B C,
 Between_H A B C -> ~ Between_H B C A.
Proof.
(* Goal: Between_H A B C *)
unfold Between_H in |- *.
(* Goal: forall (l : @Couple (@Tpoint Tn)) (P : @Tpoint Tn) (m1 m2 : @Couple (@Tpoint Tn)) (_ : not (@IncidentL Tn P l)) (_ : Para l m1) (_ : @IncidentL Tn P m1) (_ : Para l m2) (_ : @IncidentL Tn P m2), @EqL Tn m1 m2 *)
intros.
intro;
(* Goal: and (not (@eq (@Tpoint Tn) A P)) (and (not (@eq (@Tpoint Tn) B P)) (or (@Bet Tn P A B) (@Bet Tn P B A))) *)
spliter.
assert (B=C) by
 (apply (between_equality B C A);Between).
(* Goal: False *)
solve [intuition].
Qed.

Lemma between_one : forall A B C,
 A<>B -> A<>C -> B<>C -> Col A B C ->
 Between_H A B C \/ Between_H B C A \/ Between_H B A C.
Proof.
(* Goal: forall (l : @Couple (@Tpoint Tn)) (P : @Tpoint Tn) (m1 m2 : @Couple (@Tpoint Tn)) (_ : not (@IncidentL Tn P l)) (_ : Para l m1) (_ : @IncidentL Tn P m1) (_ : Para l m2) (_ : @IncidentL Tn P m2), @EqL Tn m1 m2 *)
intros.
(* Goal: or (Between_H A B C) (or (Between_H B C A) (Between_H B A C)) *)
unfold Col, Between_H in *.
(* Goal: or (and (@Bet Tn A B C) (and (not (@eq (@Tpoint Tn) A B)) (and (not (@eq (@Tpoint Tn) B C)) (not (@eq (@Tpoint Tn) A C))))) (or (and (@Bet Tn B C A) (and (not (@eq (@Tpoint Tn) B C)) (and (not (@eq (@Tpoint Tn) C A)) (not (@eq (@Tpoint Tn) B A))))) (and (@Bet Tn B A C) (and (not (@eq (@Tpoint Tn) B A)) (and (not (@eq (@Tpoint Tn) A C)) (not (@eq (@Tpoint Tn) B C)))))) *)
destruct H2 as [|[|]]; [left|right..]; Between.
Qed.


Lemma axiom_between_one : forall A B C,
 A<>B -> A<>C -> B<>C -> Col_H A B C ->
 Between_H A B C \/ Between_H B C A \/ Between_H B A C.
Proof.
(* Goal: forall (l : @Couple (@Tpoint Tn)) (P : @Tpoint Tn) (m1 m2 : @Couple (@Tpoint Tn)) (_ : not (@IncidentL Tn P l)) (_ : Para l m1) (_ : @IncidentL Tn P m1) (_ : Para l m2) (_ : @IncidentL Tn P m2), @EqL Tn m1 m2 *)
intros.
(* Goal: @OS Tn (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l) A B *)
apply between_one;try assumption.
(* Goal: @Col Tn A B C *)
apply cols_coincide_1.
(* Goal: @OS Tn (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l) A B *)
assumption.
Qed.

(** Axiom of Pasch, (Hilbert version). *)

(** First we define a predicate which means that the line l intersects the segment AB. *)

Definition cut := fun l A B =>
  ~ IncidentL A l /\ ~ IncidentL B l /\ exists I, IncidentL I l /\ Between_H A I B.

(** We show that this definition is equivalent to the predicate TS of Tarski. *)

Lemma cut_two_sides : forall l A B, cut l A B <-> TS (P1 l) (P2 l) A B.
Proof.
(* Goal: forall (l : @Couple (@Tpoint Tn)) (P : @Tpoint Tn) (m1 m2 : @Couple (@Tpoint Tn)) (_ : not (@IncidentL Tn P l)) (_ : Para l m1) (_ : @IncidentL Tn P m1) (_ : Para l m2) (_ : @IncidentL Tn P m2), @EqL Tn m1 m2 *)
intros.
(* Goal: and (cut l A P) (cut l B P) *)
unfold cut.
(* Goal: iff (and (not (IncidentL A l)) (and (not (IncidentL B l)) (@ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (IncidentL I l) (Between_H A I B))))) (@TS Tn (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l) A B) *)
unfold TS.
(* Goal: @Hilbert_euclidean_ID (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) Hilbert_euclidean_follows_from_Tarski_euclidean *)
split.
(* Goal: forall (l : @Couple (@Tpoint Tn)) (P : @Tpoint Tn) (m1 m2 : @Couple (@Tpoint Tn)) (_ : not (@IncidentL Tn P l)) (_ : Para l m1) (_ : @IncidentL Tn P m1) (_ : Para l m2) (_ : @IncidentL Tn P m2), @EqL Tn m1 m2 *)
intros.
(* Goal: and (not (@eq (@Tpoint Tn) A P)) (and (not (@eq (@Tpoint Tn) B P)) (or (@Bet Tn P A B) (@Bet Tn P B A))) *)
spliter.
(* Goal: @CongA Tn A B C A' B' C' *)
repeat split; intuition.
(* Goal: and (not (IncidentL A l)) (and (not (IncidentL B l)) (@ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (IncidentL I l) (Between_H A I B)))) *)
ex_and H1 T.
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn I (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l)) (Between_H B I P)) *)
exists T.
(* Goal: and (@Col Tn T (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l)) (@Bet Tn A T B) *)
(* Goal: forall _ : and (not (@Col Tn A (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l))) (and (not (@Col Tn B (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l))) (@ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l)) (@Bet Tn A T B)))), and (not (IncidentL A l)) (and (not (IncidentL B l)) (@ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (IncidentL I l) (Between_H A I B)))) *)
unfold IncidentL in H1.
(* Goal: and (@Col Tn T (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l)) (@Bet Tn A T B) *)
(* Goal: forall _ : and (not (@Col Tn A (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l))) (and (not (@Col Tn B (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l))) (@ex (@Tpoint Tn) (fun T : @Tpoint Tn => and (@Col Tn T (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l)) (@Bet Tn A T B)))), and (not (IncidentL A l)) (and (not (IncidentL B l)) (@ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (IncidentL I l) (Between_H A I B)))) *)
unfold Between_H in *.
(* Goal: @CongA Tn A B C A' B' C' *)
intuition.

(* Goal: forall (l : @Couple (@Tpoint Tn)) (P : @Tpoint Tn) (m1 m2 : @Couple (@Tpoint Tn)) (_ : not (@IncidentL Tn P l)) (_ : Para l m1) (_ : @IncidentL Tn P m1) (_ : Para l m2) (_ : @IncidentL Tn P m2), @EqL Tn m1 m2 *)
intros.
(* Goal: and (not (@eq (@Tpoint Tn) A P)) (and (not (@eq (@Tpoint Tn) B P)) (or (@Bet Tn P A B) (@Bet Tn P B A))) *)
spliter.
(* Goal: and (not (IncidentL A l)) (and (not (IncidentL B l)) (@ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (IncidentL I l) (Between_H A I B)))) *)
ex_and H1 T.
(* Goal: forall (M : @Tpoint Tn) (l : @Couple (@Tpoint Tn)) (_ : @Col Tn M (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l)), IncidentL M l *)
unfold IncidentL.
(* Goal: @OS Tn (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l) A B *)
repeat split; try assumption.
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn I (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l)) (Between_H B I P)) *)
exists T.
(* Goal: @Hilbert_euclidean_ID (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) Hilbert_euclidean_follows_from_Tarski_euclidean *)
split.
(* Goal: @OS Tn (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l) A B *)
assumption.
(* Goal: Between_H A B C *)
unfold Between_H.
(* Goal: @Hilbert_euclidean_ID (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) Hilbert_euclidean_follows_from_Tarski_euclidean *)
repeat split.
(* Goal: @OS Tn (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l) A B *)
assumption.
(* Goal: not (@Col Tn X O P) *)
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@CongA Tn A B C X O Y) (same_side' P Y O X)) *)
intro.
(* Goal: False *)
subst.
(* Goal: False *)
contradiction.
(* Goal: not (@Col Tn X O P) *)
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@CongA Tn A B C X O Y) (same_side' P Y O X)) *)
intro.
(* Goal: False *)
subst.
(* Goal: False *)
contradiction.
(* Goal: not (@Col Tn X O P) *)
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@CongA Tn A B C X O Y) (same_side' P Y O X)) *)
intro.
(* Goal: False *)
treat_equalities.
(* Goal: False *)
contradiction.
Qed.

Lemma cop_plane_aux : forall A B C D, Coplanar A B C D -> A <> B ->
  exists p, IncidentP A p /\ IncidentP B p /\ IncidentP C p /\ IncidentP D p.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : @Coplanar Tn A B C D) (_ : not (@eq (@Tpoint Tn) A B)), @ex Plane (fun p : Plane => and (IncidentP A p) (and (IncidentP B p) (and (IncidentP C p) (IncidentP D p)))) *)
  intros A B C D HCop HAB.
(* Goal: @ex Plane (fun p : Plane => and (IncidentP A p) (and (IncidentP B p) (and (IncidentP C p) (IncidentP D p)))) *)
  destruct (col_dec A B C) as [|HNCol]; [destruct (col_dec A B D) as [|HNCol]|].
  - destruct (not_col_exists A B HAB) as [E HNCol].
(* Goal: @Coplanar Tn A B C D *)
    apply ncols_coincide in HNCol.
(* Goal: @ex Plane (fun p : Plane => and (IncidentP A p) (and (IncidentP B p) (and (IncidentP C p) (IncidentP D p)))) *)
    exists (Plan A B E HNCol).
(* Goal: and (IncidentP A (Plan A B C HNCol)) (and (IncidentP B (Plan A B C HNCol)) (and (IncidentP C (Plan A B C HNCol)) (IncidentP D (Plan A B C HNCol)))) *)
    unfold IncidentP; simpl; repeat split; Cop.
(* Goal: @Coplanar Tn A B C D *)
  - apply ncols_coincide in HNCol.
(* Goal: @ex Plane (fun p : Plane => and (IncidentP A p) (and (IncidentP B p) (and (IncidentP C p) (IncidentP D p)))) *)
    exists (Plan A B D HNCol).
(* Goal: and (IncidentP A (Plan A B C HNCol)) (and (IncidentP B (Plan A B C HNCol)) (and (IncidentP C (Plan A B C HNCol)) (IncidentP D (Plan A B C HNCol)))) *)
    unfold IncidentP; simpl; repeat split; Cop.
(* Goal: @Coplanar Tn A B C D *)
  - apply ncols_coincide in HNCol.
(* Goal: @ex Plane (fun p : Plane => and (IncidentP A p) (and (IncidentP B p) (and (IncidentP C p) (IncidentP D p)))) *)
    exists (Plan A B C HNCol).
(* Goal: and (IncidentP A (Plan A B C HNCol)) (and (IncidentP B (Plan A B C HNCol)) (and (IncidentP C (Plan A B C HNCol)) (IncidentP D (Plan A B C HNCol)))) *)
    unfold IncidentP; simpl; repeat split; Cop.
Qed.

Lemma cop_plane : forall A B C D, Coplanar A B C D ->
  exists p, IncidentP A p /\ IncidentP B p /\ IncidentP C p /\ IncidentP D p.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (_ : @Coplanar Tn A B C D), @ex Plane (fun p : Plane => and (IncidentP A p) (and (IncidentP B p) (and (IncidentP C p) (IncidentP D p)))) *)
  intros A B C D HCop.
  destruct (eq_dec_points A B) as [|HAB]; [destruct (eq_dec_points A C);
    [destruct (eq_dec_points A D)|]|].
  - destruct (another_point D) as [E].
(* Goal: @ex Plane (fun p : Plane => and (IncidentP A p) (and (IncidentP B p) (and (IncidentP C p) (IncidentP D p)))) *)
    destruct (cop_plane_aux D E E E) as [p []]; Cop.
(* Goal: @OS Tn (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l) A B *)
    subst; exists p; repeat split; assumption.
  - destruct (cop_plane_aux A D B C) as [p]; Cop.
(* Goal: @OS Tn (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l) A B *)
    spliter; exists p; repeat split; assumption.
  - destruct (cop_plane_aux A C B D) as [p]; Cop.
(* Goal: @OS Tn (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l) A B *)
    spliter; exists p; repeat split; assumption.
  - apply (cop_plane_aux A B C D HCop HAB).
Qed.

Lemma plane_cop: forall A B C D p,
  IncidentP A p -> IncidentP B p -> IncidentP C p -> IncidentP D p -> Coplanar A B C D.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (p : Plane) (_ : IncidentP A p) (_ : IncidentP B p) (_ : IncidentP C p) (_ : IncidentP D p), @Coplanar Tn A B C D *)
  unfold IncidentP.
(* Goal: forall (A B C D : @Tpoint Tn) (p : Plane) (_ : @Coplanar Tn (M1 p) (M2 p) (M3 p) A) (_ : @Coplanar Tn (M1 p) (M2 p) (M3 p) B) (_ : @Coplanar Tn (M1 p) (M2 p) (M3 p) C) (_ : @Coplanar Tn (M1 p) (M2 p) (M3 p) D), @Coplanar Tn A B C D *)
  intros A B C D p HA HB HC HD.
(* Goal: @Coplanar Tn A B C D *)
  assert (HNCol := NCol p).
(* Goal: @Coplanar Tn A B C D *)
  apply ncols_coincide in HNCol.
(* Goal: @OS Tn (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l) A B *)
  apply coplanar_pseudo_trans with (M1 p) (M2 p) (M3 p); assumption.
Qed.

Lemma axiom_pasch : forall A B C l p, ~ Col_H A B C ->
 IncidentP A p -> IncidentP B p -> IncidentP C p -> IncidentLP l p -> ~ IncidentL C l ->
 cut l A B -> cut l A C \/ cut l B C.
Proof.
(* Goal: forall (l : @Couple (@Tpoint Tn)) (P : @Tpoint Tn) (m1 m2 : @Couple (@Tpoint Tn)) (_ : not (@IncidentL Tn P l)) (_ : Para l m1) (_ : @IncidentL Tn P m1) (_ : Para l m2) (_ : @IncidentL Tn P m2), @EqL Tn m1 m2 *)
intros.
apply cut_two_sides in H5.
(* Goal: @CongA Tn A B C A' B' C' *)
assert(~Col A B C).
apply ncols_coincide.
(* Goal: @OS Tn (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l) A B *)
assumption.

assert(HH:=H5).
unfold TS in HH.
(* Goal: and (not (@eq (@Tpoint Tn) A P)) (and (not (@eq (@Tpoint Tn) B P)) (or (@Bet Tn P A B) (@Bet Tn P B A))) *)
spliter.

unfold IncidentL in H4.
assert (HCop : Coplanar (P1 l) (P2 l) A C).
(* Goal: @Col Tn P O X *)
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@CongA Tn A B C X O Y) (same_side' P Y O X)) *)
apply plane_cop with p; trivial; apply H3; unfold IncidentL; simpl; Col.

assert(HH:= cop__one_or_two_sides (P1 l)(P2 l) A C HCop H7 H4).

induction HH.
(* Goal: or (and (not (@eq (@Tpoint Tn) A B)) (and (not (@eq (@Tpoint Tn) C D)) (and (@Coplanar Tn A B C D) (not (@ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X A B) (@Col Tn X C D))))))) (and (not (@eq (@Tpoint Tn) A B)) (and (not (@eq (@Tpoint Tn) C D)) (and (@Col Tn A C D) (@Col Tn B C D)))) *)
left.
apply <-cut_two_sides.
(* Goal: @OS Tn (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l) A B *)
assumption.
right.
apply <-cut_two_sides.
apply l9_2.
eapply l9_8_2.
apply H5.
(* Goal: @OS Tn (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l) A B *)
assumption.
Qed.

Lemma Incid_line :
 forall P A B l, A<>B ->
 IncidentL A l -> IncidentL B l -> Col P A B -> IncidentL P l.
Proof.
(* Goal: forall (l : @Couple (@Tpoint Tn)) (P : @Tpoint Tn) (m1 m2 : @Couple (@Tpoint Tn)) (_ : not (@IncidentL Tn P l)) (_ : Para l m1) (_ : @IncidentL Tn P m1) (_ : Para l m2) (_ : @IncidentL Tn P m2), @EqL Tn m1 m2 *)
intros.
(* Goal: @OS Tn A B P Q *)
unfold IncidentL in *.
(* Goal: @Col Tn P (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l) *)
destruct l as [C D HCD].
(* Goal: @OS Tn A B P Q *)
simpl in *.
(* Goal: @Col Tn P C D *)
ColR.
Qed.




(** * Group IV Congruence *)

(** The cong predicate of Hilbert is the same as the one of Tarski: *)

Definition outH := fun P A B => Between_H P A B \/ Between_H P B A \/ (P <> A /\ A = B).

Lemma out_outH : forall P A B, Out P A B -> outH P A B.
(* Goal: forall (P A B : @Tpoint Tn) (_ : or (Between_H P A B) (or (Between_H P B A) (and (not (@eq (@Tpoint Tn) P A)) (@eq (@Tpoint Tn) A B)))), @Out Tn P A B *)
unfold Out.
(* Goal: forall (P A B : @Tpoint Tn) (_ : outH P A B), @Out Tn P A B *)
unfold outH.
(* Goal: forall (l : @Couple (@Tpoint Tn)) (P : @Tpoint Tn) (m1 m2 : @Couple (@Tpoint Tn)) (_ : not (@IncidentL Tn P l)) (_ : Para l m1) (_ : @IncidentL Tn P m1) (_ : Para l m2) (_ : @IncidentL Tn P m2), @EqL Tn m1 m2 *)
intros.
(* Goal: and (not (@eq (@Tpoint Tn) A P)) (and (not (@eq (@Tpoint Tn) B P)) (or (@Bet Tn P A B) (@Bet Tn P B A))) *)
spliter.
(* Goal: or (Between_H P A B) (or (Between_H P B A) (and (not (@eq (@Tpoint Tn) P A)) (@eq (@Tpoint Tn) A B))) *)
induction H1.

(* Goal: or (Between_H P A B) (or (Between_H P B A) (and (not (@eq (@Tpoint Tn) P A)) (@eq (@Tpoint Tn) A B))) *)
induction (eq_dec_points A B).
right; right.
(* Goal: not (@eq (@Tpoint Tn) A P) *)
(* Goal: or (@Bet Tn P A B) (@Bet Tn P B A) *)
split; auto.
(* Goal: or (and (not (@eq (@Tpoint Tn) A B)) (and (not (@eq (@Tpoint Tn) C D)) (and (@Coplanar Tn A B C D) (not (@ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X A B) (@Col Tn X C D))))))) (and (not (@eq (@Tpoint Tn) A B)) (and (not (@eq (@Tpoint Tn) C D)) (and (@Col Tn A C D) (@Col Tn B C D)))) *)
left.
(* Goal: Between_H A B C *)
unfold Between_H.
(* Goal: not (@eq (@Tpoint Tn) A P) *)
(* Goal: or (@Bet Tn P A B) (@Bet Tn P B A) *)
repeat split; auto.


(* Goal: or (Between_H P A B) (or (Between_H P B A) (and (not (@eq (@Tpoint Tn) P A)) (@eq (@Tpoint Tn) A B))) *)
induction (eq_dec_points A B).
right; right.
(* Goal: not (@eq (@Tpoint Tn) A P) *)
(* Goal: or (@Bet Tn P A B) (@Bet Tn P B A) *)
split; auto.
(* Goal: or (and (not (@eq (@Tpoint Tn) A B)) (and (not (@eq (@Tpoint Tn) C D)) (and (@Coplanar Tn A B C D) (not (@ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X A B) (@Col Tn X C D))))))) (and (not (@eq (@Tpoint Tn) A B)) (and (not (@eq (@Tpoint Tn) C D)) (and (@Col Tn A C D) (@Col Tn B C D)))) *)
right; left.
(* Goal: Between_H A B C *)
unfold Between_H.
(* Goal: not (@eq (@Tpoint Tn) A P) *)
(* Goal: or (@Bet Tn P A B) (@Bet Tn P B A) *)
repeat split; auto.
Qed.

Lemma axiom_hcong_1_existence : forall A B A' P l,
  A <> B -> A' <> P ->
  IncidentL A' l -> IncidentL P l ->
  exists B', IncidentL B' l /\ outH A' P B' /\ Cong A' B' A B.
Proof.
(* Goal: not (@eq (@Tpoint Tn) A P) *)
(* Goal: or (@Bet Tn P A B) (@Bet Tn P B A) *)
intros; destruct (l6_11_existence A' A B P) as [B' [HOut HCong]]; auto.
(* Goal: @OS Tn A B P Q *)
exists B'; repeat split; try apply out_outH, l6_6; auto; unfold IncidentL in *.
(* Goal: @Col Tn P C D *)
destruct l; simpl in *; ColR.
Qed.

Lemma axiom_hcong_1_uniqueness :
 forall A B l M A' B' A'' B'', A <> B -> IncidentL M l ->
  IncidentL A' l -> IncidentL B' l ->
  IncidentL A'' l -> IncidentL B'' l ->
  Between_H A' M B' -> Cong M A' A B ->
  Cong M B' A B -> Between_H A'' M B'' ->
  Cong M A'' A B -> Cong M B'' A B ->
  (A' = A'' /\ B' = B'') \/ (A' = B'' /\ B' = A'').
Proof.
(* Goal: Between_H A B C *)
unfold Between_H.
(* Goal: forall (M : @Tpoint Tn) (l : @Couple (@Tpoint Tn)) (_ : @Col Tn M (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l)), IncidentL M l *)
unfold IncidentL.
(* Goal: forall (l : @Couple (@Tpoint Tn)) (P : @Tpoint Tn) (m1 m2 : @Couple (@Tpoint Tn)) (_ : not (@IncidentL Tn P l)) (_ : Para l m1) (_ : @IncidentL Tn P m1) (_ : Para l m2) (_ : @IncidentL Tn P m2), @EqL Tn m1 m2 *)
intros.
(* Goal: and (not (@eq (@Tpoint Tn) A P)) (and (not (@eq (@Tpoint Tn) B P)) (or (@Bet Tn P A B) (@Bet Tn P B A))) *)
spliter.

assert(A' <> M /\ A'' <> M /\ B' <> M /\ B'' <> M /\ A' <> B' /\ A'' <> B'').
(* Goal: not (@eq (@Tpoint Tn) A P) *)
(* Goal: or (@Bet Tn P A B) (@Bet Tn P B A) *)
repeat split; intro; treat_equalities; tauto.
(* Goal: and (not (@eq (@Tpoint Tn) A P)) (and (not (@eq (@Tpoint Tn) B P)) (or (@Bet Tn P A B) (@Bet Tn P B A))) *)
spliter.

induction(out_dec M A' A'').
(* Goal: or (and (not (@eq (@Tpoint Tn) A B)) (and (not (@eq (@Tpoint Tn) C D)) (and (@Coplanar Tn A B C D) (not (@ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X A B) (@Col Tn X C D))))))) (and (not (@eq (@Tpoint Tn) A B)) (and (not (@eq (@Tpoint Tn) C D)) (and (@Col Tn A C D) (@Col Tn B C D)))) *)
left.
assert(A' = A'').
(* Goal: @OS Tn (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l) A B *)
eapply (l6_11_uniqueness M A B A''); try assumption.
apply out_trivial.
(* Goal: @OS Tn (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l) A B *)
assumption.

(* Goal: @Hilbert_euclidean_ID (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) Hilbert_euclidean_follows_from_Tarski_euclidean *)
split.
(* Goal: @OS Tn (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l) A B *)
assumption.
subst A''.

(* Goal: @OS Tn (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l) A B *)
eapply (l6_11_uniqueness M A B B''); try assumption.

(* Goal: forall (P A B : @Tpoint Tn) (_ : or (Between_H P A B) (or (Between_H P B A) (and (not (@eq (@Tpoint Tn) P A)) (@eq (@Tpoint Tn) A B)))), @Out Tn P A B *)
unfold Out.
(* Goal: @OS Tn (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l) A B *)
repeat split; try assumption.
eapply l5_2.
apply H18.
(* Goal: @OS Tn (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l) A B *)
assumption.
(* Goal: @OS Tn (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l) A B *)
assumption.
apply out_trivial.
(* Goal: @OS Tn (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l) A B *)
assumption.

right.
apply not_out_bet in H23.

assert(A' = B'').
(* Goal: @OS Tn (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l) A B *)
eapply (l6_11_uniqueness M A B A'); try assumption.
apply out_trivial.
(* Goal: @OS Tn (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l) A B *)
assumption.

(* Goal: forall (P A B : @Tpoint Tn) (_ : or (Between_H P A B) (or (Between_H P B A) (and (not (@eq (@Tpoint Tn) P A)) (@eq (@Tpoint Tn) A B)))), @Out Tn P A B *)
unfold Out.
(* Goal: @OS Tn (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l) A B *)
repeat split; try assumption.

eapply l5_2.
apply H18.
(* Goal: @OS Tn (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l) A B *)
assumption.
(* Goal: @Bet Tn C A x *)
(* Goal: False *)
(* Goal: @Cong Tn P Q A x *)
apply between_symmetry.
(* Goal: @OS Tn (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l) A B *)
assumption.

(* Goal: @Hilbert_euclidean_ID (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) Hilbert_euclidean_follows_from_Tarski_euclidean *)
split.
(* Goal: @OS Tn (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l) A B *)
assumption.

subst B''.
(* Goal: @OS Tn (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l) A B *)
eapply (l6_11_uniqueness M A B B'); try assumption.
apply out_trivial.
(* Goal: @OS Tn (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l) A B *)
assumption.
(* Goal: forall (P A B : @Tpoint Tn) (_ : or (Between_H P A B) (or (Between_H P B A) (and (not (@eq (@Tpoint Tn) P A)) (@eq (@Tpoint Tn) A B)))), @Out Tn P A B *)
unfold Out.
(* Goal: @OS Tn (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l) A B *)
repeat split; try assumption.
eapply l5_2.
apply H20.
(* Goal: @Bet Tn C A x *)
(* Goal: False *)
(* Goal: @Cong Tn P Q A x *)
apply between_symmetry.
(* Goal: @OS Tn (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l) A B *)
assumption.
(* Goal: @OS Tn (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l) A B *)
assumption.
eapply col3.
apply (Cond l).
(* Goal: @Col Tn P O X *)
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@CongA Tn A B C X O Y) (same_side' P Y O X)) *)
Col.
(* Goal: @Col Tn P O X *)
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@CongA Tn A B C X O Y) (same_side' P Y O X)) *)
Col.
(* Goal: @Col Tn P O X *)
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@CongA Tn A B C X O Y) (same_side' P Y O X)) *)
Col.
Qed.

(** As a remark we also prove another version of this axiom as formalized in Isabelle by
Phil Scott. *)

Definition same_side_scott := fun E A B => E <> A /\ E <> B /\ Col_H E A B /\ ~ Between_H A E B.

Remark axiom_hcong_scott:
 forall P Q A C, A <> C -> P <> Q ->
  exists B, same_side_scott A B C  /\ Cong P Q A B.
Proof.
(* Goal: forall (l : @Couple (@Tpoint Tn)) (P : @Tpoint Tn) (m1 m2 : @Couple (@Tpoint Tn)) (_ : not (@IncidentL Tn P l)) (_ : Para l m1) (_ : @IncidentL Tn P m1) (_ : Para l m2) (_ : @IncidentL Tn P m2), @EqL Tn m1 m2 *)
intros.
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (same_side_scott A B C) (@Cong Tn P Q A B)) *)
unfold same_side_scott.
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (and (not (@eq (@Tpoint Tn) A B)) (and (not (@eq (@Tpoint Tn) A C)) (and (Col_H A B C) (not (Between_H B A C))))) (@Cong Tn P Q A B)) *)
assert (exists X : Tpoint, Out A X C /\ Cong A X P Q).
(* Goal: not (@eq (@Tpoint Tn) A P) *)
(* Goal: or (@Bet Tn P A B) (@Bet Tn P B A) *)
apply l6_11_existence;auto.
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (and (not (@eq (@Tpoint Tn) A B)) (and (not (@eq (@Tpoint Tn) A C)) (and (Col_H A B C) (not (Between_H B A C))))) (@Cong Tn P Q A B)) *)
decompose [ex and] H1;clear H1.
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (and (not (@eq (@Tpoint Tn) A B)) (and (not (@eq (@Tpoint Tn) A C)) (and (Col_H A B C) (not (Between_H B A C))))) (@Cong Tn P Q A B)) *)
exists x.
(* Goal: @Hilbert_euclidean_ID (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) Hilbert_euclidean_follows_from_Tarski_euclidean *)
repeat split.
(* Goal: not (Between_H x A C) *)
(* Goal: @Cong Tn P Q A x *)
unfold Out in H3.
(* Goal: @CongA Tn A B C A' B' C' *)
intuition.
(* Goal: not (Between_H x A C) *)
(* Goal: @Cong Tn P Q A x *)
unfold Out in H3.
(* Goal: @CongA Tn A B C A' B' C' *)
intuition.
(* Goal: Col_H A x C *)
(* Goal: not (Between_H x A C) *)
(* Goal: @Cong Tn P Q A x *)
apply cols_coincide_2.
(* Goal: @OS Tn (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l) A B *)
apply out_col;assumption.


(* Goal: not (Between_H x A C) *)
(* Goal: @Cong Tn P Q A x *)
unfold Out in H3.
(* Goal: Between_H A B C *)
unfold Between_H.
(* Goal: not (@Col Tn X O P) *)
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@CongA Tn A B C X O Y) (same_side' P Y O X)) *)
intro.
(* Goal: False *)
(* Goal: @Cong Tn P Q A x *)
decompose [and] H3;clear H3.
(* Goal: False *)
(* Goal: @Cong Tn P Q A x *)
decompose [and] H1;clear H1.
(* Goal: False *)
(* Goal: @Cong Tn P Q A x *)
clear H8.
(* Goal: False *)
(* Goal: @Cong Tn P Q A x *)
destruct H7.
(* Goal: False *)
(* Goal: False *)
(* Goal: @Cong Tn P Q A x *)
assert (A = x).
(* Goal: not (@eq (@Tpoint Tn) A P) *)
(* Goal: or (@Bet Tn P A B) (@Bet Tn P B A) *)
eapply between_equality;eauto.
(* Goal: @CongA Tn A B C A' B' C' *)
intuition.
(* Goal: False *)
(* Goal: @Cong Tn P Q A x *)
assert (A = C).
(* Goal: not (@eq (@Tpoint Tn) A P) *)
(* Goal: or (@Bet Tn P A B) (@Bet Tn P B A) *)
eapply between_equality;eauto.
(* Goal: @Bet Tn C A x *)
(* Goal: False *)
(* Goal: @Cong Tn P Q A x *)
apply between_symmetry.
(* Goal: not (@eq (@Tpoint Tn) A P) *)
(* Goal: or (@Bet Tn P A B) (@Bet Tn P B A) *)
auto.
(* Goal: @CongA Tn A B C A' B' C' *)
intuition.
(* Goal: @Cong Tn P Q A x *)
Cong.
Qed.

(** We define when two segments do not intersect. *)

Definition disjoint := fun A B C D => ~ exists P, Between_H A P B /\ Between_H C P D.

(** Note that two disjoint segments may share one of their extremities. *)

Lemma col_disjoint_bet : forall A B C, Col_H A B C -> disjoint A B B C -> Bet A B C.
Proof.
(* Goal: forall (l : @Couple (@Tpoint Tn)) (P : @Tpoint Tn) (m1 m2 : @Couple (@Tpoint Tn)) (_ : not (@IncidentL Tn P l)) (_ : Para l m1) (_ : @IncidentL Tn P m1) (_ : Para l m2) (_ : @IncidentL Tn P m2), @EqL Tn m1 m2 *)
intros.
apply cols_coincide_1 in H.
unfold disjoint in H0.

(* Goal: or (Between_H P A B) (or (Between_H P B A) (and (not (@eq (@Tpoint Tn) P A)) (@eq (@Tpoint Tn) A B))) *)
induction (eq_dec_points A B).
subst  B.
apply between_trivial2.
induction (eq_dec_points B C).
subst  C.
(* Goal: @Bet Tn P A A *)
apply between_trivial.

unfold Col in H.
(* Goal: and (not (@eq (@Tpoint Tn) A P)) (and (not (@eq (@Tpoint Tn) B P)) (or (@Bet Tn P A B) (@Bet Tn P B A))) *)
induction H.
(* Goal: @OS Tn (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l) A B *)
assumption.

(* Goal: and (not (@eq (@Tpoint Tn) A P)) (and (not (@eq (@Tpoint Tn) B P)) (or (@Bet Tn P A B) (@Bet Tn P B A))) *)
induction H.
apply False_ind.
apply H0.
assert(exists M, Midpoint M B C) by(apply midpoint_existence).
ex_and H3 M.
exists M.
unfold Midpoint in H4.
(* Goal: and (not (@eq (@Tpoint Tn) A P)) (and (not (@eq (@Tpoint Tn) B P)) (or (@Bet Tn P A B) (@Bet Tn P B A))) *)
spliter.
(* Goal: @Hilbert_euclidean_ID (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) Hilbert_euclidean_follows_from_Tarski_euclidean *)
split.
(* Goal: Between_H A B C *)
unfold Between_H.
(* Goal: @Hilbert_euclidean_ID (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) Hilbert_euclidean_follows_from_Tarski_euclidean *)
repeat split.
(* Goal: @Bet Tn C A x *)
(* Goal: False *)
(* Goal: @Cong Tn P Q A x *)
apply between_symmetry.
eapply between_exchange4.
apply H3.
(* Goal: @OS Tn (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l) A B *)
assumption.
(* Goal: not (@Col Tn X O P) *)
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@CongA Tn A B C X O Y) (same_side' P Y O X)) *)
intro.
(* Goal: False *)
treat_equalities.
(*
apply between_symmetry in H.
apply between_equality in H.
(* Goal: False *)
treat_equalities.
*)
(* Goal: not (@eq (@Tpoint Tn) A P) *)
(* Goal: or (@Bet Tn P A B) (@Bet Tn P B A) *)
tauto.
(*
(* Goal: @Bet Tn C A x *)
(* Goal: False *)
(* Goal: @Cong Tn P Q A x *)
apply between_symmetry.
(* Goal: @OS Tn (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l) A B *)
assumption.
*)
(* Goal: not (@Col Tn X O P) *)
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@CongA Tn A B C X O Y) (same_side' P Y O X)) *)
intro.
(* Goal: False *)
treat_equalities.
(* Goal: not (@eq (@Tpoint Tn) A P) *)
(* Goal: or (@Bet Tn P A B) (@Bet Tn P B A) *)
tauto.
(* Goal: @OS Tn (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l) A B *)
assumption.
(* Goal: Between_H A B C *)
unfold Between_H.
(* Goal: @Hilbert_euclidean_ID (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) Hilbert_euclidean_follows_from_Tarski_euclidean *)
repeat split.
(* Goal: @OS Tn (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l) A B *)
assumption.
(* Goal: not (@Col Tn X O P) *)
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@CongA Tn A B C X O Y) (same_side' P Y O X)) *)
intro.
(* Goal: False *)
treat_equalities.
(* Goal: not (@eq (@Tpoint Tn) A P) *)
(* Goal: or (@Bet Tn P A B) (@Bet Tn P B A) *)
tauto.
(* Goal: not (@Col Tn X O P) *)
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@CongA Tn A B C X O Y) (same_side' P Y O X)) *)
intro.
(* Goal: False *)
treat_equalities.
(* Goal: not (@eq (@Tpoint Tn) A P) *)
(* Goal: or (@Bet Tn P A B) (@Bet Tn P B A) *)
tauto.
(* Goal: @OS Tn (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l) A B *)
assumption.

apply False_ind.
apply H0.
assert(exists M, Midpoint M A B) by(apply midpoint_existence).
ex_and H3 M.
exists M.
unfold Midpoint in H4.
(* Goal: and (not (@eq (@Tpoint Tn) A P)) (and (not (@eq (@Tpoint Tn) B P)) (or (@Bet Tn P A B) (@Bet Tn P B A))) *)
spliter.
(* Goal: @Hilbert_euclidean_ID (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) Hilbert_euclidean_follows_from_Tarski_euclidean *)
split.
(* Goal: Between_H A B C *)
unfold Between_H.
(* Goal: @Hilbert_euclidean_ID (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) Hilbert_euclidean_follows_from_Tarski_euclidean *)
repeat split.
(* Goal: @OS Tn (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l) A B *)
assumption.
(* Goal: not (@Col Tn X O P) *)
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@CongA Tn A B C X O Y) (same_side' P Y O X)) *)
intro.
(* Goal: False *)
treat_equalities.
(* Goal: not (@eq (@Tpoint Tn) A P) *)
(* Goal: or (@Bet Tn P A B) (@Bet Tn P B A) *)
tauto.
(* Goal: not (@Col Tn X O P) *)
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@CongA Tn A B C X O Y) (same_side' P Y O X)) *)
intro.
(* Goal: False *)
treat_equalities.
(* Goal: not (@eq (@Tpoint Tn) A P) *)
(* Goal: or (@Bet Tn P A B) (@Bet Tn P B A) *)
tauto.
(* Goal: @OS Tn (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l) A B *)
assumption.

(* Goal: Between_H A B C *)
unfold Between_H.
(* Goal: @Hilbert_euclidean_ID (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) Hilbert_euclidean_follows_from_Tarski_euclidean *)
repeat split.

eapply between_exchange4.
(* Goal: @Bet Tn C A x *)
(* Goal: False *)
(* Goal: @Cong Tn P Q A x *)
apply between_symmetry.
apply H3.
(* Goal: @Bet Tn C A x *)
(* Goal: False *)
(* Goal: @Cong Tn P Q A x *)
apply between_symmetry.
(* Goal: @OS Tn (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l) A B *)
assumption.
(* Goal: not (@Col Tn X O P) *)
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@CongA Tn A B C X O Y) (same_side' P Y O X)) *)
intro.
(* Goal: False *)
treat_equalities.
(* Goal: not (@eq (@Tpoint Tn) A P) *)
(* Goal: or (@Bet Tn P A B) (@Bet Tn P B A) *)
tauto.
(* Goal: not (@Col Tn X O P) *)
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@CongA Tn A B C X O Y) (same_side' P Y O X)) *)
intro.
(* Goal: False *)
treat_equalities.
(* Goal: @CongA Tn A B C A' B' C' *)
intuition.
(* Goal: @OS Tn (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l) A B *)
assumption.
Qed.


Lemma axiom_hcong_3 : forall A B C A' B' C',
   Col_H A B C -> Col_H A' B' C' ->
  disjoint A B B C -> disjoint A' B' B' C' ->
  Cong A B A' B' -> Cong B C B' C' -> Cong A C A' C'.
Proof.
(* Goal: forall (l : @Couple (@Tpoint Tn)) (P : @Tpoint Tn) (m1 m2 : @Couple (@Tpoint Tn)) (_ : not (@IncidentL Tn P l)) (_ : Para l m1) (_ : @IncidentL Tn P m1) (_ : Para l m2) (_ : @IncidentL Tn P m2), @EqL Tn m1 m2 *)
intros.
(* Goal: @Cong Tn A C A' C' *)
assert(Bet A B C).
(* Goal: @Bet Tn A' B' C' *)
(* Goal: @Cong Tn A C A' C' *)
eapply col_disjoint_bet.
(* Goal: @OS Tn (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l) A B *)
assumption.
(* Goal: @OS Tn (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l) A B *)
assumption.

(* Goal: @Cong Tn A C A' C' *)
assert(Bet A' B' C').
(* Goal: @Bet Tn A' B' C' *)
(* Goal: @Cong Tn A C A' C' *)
eapply col_disjoint_bet.
(* Goal: @OS Tn (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l) A B *)
assumption.
(* Goal: @OS Tn (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l) A B *)
assumption.
(* Goal: not (@eq (@Tpoint Tn) A P) *)
(* Goal: or (@Bet Tn P A B) (@Bet Tn P B A) *)
eapply l2_11;eauto.
Qed.

Lemma exists_not_incident : forall A B : Tpoint, forall  HH : A <> B , exists C, ~ IncidentL C (Lin A B HH).
Proof.
(* Goal: forall (l : @Couple (@Tpoint Tn)) (P : @Tpoint Tn) (m1 m2 : @Couple (@Tpoint Tn)) (_ : not (@IncidentL Tn P l)) (_ : Para l m1) (_ : @IncidentL Tn P m1) (_ : Para l m2) (_ : @IncidentL Tn P m2), @EqL Tn m1 m2 *)
intros.
(* Goal: forall (M : @Tpoint Tn) (l : @Couple (@Tpoint Tn)) (_ : @Col Tn M (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l)), IncidentL M l *)
unfold IncidentL.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => not (@Col Tn C (@P1 (@Tpoint Tn) (Lin A B HH)) (@P2 (@Tpoint Tn) (Lin A B HH)))) *)
assert(HC:=not_col_exists A B HH).
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => not (@Col Tn C (@P1 (@Tpoint Tn) (Lin A B HH)) (@P2 (@Tpoint Tn) (Lin A B HH)))) *)
ex_and HC C.
(* Goal: @ex (@Tpoint Tn) (fun C : @Tpoint Tn => not (@Col Tn C (@P1 (@Tpoint Tn) (Lin A B HH)) (@P2 (@Tpoint Tn) (Lin A B HH)))) *)
exists C.
(* Goal: not (@Col Tn X O P) *)
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@CongA Tn A B C X O Y) (same_side' P Y O X)) *)
intro.
(* Goal: False *)
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@CongA Tn A B C X O Y) (same_side' P Y O X)) *)
apply H.
(* Goal: @Col Tn A B C *)
simpl in H0.
(* Goal: @Col Tn P O X *)
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@CongA Tn A B C X O Y) (same_side' P Y O X)) *)
Col.
Qed.

Definition same_side := fun A B l => exists P, cut l A P /\ cut l B P.

(** Same side predicate corresponds to OS of Tarski. *)

Lemma same_side_one_side : forall A B l, same_side A B l -> OS (P1 l) (P2 l) A B.
Proof.
(* Goal: same_side A B l *)
unfold same_side.
(* Goal: forall (l : @Couple (@Tpoint Tn)) (P : @Tpoint Tn) (m1 m2 : @Couple (@Tpoint Tn)) (_ : not (@IncidentL Tn P l)) (_ : Para l m1) (_ : @IncidentL Tn P m1) (_ : Para l m2) (_ : @IncidentL Tn P m2), @EqL Tn m1 m2 *)
intros.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (cut l A P) (cut l B P)) *)
destruct H as [P []].
apply cut_two_sides in H.
apply cut_two_sides in H0.
eapply l9_8_1.
(* Goal: False *)
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@CongA Tn A B C X O Y) (same_side' P Y O X)) *)
apply H.
apply H0.
Qed.



Lemma one_side_same_side : forall A B l, OS (P1 l) (P2 l) A B -> same_side A B l.
Proof.
(* Goal: forall (l : @Couple (@Tpoint Tn)) (P : @Tpoint Tn) (m1 m2 : @Couple (@Tpoint Tn)) (_ : not (@IncidentL Tn P l)) (_ : Para l m1) (_ : @IncidentL Tn P m1) (_ : Para l m2) (_ : @IncidentL Tn P m2), @EqL Tn m1 m2 *)
intros.
(* Goal: same_side A B l *)
unfold same_side.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (cut l A P) (cut l B P)) *)
unfold OS in H.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (cut l A P) (cut l B P)) *)
destruct H as [P []].
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => and (cut l A P) (cut l B P)) *)
exists P.
(* Goal: and (cut l A P) (cut l B P) *)
unfold cut.
(* Goal: forall (M : @Tpoint Tn) (l : @Couple (@Tpoint Tn)) (_ : @Col Tn M (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l)), IncidentL M l *)
unfold IncidentL.
(* Goal: and (and (not (@Col Tn A (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l))) (and (not (@Col Tn P (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l))) (@ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn I (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l)) (Between_H A I P))))) (and (not (@Col Tn B (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l))) (and (not (@Col Tn P (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l))) (@ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn I (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l)) (Between_H B I P))))) *)
unfold TS in H.
(* Goal: and (and (not (@Col Tn A (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l))) (and (not (@Col Tn P (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l))) (@ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn I (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l)) (Between_H A I P))))) (and (not (@Col Tn B (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l))) (and (not (@Col Tn P (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l))) (@ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn I (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l)) (Between_H B I P))))) *)
unfold TS in H0.
(* Goal: and (not (@eq (@Tpoint Tn) A P)) (and (not (@eq (@Tpoint Tn) B P)) (or (@Bet Tn P A B) (@Bet Tn P B A))) *)
spliter.
(* Goal: not (@eq (@Tpoint Tn) A P) *)
(* Goal: or (@Bet Tn P A B) (@Bet Tn P B A) *)
repeat split; auto.
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn I (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l)) (Between_H A I P)) *)
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn I (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l)) (Between_H B I P)) *)
ex_and H4 T.
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn I (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l)) (Between_H B I P)) *)
exists T.
(* Goal: Between_H A B C *)
unfold Between_H.
(* Goal: not (@eq (@Tpoint Tn) A P) *)
(* Goal: or (@Bet Tn P A B) (@Bet Tn P B A) *)
repeat split; auto.
(* Goal: not (@Col Tn X O P) *)
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@CongA Tn A B C X O Y) (same_side' P Y O X)) *)
intro.
(* Goal: False *)
subst T.
(* Goal: False *)
contradiction.
(* Goal: not (@Col Tn X O P) *)
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@CongA Tn A B C X O Y) (same_side' P Y O X)) *)
intro.
(* Goal: False *)
subst T.
(* Goal: False *)
contradiction.
(* Goal: not (@Col Tn X O P) *)
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@CongA Tn A B C X O Y) (same_side' P Y O X)) *)
intro.
(* Goal: False *)
subst P.
(* Goal: False *)
apply between_identity in H5.
(* Goal: False *)
subst T.
(* Goal: False *)
contradiction.
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn I (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l)) (Between_H B I P)) *)
ex_and H2 T.
(* Goal: @ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn I (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l)) (Between_H B I P)) *)
exists T.
(* Goal: Between_H A B C *)
unfold Between_H.
(* Goal: not (@eq (@Tpoint Tn) A P) *)
(* Goal: or (@Bet Tn P A B) (@Bet Tn P B A) *)
repeat split; auto.
(* Goal: not (@Col Tn X O P) *)
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@CongA Tn A B C X O Y) (same_side' P Y O X)) *)
intro.
(* Goal: False *)
subst T.
(* Goal: False *)
contradiction.
(* Goal: not (@Col Tn X O P) *)
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@CongA Tn A B C X O Y) (same_side' P Y O X)) *)
intro.
(* Goal: False *)
subst T.
(* Goal: False *)
contradiction.
(* Goal: not (@Col Tn X O P) *)
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@CongA Tn A B C X O Y) (same_side' P Y O X)) *)
intro.
(* Goal: False *)
subst P.
(* Goal: False *)
apply between_identity in H5.
(* Goal: False *)
subst T.
(* Goal: False *)
contradiction.
Qed.

Definition same_side' := fun A B X Y =>
  X <> Y /\ forall l, IncidentL X l -> IncidentL Y l -> same_side A B l.

Lemma OS_distinct : forall P Q A B,
  OS P Q A B -> P<>Q.
Proof.
(* Goal: forall (l : @Couple (@Tpoint Tn)) (P : @Tpoint Tn) (m1 m2 : @Couple (@Tpoint Tn)) (_ : not (@IncidentL Tn P l)) (_ : Para l m1) (_ : @IncidentL Tn P m1) (_ : Para l m2) (_ : @IncidentL Tn P m2), @EqL Tn m1 m2 *)
intros.
(* Goal: not (@eq (@Tpoint Tn) P Q) *)
apply one_side_not_col123 in H.
(* Goal: @OS Tn (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l) A B *)
assert_diffs;assumption.
Qed.


Lemma OS_same_side' :
 forall P Q A B, OS P Q A B -> same_side' A B P Q.
Proof.
(* Goal: forall (l : @Couple (@Tpoint Tn)) (P : @Tpoint Tn) (m1 m2 : @Couple (@Tpoint Tn)) (_ : not (@IncidentL Tn P l)) (_ : Para l m1) (_ : @IncidentL Tn P m1) (_ : Para l m2) (_ : @IncidentL Tn P m2), @EqL Tn m1 m2 *)
intros.
(* Goal: same_side' A B P Q *)
unfold same_side'.
(* Goal: forall (l : @Couple (@Tpoint Tn)) (P : @Tpoint Tn) (m1 m2 : @Couple (@Tpoint Tn)) (_ : not (@IncidentL Tn P l)) (_ : Para l m1) (_ : @IncidentL Tn P m1) (_ : Para l m2) (_ : @IncidentL Tn P m2), @EqL Tn m1 m2 *)
intros.
(* Goal: @Hilbert_euclidean_ID (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) Hilbert_euclidean_follows_from_Tarski_euclidean *)
split.
(* Goal: @OS Tn (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l) A B *)
apply OS_distinct with A B;assumption.
(* Goal: forall (l : @Couple (@Tpoint Tn)) (P : @Tpoint Tn) (m1 m2 : @Couple (@Tpoint Tn)) (_ : not (@IncidentL Tn P l)) (_ : Para l m1) (_ : @IncidentL Tn P m1) (_ : Para l m2) (_ : @IncidentL Tn P m2), @EqL Tn m1 m2 *)
intros.

apply  one_side_same_side.
(* Goal: @OS Tn (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l) A B *)
destruct l.
(* Goal: @OS Tn A B P Q *)
unfold IncidentL in *.
(* Goal: @OS Tn A B P Q *)
simpl in *.
(* Goal: @Col Tn P C D *)
apply col2_os__os with P Q; try assumption; ColR.
Qed.

Lemma same_side_OS :
 forall P Q A B, same_side' P Q A B -> OS A B P Q.
Proof.
(* Goal: forall (l : @Couple (@Tpoint Tn)) (P : @Tpoint Tn) (m1 m2 : @Couple (@Tpoint Tn)) (_ : not (@IncidentL Tn P l)) (_ : Para l m1) (_ : @IncidentL Tn P m1) (_ : Para l m2) (_ : @IncidentL Tn P m2), @EqL Tn m1 m2 *)
intros.
(* Goal: @OS Tn A B P Q *)
unfold same_side' in *.
(* Goal: @OS Tn A B P Q *)
destruct H.
(* Goal: @OS Tn A B P Q *)
destruct (axiom_line_existence A B H).
(* Goal: @OS Tn A B P Q *)
destruct H1.
(* Goal: @OS Tn A B P Q *)
assert (T:=H0 x H1 H2).
(* Goal: @OS Tn A B P Q *)
assert (U:=same_side_one_side P Q x T).
(* Goal: @OS Tn A B P Q *)
destruct x.
(* Goal: @OS Tn A B P Q *)
unfold IncidentL in *.
(* Goal: @OS Tn A B P Q *)
simpl in *.
(* Goal: @Col Tn P O X *)
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@CongA Tn A B C X O Y) (same_side' P Y O X)) *)
apply col2_os__os with P1 P2;Col.
Qed.

(** This is equivalent to the out predicate of Tarski. *)

Lemma outH_out : forall P A B, outH P A B -> Out P A B.
Proof.
(* Goal: forall (P A B : @Tpoint Tn) (_ : outH P A B), @Out Tn P A B *)
unfold outH.
(* Goal: forall (P A B : @Tpoint Tn) (_ : or (Between_H P A B) (or (Between_H P B A) (and (not (@eq (@Tpoint Tn) P A)) (@eq (@Tpoint Tn) A B)))), @Out Tn P A B *)
unfold Out.
(* Goal: forall (l : @Couple (@Tpoint Tn)) (P : @Tpoint Tn) (m1 m2 : @Couple (@Tpoint Tn)) (_ : not (@IncidentL Tn P l)) (_ : Para l m1) (_ : @IncidentL Tn P m1) (_ : Para l m2) (_ : @IncidentL Tn P m2), @EqL Tn m1 m2 *)
intros.
(* Goal: and (not (@eq (@Tpoint Tn) A P)) (and (not (@eq (@Tpoint Tn) B P)) (or (@Bet Tn P A B) (@Bet Tn P B A))) *)
induction H.
(* Goal: and (not (@eq (@Tpoint Tn) A P)) (and (not (@eq (@Tpoint Tn) B P)) (or (@Bet Tn P A B) (@Bet Tn P B A))) *)
(* Goal: and (not (@eq (@Tpoint Tn) A P)) (and (not (@eq (@Tpoint Tn) B P)) (or (@Bet Tn P A B) (@Bet Tn P B A))) *)
unfold Between_H in H.
(* Goal: and (not (@eq (@Tpoint Tn) A P)) (and (not (@eq (@Tpoint Tn) B P)) (or (@Bet Tn P A B) (@Bet Tn P B A))) *)
spliter.
(* Goal: not (@eq (@Tpoint Tn) A P) *)
(* Goal: or (@Bet Tn P A B) (@Bet Tn P B A) *)
repeat split; auto.
(* Goal: and (not (@eq (@Tpoint Tn) A P)) (and (not (@eq (@Tpoint Tn) B P)) (or (@Bet Tn P A B) (@Bet Tn P B A))) *)
induction H.
(* Goal: and (not (@eq (@Tpoint Tn) A P)) (and (not (@eq (@Tpoint Tn) B P)) (or (@Bet Tn P A B) (@Bet Tn P B A))) *)
(* Goal: and (not (@eq (@Tpoint Tn) A P)) (and (not (@eq (@Tpoint Tn) B P)) (or (@Bet Tn P A B) (@Bet Tn P B A))) *)
unfold Between_H in H.
(* Goal: and (not (@eq (@Tpoint Tn) A P)) (and (not (@eq (@Tpoint Tn) B P)) (or (@Bet Tn P A B) (@Bet Tn P B A))) *)
spliter.
(* Goal: not (@eq (@Tpoint Tn) A P) *)
(* Goal: or (@Bet Tn P A B) (@Bet Tn P B A) *)
repeat split; auto.
(* Goal: and (not (@eq (@Tpoint Tn) A P)) (and (not (@eq (@Tpoint Tn) B P)) (or (@Bet Tn P A B) (@Bet Tn P B A))) *)
spliter.
(* Goal: @Hilbert_euclidean_ID (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) Hilbert_euclidean_follows_from_Tarski_euclidean *)
repeat split.
(* Goal: not (@eq (@Tpoint Tn) A P) *)
(* Goal: or (@Bet Tn P A B) (@Bet Tn P B A) *)
auto.
(* Goal: or (@Bet Tn P A B) (@Bet Tn P B A) *)
subst B.
(* Goal: not (@eq (@Tpoint Tn) A P) *)
(* Goal: or (@Bet Tn P A B) (@Bet Tn P B A) *)
auto.
(* Goal: or (@Bet Tn P A B) (@Bet Tn P B A) *)
subst B.
(* Goal: or (and (not (@eq (@Tpoint Tn) A B)) (and (not (@eq (@Tpoint Tn) C D)) (and (@Coplanar Tn A B C D) (not (@ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X A B) (@Col Tn X C D))))))) (and (not (@eq (@Tpoint Tn) A B)) (and (not (@eq (@Tpoint Tn) C D)) (and (@Col Tn A C D) (@Col Tn B C D)))) *)
left.
(* Goal: @Bet Tn P A A *)
apply between_trivial.
Qed.

(** The 2D version of the fourth congruence axiom **)

Lemma incident_col : forall M l, IncidentL M l -> Col M (P1 l)(P2 l).
Proof.
(* Goal: forall (M : @Tpoint Tn) (l : @Couple (@Tpoint Tn)) (_ : @Col Tn M (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l)), IncidentL M l *)
unfold IncidentL.
(* Goal: forall (l : @Couple (@Tpoint Tn)) (P : @Tpoint Tn) (m1 m2 : @Couple (@Tpoint Tn)) (_ : not (@IncidentL Tn P l)) (_ : Para l m1) (_ : @IncidentL Tn P m1) (_ : Para l m2) (_ : @IncidentL Tn P m2), @EqL Tn m1 m2 *)
intros.
(* Goal: @OS Tn (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l) A B *)
assumption.
Qed.

Lemma col_incident : forall M l, Col M (P1 l)(P2 l) -> IncidentL M l.
Proof.
(* Goal: forall (M : @Tpoint Tn) (l : @Couple (@Tpoint Tn)) (_ : @Col Tn M (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l)), IncidentL M l *)
unfold IncidentL.
(* Goal: forall (l : @Couple (@Tpoint Tn)) (P : @Tpoint Tn) (m1 m2 : @Couple (@Tpoint Tn)) (_ : not (@IncidentL Tn P l)) (_ : Para l m1) (_ : @IncidentL Tn P m1) (_ : Para l m2) (_ : @IncidentL Tn P m2), @EqL Tn m1 m2 *)
intros.
(* Goal: @OS Tn (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l) A B *)
assumption.
Qed.

Lemma Bet_Between_H : forall A B C,
 Bet A B C -> A<>B -> B<>C -> Between_H A B C.
Proof.
(* Goal: forall (l : @Couple (@Tpoint Tn)) (P : @Tpoint Tn) (m1 m2 : @Couple (@Tpoint Tn)) (_ : not (@IncidentL Tn P l)) (_ : Para l m1) (_ : @IncidentL Tn P m1) (_ : Para l m2) (_ : @IncidentL Tn P m2), @EqL Tn m1 m2 *)
intros.
(* Goal: Between_H A B C *)
unfold Between_H.
(* Goal: @OS Tn (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l) A B *)
repeat split;try assumption.
(* Goal: not (@Col Tn X O P) *)
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@CongA Tn A B C X O Y) (same_side' P Y O X)) *)
intro.
(* Goal: False *)
subst.
(* Goal: False *)
treat_equalities.
(* Goal: @CongA Tn A B C A' B' C' *)
intuition.
Qed.

Lemma axiom_cong_5' : forall A B C A' B' C', ~ Col_H A B C -> ~ Col_H A' B' C' ->
           Cong A B A' B' -> Cong A C A' C' -> CongA B A C B' A' C' -> CongA A B C A' B' C'.
Proof.
(* Goal: forall (A B C A' B' C' : @Tpoint Tn) (_ : not (Col_H A B C)) (_ : not (Col_H A' B' C')) (_ : @Cong Tn A B A' B') (_ : @Cong Tn A C A' C') (_ : @CongA Tn B A C B' A' C'), @CongA Tn A B C A' B' C' *)
intros A B C A' B' C'.
(* Goal: forall (l : @Couple (@Tpoint Tn)) (P : @Tpoint Tn) (m1 m2 : @Couple (@Tpoint Tn)) (_ : not (@IncidentL Tn P l)) (_ : Para l m1) (_ : @IncidentL Tn P m1) (_ : Para l m2) (_ : @IncidentL Tn P m2), @EqL Tn m1 m2 *)
intros.
(* Goal: @CongA Tn A B C A' B' C' *)
assert (T:=l11_49 B A C B' A' C').
(* Goal: @CongA Tn A B C A' B' C' *)
assert (~ Col A B C).
(* Goal: not (@Col Tn X O P) *)
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@CongA Tn A B C X O Y) (same_side' P Y O X)) *)
intro.
(* Goal: False *)
(* Goal: @CongA Tn A B C A' B' C' *)
apply cols_coincide_2 in H4.
(* Goal: @CongA Tn A B C A' B' C' *)
intuition.
(* Goal: @CongA Tn A B C C B A *)
assert_diffs.
(* Goal: @CongA Tn A B C A' B' C' *)
intuition.
Qed.


Lemma axiom_hcong_4_existence :  forall A B C O X P,
   ~ Col_H P O X -> ~ Col_H A B C ->
  exists Y, CongA A B C X O Y  (* /\ ~Col O X Y *) /\ same_side' P Y O X.
Proof.
(* Goal: forall (l : @Couple (@Tpoint Tn)) (P : @Tpoint Tn) (m1 m2 : @Couple (@Tpoint Tn)) (_ : not (@IncidentL Tn P l)) (_ : Para l m1) (_ : @IncidentL Tn P m1) (_ : Para l m2) (_ : @IncidentL Tn P m2), @EqL Tn m1 m2 *)
intros.
rewrite <- cols_coincide in H.
rewrite <- cols_coincide in H0.

(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@CongA Tn A B C X O Y) (same_side' P Y O X)) *)
assert(~Col X O P).
(* Goal: not (@Col Tn X O P) *)
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@CongA Tn A B C X O Y) (same_side' P Y O X)) *)
intro.
(* Goal: False *)
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@CongA Tn A B C X O Y) (same_side' P Y O X)) *)
apply H.
(* Goal: @Col Tn P O X *)
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@CongA Tn A B C X O Y) (same_side' P Y O X)) *)
Col.
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@CongA Tn A B C X O Y) (same_side' P Y O X)) *)
assert(HH:=angle_construction_1 A B C X O P H0 H1).

(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@CongA Tn A B C X O Y) (same_side' P Y O X)) *)
ex_and HH Y.

(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@CongA Tn A B C X O Y) (same_side' P Y O X)) *)
exists Y.
(* Goal: @Hilbert_euclidean_ID (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) Hilbert_euclidean_follows_from_Tarski_euclidean *)
split.
(* Goal: @OS Tn (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l) A B *)
assumption.
(* Goal: same_side' P Y O X *)
apply OS_same_side'.
(* Goal: @OS Tn O X P Y *)
apply invert_one_side.
(* Goal: @OS Tn (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l) B A *)
apply one_side_symmetry.
(* Goal: @OS Tn (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l) A B *)
assumption.
Qed.

Lemma same_side_trans :
 forall A B C l,
  same_side A B l -> same_side B C l -> same_side A C l.
Proof.
(* Goal: forall (l : @Couple (@Tpoint Tn)) (P : @Tpoint Tn) (m1 m2 : @Couple (@Tpoint Tn)) (_ : not (@IncidentL Tn P l)) (_ : Para l m1) (_ : @IncidentL Tn P m1) (_ : Para l m2) (_ : @IncidentL Tn P m2), @EqL Tn m1 m2 *)
intros.
(* Goal: same_side B A l *)
apply one_side_same_side.
(* Goal: @OS Tn (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l) B A *)
apply same_side_one_side in H.
apply same_side_one_side in H0.
eapply one_side_transitivity.
(* Goal: False *)
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@CongA Tn A B C X O Y) (same_side' P Y O X)) *)
apply H.
(* Goal: @OS Tn (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l) A B *)
assumption.
Qed.

Lemma same_side_sym :
 forall A B l,
  same_side A B l -> same_side B A l.
Proof.
(* Goal: forall (l : @Couple (@Tpoint Tn)) (P : @Tpoint Tn) (m1 m2 : @Couple (@Tpoint Tn)) (_ : not (@IncidentL Tn P l)) (_ : Para l m1) (_ : @IncidentL Tn P m1) (_ : Para l m2) (_ : @IncidentL Tn P m2), @EqL Tn m1 m2 *)
intros.
(* Goal: same_side B A l *)
apply one_side_same_side.
(* Goal: @OS Tn (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l) B A *)
apply same_side_one_side in H.
(* Goal: @OS Tn (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l) B A *)
apply one_side_symmetry.
(* Goal: @OS Tn (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l) A B *)
assumption.
Qed.


Lemma axiom_hcong_4_uniqueness :
  forall A B C O P X Y Y', ~ Col_H P O X  -> ~ Col_H A B C -> CongA A B C X O Y -> CongA A B C X O Y' -> 
  same_side' P Y O X -> same_side' P Y' O X -> outH O Y Y'.
Proof.
(* Goal: forall (l : @Couple (@Tpoint Tn)) (P : @Tpoint Tn) (m1 m2 : @Couple (@Tpoint Tn)) (_ : not (@IncidentL Tn P l)) (_ : Para l m1) (_ : @IncidentL Tn P m1) (_ : Para l m2) (_ : @IncidentL Tn P m2), @EqL Tn m1 m2 *)
intros.
rewrite <- cols_coincide in H.
rewrite <- cols_coincide in H0.
assert (T:CongA X O Y X O Y').
eapply conga_trans.
apply conga_sym.
apply H1.
(* Goal: @OS Tn (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l) A B *)
assumption.

apply conga_cop__or_out_ts in T.
induction T.
apply out_outH.
(* Goal: @OS Tn (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l) A B *)
assumption.

apply same_side_OS in H3.
apply same_side_OS in H4.
exfalso.
assert (OS O X Y Y').
apply one_side_transitivity with P.
(* Goal: @OS Tn (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l) B A *)
apply one_side_symmetry.
(* Goal: @OS Tn (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l) A B *)
assumption.
(* Goal: @OS Tn (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l) A B *)
assumption.
apply invert_one_side in H6.
apply l9_9 in H5.
(* Goal: @CongA Tn A B C A' B' C' *)
intuition.

apply same_side_OS in H3.
apply same_side_OS in H4.
apply coplanar_trans_1 with P; Col; Cop.
Qed.

Lemma axiom_conga_comm : forall A B C,
 ~ Col_H A B C -> CongA A B C C B A.
Proof.
(* Goal: forall (l : @Couple (@Tpoint Tn)) (P : @Tpoint Tn) (m1 m2 : @Couple (@Tpoint Tn)) (_ : not (@IncidentL Tn P l)) (_ : Para l m1) (_ : @IncidentL Tn P m1) (_ : Para l m2) (_ : @IncidentL Tn P m2), @EqL Tn m1 m2 *)
intros.
rewrite <- cols_coincide in H.
(* Goal: @CongA Tn A B C C B A *)
assert_diffs.
(* Goal: not (@eq (@Tpoint Tn) A P) *)
(* Goal: or (@Bet Tn P A B) (@Bet Tn P B A) *)
apply conga_pseudo_refl;auto.
Qed.

Lemma axiom_congaH_outH_congaH :
 forall A B C D E F A' C' D' F' : Tpoint,
  CongA A B C D E F ->
  Between_H B A A' \/ Between_H B A' A \/ B <> A /\ A = A' ->
  Between_H B C C' \/ Between_H B C' C \/ B <> C /\ C = C' ->
  Between_H E D D' \/ Between_H E D' D \/ E <> D /\ D = D' ->
  Between_H E F F' \/ Between_H E F' F \/ E <> F /\ F = F' ->
  CongA A' B C' D' E F'.
Proof.
(* Goal: forall (l : @Couple (@Tpoint Tn)) (P : @Tpoint Tn) (m1 m2 : @Couple (@Tpoint Tn)) (_ : not (@IncidentL Tn P l)) (_ : Para l m1) (_ : @IncidentL Tn P m1) (_ : Para l m2) (_ : @IncidentL Tn P m2), @EqL Tn m1 m2 *)
intros.
(* Goal: @CongA Tn A' B C' D' E F' *)
apply out_conga with A C D F;auto using outH_out.
Qed.

Lemma axiom_conga_permlr:
forall A B C D E F : Tpoint, CongA A B C D E F -> CongA C B A F E D.
Proof.
(* Goal: forall (A B C D E F : @Tpoint Tn) (_ : @CongA Tn A B C D E F), @CongA Tn C B A F E D *)
apply Ch11_angles.conga_comm.
Qed.

(*
Lemma axiom_inter_dec : forall l m,
  (exists P, IncidentL P l /\ IncidentL P m) \/ ~ (exists P, IncidentL P l /\ IncidentL P m).
Proof.
intros l m;
elim (inter_dec (P1 l) (P2 l) (P1 m) (P2 m));
(* Goal: not (@eq (@Tpoint Tn) A P) *)
(* Goal: or (@Bet Tn P A B) (@Bet Tn P B A) *)
intro; [left|right]; auto.
Qed.
*)

Lemma axiom_conga_refl : forall A B C, ~ Col_H A B C -> CongA A B C A B C.
Proof.
(* Goal: forall (A B C : @Tpoint Tn) (_ : not (Col_H A B C)), @CongA Tn A B C A B C *)
intros A B C H.
(* Goal: @Col Tn P O X *)
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@CongA Tn A B C X O Y) (same_side' P Y O X)) *)
apply Ch11_angles.conga_refl; intro; subst; apply H; apply cols_coincide; Col.
Qed.

End T.

Section Tarski_neutral_to_Hilbert_neutral.

Context `{TnEQD:Tarski_neutral_dimensionless_with_decidable_point_equality}.

Instance Hilbert_neutral_follows_from_Tarski_neutral : Hilbert_neutral_dimensionless.
Proof.
exact (Build_Hilbert_neutral_dimensionless Tpoint Line Plane EqL EqL_Equiv EqP EqP_Equiv IncidentL
       IncidentP axiom_Incid_morphism axiom_Incid_dec axiom_Incidp_morphism axiom_Incidp_dec
       eq_dec_points axiom_line_existence axiom_line_uniqueness axiom_two_points_on_line PA
       PB PC lower_dim' axiom_plane_existence axiom_one_point_on_plane axiom_plane_uniqueness
       axiom_line_on_plane Between_H axiom_between_diff axiom_between_col axiom_between_comm
       axiom_between_out axiom_between_only_one axiom_pasch Cong cong_right_commutativity
       axiom_hcong_1_existence cong_inner_transitivity
        axiom_hcong_3 CongA axiom_conga_refl axiom_conga_comm
       axiom_conga_permlr axiom_congaH_outH_congaH axiom_hcong_4_existence
       axiom_hcong_4_uniqueness axiom_cong_5').
Defined.

End Tarski_neutral_to_Hilbert_neutral.

Section Tarski_neutral_2D_to_Hilbert_neutral_2D.

Context `{T2D:Tarski_2D}.

Instance Hilbert_2D_follows_from_Tarski_2D : Hilbert_neutral_2D Hilbert_neutral_follows_from_Tarski_neutral.
Proof.
(* Goal: @Hilbert_euclidean_ID (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) Hilbert_euclidean_follows_from_Tarski_euclidean *)
split.
(* Goal: forall (A B C : @Point (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD)) (l : @hilbert_axioms.Line (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD)) (_ : not (@ColH (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) A B C)) (_ : not (@IncidL (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) C l)) (_ : @hilbert_axioms.cut (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) l A B), or (@hilbert_axioms.cut (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) l A C) (@hilbert_axioms.cut (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) l B C) *)
intros A B C l HNCol HNCl Hcut.
apply axiom_pasch with (Plan A B C HNCol); trivial;
  unfold IncidentLP, IncidentP; intros; try (apply all_coplanar).
Defined.

End Tarski_neutral_2D_to_Hilbert_neutral_2D.

Section Tarski_neutral_3D_to_Hilbert_neutral_3D.

Context `{T3D:Tarski_3D}.

Lemma lower_dim_3' : {A : Tpoint & {B : Tpoint & {C : Tpoint & {D |
  ~ exists p, IncidentP A p /\ IncidentP B p /\ IncidentP C p /\ IncidentP D p}}}}.
Proof.
(* Goal: @sigT (@Tpoint Tn) (fun A : @Tpoint Tn => @sigT (@Tpoint Tn) (fun B : @Tpoint Tn => @sigT (@Tpoint Tn) (fun C : @Tpoint Tn => @sig (@Tpoint Tn) (fun D : @Tpoint Tn => not (@ex (@Plane Tn) (fun p : @Plane Tn => and (@IncidentP Tn A p) (and (@IncidentP Tn B p) (and (@IncidentP Tn C p) (@IncidentP Tn D p))))))))) *)
exists S1, S2, S3, S4.
(* Goal: and (not (@eq (@Tpoint Tn) A P)) (and (not (@eq (@Tpoint Tn) B P)) (or (@Bet Tn P A B) (@Bet Tn P B A))) *)
intros [p]; spliter.
(* Goal: @OS Tn (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l) A B *)
apply tarski_axioms.lower_dim_3, plane_cop with p; assumption.
Qed.

Instance Hilbert_3D_follows_from_Tarski_3D : Hilbert_neutral_3D Hilbert_neutral_follows_from_Tarski_neutral.
Proof.
(* Goal: Hilbert_neutral_3D (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) *)
destruct lower_dim_3' as [A [B [C [D n]]]].
(* Goal: Hilbert_neutral_3D (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) *)
exists A B C D; [|assumption].
(* Goal: forall (A : @Point (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD)) (p q : @hilbert_axioms.Plane (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD)) (_ : @IncidP (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) A p) (_ : @IncidP (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) A q), @ex (@Point (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD)) (fun B : @Point (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) => and (@IncidP (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) B p) (and (@IncidP (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) B q) (not (@eq (@Point (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD)) A B)))) *)
clear A B C D n.
(* Goal: forall (A : @Point (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD)) (p q : @hilbert_axioms.Plane (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD)) (_ : @IncidP (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) A p) (_ : @IncidP (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) A q), @ex (@Point (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD)) (fun B : @Point (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) => and (@IncidP (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) B p) (and (@IncidP (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) B q) (not (@eq (@Point (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD)) A B)))) *)
intros A p q HAp HAq.
(* Goal: @ex (@Point (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD)) (fun B : @Point (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) => and (@IncidP (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) B p) (and (@IncidP (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) B q) (not (@eq (@Point (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD)) A B)))) *)
destruct p as [P1 P2 P3 HP].
(* Goal: @ex (@Point (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD)) (fun B : @Point (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) => and (@IncidP (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) B (@Plan Tn P1 P2 P3 HP)) (and (@IncidP (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) B q) (not (@eq (@Point (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD)) A B)))) *)
destruct q as [Q1 Q2 Q3 HQ].
(* Goal: @OS Tn A B P Q *)
unfold IncidP in *; simpl in *; unfold IncidentP in *; simpl in *.
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (@Coplanar Tn P1 P2 P3 B) (and (@Coplanar Tn Q1 Q2 Q3 B) (not (@eq (@Tpoint Tn) A B)))) *)
assert (pi : plane_intersection_axiom).
(* Goal: @plane_intersection_axiom Tn *)
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (@Coplanar Tn P1 P2 P3 B) (and (@Coplanar Tn Q1 Q2 Q3 B) (not (@eq (@Tpoint Tn) A B)))) *)
cut upper_dim_3_axiom.
(* Goal: not (@eq (@Tpoint Tn) A P) *)
(* Goal: or (@Bet Tn P A B) (@Bet Tn P B A) *)
apply upper_dim_3_equivalent_axioms; simpl; tauto.
(* Goal: @upper_dim_3_axiom Tn *)
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (@Coplanar Tn P1 P2 P3 B) (and (@Coplanar Tn Q1 Q2 Q3 B) (not (@eq (@Tpoint Tn) A B)))) *)
unfold upper_dim_3_axiom.
(* Goal: forall (A B C P Q R : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) P Q)) (_ : not (@eq (@Tpoint Tn) Q R)) (_ : not (@eq (@Tpoint Tn) P R)) (_ : @Cong Tn A P A Q) (_ : @Cong Tn B P B Q) (_ : @Cong Tn C P C Q) (_ : @Cong Tn A P A R) (_ : @Cong Tn B P B R) (_ : @Cong Tn C P C R), or (@Bet Tn A B C) (or (@Bet Tn B C A) (@Bet Tn C A B)) *)
(* Goal: @ex (@Tpoint Tn) (fun B : @Tpoint Tn => and (@Coplanar Tn P1 P2 P3 B) (and (@Coplanar Tn Q1 Q2 Q3 B) (not (@eq (@Tpoint Tn) A B)))) *)
apply upper_dim_3.
(* Goal: @OS Tn (@P1 (@Tpoint Tn) l) (@P2 (@Tpoint Tn) l) A B *)
apply pi; assumption.
Defined.

End Tarski_neutral_3D_to_Hilbert_neutral_3D.

Section Tarski_Euclidean_to_Hilbert_Euclidean.

Context `{TE:Tarski_euclidean}.

(** * Group Parallels *)

Definition Para := fun l m =>
  (~ exists X, IncidentL X l /\ IncidentL X m) /\ exists p, IncidentLP l p /\ IncidentLP m p.

Lemma Para_Par : forall A B C D (HAB : A<>B) (HCD: C<>D),
 Para (Lin A B HAB) (Lin C D HCD) -> Par A B C D.
Proof.
(* Goal: forall (A B C D : @Tpoint Tn) (HAB : not (@eq (@Tpoint Tn) A B)) (HCD : not (@eq (@Tpoint Tn) C D)) (_ : Para (@Lin Tn A B HAB) (@Lin Tn C D HCD)), @Par Tn A B C D *)
unfold Para, IncidentL, Par, Par_strict; simpl.
(* Goal: forall (l : @Couple (@Tpoint Tn)) (P : @Tpoint Tn) (m1 m2 : @Couple (@Tpoint Tn)) (_ : not (@IncidentL Tn P l)) (_ : Para l m1) (_ : @IncidentL Tn P m1) (_ : Para l m2) (_ : @IncidentL Tn P m2), @EqL Tn m1 m2 *)
intros.
(* Goal: or (and (not (@eq (@Tpoint Tn) A B)) (and (not (@eq (@Tpoint Tn) C D)) (and (@Coplanar Tn A B C D) (not (@ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X A B) (@Col Tn X C D))))))) (and (not (@eq (@Tpoint Tn) A B)) (and (not (@eq (@Tpoint Tn) C D)) (and (@Col Tn A C D) (@Col Tn B C D)))) *)
destruct H as [HNI [p []]].
(* Goal: or (and (not (@eq (@Tpoint Tn) A B)) (and (not (@eq (@Tpoint Tn) C D)) (and (@Coplanar Tn A B C D) (not (@ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X A B) (@Col Tn X C D))))))) (and (not (@eq (@Tpoint Tn) A B)) (and (not (@eq (@Tpoint Tn) C D)) (and (@Col Tn A C D) (@Col Tn B C D)))) *)
left.
(* Goal: not (@eq (@Tpoint Tn) A P) *)
(* Goal: or (@Bet Tn P A B) (@Bet Tn P B A) *)
repeat split;auto.
(* Goal: @Col Tn P O X *)
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@CongA Tn A B C X O Y) (same_side' P Y O X)) *)
apply plane_cop with p; [apply H|apply H|apply H0..]; unfold IncidentL; simpl; Col.
Qed.

Lemma axiom_euclid_uniqueness :
  forall l P m1 m2,
  ~ IncidentL P l ->
   Para l m1 -> IncidentL P m1 ->
   Para l m2 -> IncidentL P m2 ->
   EqL m1 m2.
Proof.
(* Goal: forall (l : @Couple (@Tpoint Tn)) (P : @Tpoint Tn) (m1 m2 : @Couple (@Tpoint Tn)) (_ : not (@IncidentL Tn P l)) (_ : Para l m1) (_ : @IncidentL Tn P m1) (_ : Para l m2) (_ : @IncidentL Tn P m2), @EqL Tn m1 m2 *)
intros.
(* Goal: @EqL Tn m1 m2 *)
destruct l as [A B HAB].
(* Goal: @EqL Tn m1 m2 *)
destruct m1 as [C D HCD].
(* Goal: @EqL Tn (build_couple (@Tpoint Tn) C D HCD) m2 *)
destruct m2 as [C' D' HCD'].
(* Goal: @OS Tn A B P Q *)
unfold IncidentL in *;simpl in *.
(* Goal: @EqL Tn (build_couple (@Tpoint Tn) C D HCD) (build_couple (@Tpoint Tn) C' D' HCD') *)
apply Para_Par in H0.
(* Goal: @EqL Tn (build_couple (@Tpoint Tn) C D HCD) (build_couple (@Tpoint Tn) C' D' HCD') *)
apply Para_Par in H2.
(* Goal: forall (l : @Couple (@Tpoint Tn)) (P : @Tpoint Tn) (m1 m2 : @Couple (@Tpoint Tn)) (_ : not (@IncidentL Tn P l)) (_ : Para l m1) (_ : @IncidentL Tn P m1) (_ : Para l m2) (_ : @IncidentL Tn P m2), @EqL Tn m1 m2 *)
elim (tarski_s_euclid_implies_playfair euclid A B C D C' D' P H0 H1 H2 H3);intros.
apply axiom_line_uniqueness with C' D';
(* Goal: @Col Tn P O X *)
(* Goal: @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@CongA Tn A B C X O Y) (same_side' P Y O X)) *)
unfold IncidentL;simpl;Col.
Qed.

Instance Hilbert_euclidean_follows_from_Tarski_euclidean :
  Hilbert_euclidean Hilbert_neutral_follows_from_Tarski_neutral.
Proof.
(* Goal: @Hilbert_euclidean_ID (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) Hilbert_euclidean_follows_from_Tarski_euclidean *)
split.
(* Goal: forall (l : @hilbert_axioms.Line (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD)) (P : @Point (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD)) (m1 m2 : @hilbert_axioms.Line (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD)) (_ : not (@IncidL (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) P l)) (_ : and (not (@ex (@Point (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD)) (fun X : @Point (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) => and (@IncidL (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) X l) (@IncidL (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) X m1)))) (@ex (@hilbert_axioms.Plane (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD)) (fun p : @hilbert_axioms.Plane (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) => and (@IncidLP (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) l p) (@IncidLP (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) m1 p)))) (_ : @IncidL (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) P m1) (_ : and (not (@ex (@Point (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD)) (fun X : @Point (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) => and (@IncidL (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) X l) (@IncidL (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) X m2)))) (@ex (@hilbert_axioms.Plane (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD)) (fun p : @hilbert_axioms.Plane (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) => and (@IncidLP (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) l p) (@IncidLP (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) m2 p)))) (_ : @IncidL (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) P m2), @hilbert_axioms.EqL (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) m1 m2 *)
apply axiom_euclid_uniqueness.
Defined.

Instance Hilbert_euclidean_ID_follows_from_Tarski_euclidean :
  Hilbert_euclidean_ID Hilbert_euclidean_follows_from_Tarski_euclidean.
Proof.
(* Goal: @Hilbert_euclidean_ID (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) Hilbert_euclidean_follows_from_Tarski_euclidean *)
split.
(* Goal: forall l m : @hilbert_axioms.Line (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD), or (@ex (@Point (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD)) (fun I : @Point (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) => and (@IncidL (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) I l) (@IncidL (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) I m))) (not (@ex (@Point (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD)) (fun I : @Point (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) => and (@IncidL (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) I l) (@IncidL (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) I m)))) *)
intros l m.
(* Goal: or (@ex (@Point (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD)) (fun I : @Point (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) => and (@IncidL (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) I l) (@IncidL (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) I m))) (not (@ex (@Point (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD)) (fun I : @Point (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) => and (@IncidL (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) I l) (@IncidL (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) I m)))) *)
assert (ID : decidability_of_intersection).
(* Goal: @decidability_of_intersection Tn *)
(* Goal: or (@ex (@Point (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD)) (fun I : @Point (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) => and (@IncidL (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) I l) (@IncidL (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) I m))) (not (@ex (@Point (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD)) (fun I : @Point (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) => and (@IncidL (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) I l) (@IncidL (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) I m)))) *)
apply strong_parallel_postulate_implies_inter_dec.
(* Goal: @strong_parallel_postulate Tn *)
(* Goal: or (@ex (@Point (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD)) (fun I : @Point (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) => and (@IncidL (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) I l) (@IncidL (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) I m))) (not (@ex (@Point (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD)) (fun I : @Point (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) => and (@IncidL (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) I l) (@IncidL (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) I m)))) *)
cut tarski_s_parallel_postulate.
(* Goal: not (@eq (@Tpoint Tn) A P) *)
(* Goal: or (@Bet Tn P A B) (@Bet Tn P B A) *)
apply equivalent_postulates_without_decidability_of_intersection_of_lines_bis; simpl; tauto.
(* Goal: @tarski_s_parallel_postulate Tn *)
(* Goal: or (@ex (@Point (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD)) (fun I : @Point (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) => and (@IncidL (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) I l) (@IncidL (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) I m))) (not (@ex (@Point (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD)) (fun I : @Point (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) => and (@IncidL (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) I l) (@IncidL (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) I m)))) *)
unfold tarski_s_parallel_postulate.
(* Goal: forall (A B C D T : @Tpoint Tn) (_ : @Bet Tn A D T) (_ : @Bet Tn B D C) (_ : not (@eq (@Tpoint Tn) A D)), @ex (@Tpoint Tn) (fun X : @Tpoint Tn => @ex (@Tpoint Tn) (fun Y : @Tpoint Tn => and (@Bet Tn A B X) (and (@Bet Tn A C Y) (@Bet Tn X T Y)))) *)
(* Goal: or (@ex (@Point (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD)) (fun I : @Point (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) => and (@IncidL (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) I l) (@IncidL (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) I m))) (not (@ex (@Point (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD)) (fun I : @Point (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) => and (@IncidL (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) I l) (@IncidL (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) I m)))) *)
apply euclid.
(* Goal: or (@ex (@Point (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD)) (fun I : @Point (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) => and (@IncidL (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) I l) (@IncidL (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) I m))) (not (@ex (@Point (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD)) (fun I : @Point (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) => and (@IncidL (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) I l) (@IncidL (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) I m)))) *)
destruct l as [L1 L2 HL].
(* Goal: or (@ex (@Point (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD)) (fun I : @Point (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) => and (@IncidL (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) I (build_couple (@Tpoint Tn) L1 L2 HL)) (@IncidL (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) I m))) (not (@ex (@Point (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD)) (fun I : @Point (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) => and (@IncidL (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) I (build_couple (@Tpoint Tn) L1 L2 HL)) (@IncidL (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) I m)))) *)
destruct m as [M1 M2 HM].
(* Goal: or (@ex (@Point (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD)) (fun I : @Point (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) => and (@IncidL (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) I (build_couple (@Tpoint Tn) L1 L2 HL)) (@IncidL (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) I (build_couple (@Tpoint Tn) M1 M2 HM)))) (not (@ex (@Point (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD)) (fun I : @Point (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) => and (@IncidL (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) I (build_couple (@Tpoint Tn) L1 L2 HL)) (@IncidL (@Hilbert_neutral_follows_from_Tarski_neutral Tn TnEQD) I (build_couple (@Tpoint Tn) M1 M2 HM))))) *)
simpl; unfold IncidentL; simpl.
(* Goal: or (@ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn I L1 L2) (@Col Tn I M1 M2))) (not (@ex (@Tpoint Tn) (fun I : @Tpoint Tn => and (@Col Tn I L1 L2) (@Col Tn I M1 M2)))) *)
apply ID.
Defined.

End Tarski_Euclidean_to_Hilbert_Euclidean.