(* Gabriel Braun March 2013 *)

Require Export GeoCoq.Tarski_dev.Annexes.vectors.

Section Projections.

Context `{T2D:Tarski_2D}.
Context `{TE:@Tarski_euclidean Tn TnEQD}.

Lemma project_id : forall A B X Y P P', Proj P P' A B X Y -> Col A B P -> P = P'.
Proof.
(* Goal: forall (P P' A B : @Tpoint Tn) (_ : @Projp Tn P P' A B), @Projp Tn P' P' A B *)
intros.
(* Goal: @Col Tn A B P *)
unfold Proj in H.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.
(* Goal: not (@Col Tn A B P) *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
induction H4.

(* Goal: @eq (@Tpoint Tn) P Q *)
apply False_ind.
(* Goal: False *)
(* Goal: @eq (@Tpoint Tn) P P' *)
apply H2.

(* Goal: or (not (@eq (@Tpoint Tn) P' A)) (not (@eq (@Tpoint Tn) P' B)) *)
(* Goal: or (not (@eq (@Tpoint Tn) P' A)) (not (@eq (@Tpoint Tn) P' B)) *)
induction(eq_dec_points P' A).
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
subst P'.
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
eapply  (par_col_par_2 _ P); Col.
(* Goal: not (@Par Tn A B X Y) *)
(* Goal: @Col Tn A B P' *)
(* Goal: or (@Par Tn P P' X Y) (@eq (@Tpoint Tn) P P') *)
(* Goal: and (@Proj Tn P P' A B X Y) (forall (x' : @Tpoint Tn) (_ : @Proj Tn P x' A B X Y), @eq (@Tpoint Tn) P' x') *)
Par.

(* Goal: @Par Tn A B X Y *)
(* Goal: @eq (@Tpoint Tn) P P' *)
eapply (par_col_par_2 _ P'); Col.
(* Goal: @Par Tn A P X Y *)
apply par_left_comm.
(* Goal: @Par Tn A B X Y *)
eapply (par_col_par_2 _ P); Col.
(* Goal: @Col Tn P Q A *)
ColR.
(* Goal: not (@Par Tn A B X Y) *)
(* Goal: @Col Tn A B P' *)
(* Goal: or (@Par Tn P P' X Y) (@eq (@Tpoint Tn) P P') *)
(* Goal: and (@Proj Tn P P' A B X Y) (forall (x' : @Tpoint Tn) (_ : @Proj Tn P x' A B X Y), @eq (@Tpoint Tn) P' x') *)
Par.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.
Qed.

Lemma project_not_id : forall A B X Y P P', Proj P P' A B X Y -> ~Col A B P -> P <> P'.
Proof.
(* Goal: forall (P P' A B : @Tpoint Tn) (_ : @Projp Tn P P' A B), @Projp Tn P' P' A B *)
intros.
(* Goal: not (@Col Tn C A B) *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
intro.
(* Goal: False *)
apply H0.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
subst P'.
(* Goal: @Col Tn A B P *)
unfold Proj in H.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.
Qed.

Lemma project_col : forall A B X Y P , Proj P P A B X Y -> Col A B P.
Proof.
(* Goal: forall (P P' A B : @Tpoint Tn) (_ : @Projp Tn P P' A B), @Projp Tn P' P' A B *)
intros.
(* Goal: @Col Tn A B P *)
unfold Proj in H.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.
Qed.

Lemma project_not_col : forall A B X Y P P', Proj P P' A B X Y -> P <> P' -> ~Col A B P.
Proof.
(* Goal: forall (P P' A B : @Tpoint Tn) (_ : @Projp Tn P P' A B), @Projp Tn P' P' A B *)
intros.
(* Goal: not (@Col Tn C A B) *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
intro.
(* Goal: False *)
apply H0.
eapply project_id.
(* Goal: False *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
apply H.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.
Qed.

Lemma project_par : forall A B X Y P Q P' Q', Proj P P' A B X Y -> Proj Q Q' A B X Y -> Par P Q X Y -> P' = Q'.
Proof.
(* Goal: forall (P P' A B : @Tpoint Tn) (_ : @Projp Tn P P' A B), @Projp Tn P' P' A B *)
intros.
(* Goal: @eq (@Tpoint Tn) P' Q' *)
assert(HH:=H).
(* Goal: @eq (@Tpoint Tn) P' Q' *)
assert(HH0:=H0).
(* Goal: @eq (@Tpoint Tn) P' Q' *)
unfold Proj in HH.
(* Goal: @eq (@Tpoint Tn) P' Q' *)
unfold Proj in HH0.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.

(* Goal: @Proj Tn P P' A B X Y *)
apply par_distincts in H1.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.

(* Goal: @eq (@Tpoint Tn) P' Q' *)
induction H11.

(* Goal: @eq (@Tpoint Tn) P' Q' *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
assert(Col P P P' /\ Col Q P P').
(* Goal: and (@Col Tn P P P') (@Col Tn Q P P') *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
apply(parallel_uniqueness X Y P P' P Q P); Col.
(* Goal: not (@Par Tn A B X Y) *)
(* Goal: @Col Tn A B P' *)
(* Goal: or (@Par Tn P P' X Y) (@eq (@Tpoint Tn) P P') *)
(* Goal: and (@Proj Tn P P' A B X Y) (forall (x' : @Tpoint Tn) (_ : @Proj Tn P x' A B X Y), @eq (@Tpoint Tn) P' x') *)
Par.
(* Goal: not (@Par Tn A B X Y) *)
(* Goal: @Col Tn A B P' *)
(* Goal: or (@Par Tn P P' X Y) (@eq (@Tpoint Tn) P P') *)
(* Goal: and (@Proj Tn P P' A B X Y) (forall (x' : @Tpoint Tn) (_ : @Proj Tn P x' A B X Y), @eq (@Tpoint Tn) P' x') *)
Par.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.

(* Goal: @eq (@Tpoint Tn) P' Q' *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
apply par_distincts in H11.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.

(* Goal: @eq (@Tpoint Tn) P' Q' *)
induction H6.

(* Goal: @eq (@Tpoint Tn) P' Q' *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
assert(Col P Q Q' /\ Col Q Q Q').
(* Goal: and (@Col Tn P Q Q') (@Col Tn Q Q Q') *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
apply(parallel_uniqueness X Y Q Q' P Q Q); Col.
(* Goal: not (@Par Tn A B X Y) *)
(* Goal: @Col Tn A B P' *)
(* Goal: or (@Par Tn P P' X Y) (@eq (@Tpoint Tn) P P') *)
(* Goal: and (@Proj Tn P P' A B X Y) (forall (x' : @Tpoint Tn) (_ : @Proj Tn P x' A B X Y), @eq (@Tpoint Tn) P' x') *)
Par.
(* Goal: not (@Par Tn A B X Y) *)
(* Goal: @Col Tn A B P' *)
(* Goal: or (@Par Tn P P' X Y) (@eq (@Tpoint Tn) P P') *)
(* Goal: and (@Proj Tn P P' A B X Y) (forall (x' : @Tpoint Tn) (_ : @Proj Tn P x' A B X Y), @eq (@Tpoint Tn) P' x') *)
Par.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.

(* Goal: @eq (@Tpoint Tn) P' Q' *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
clean_duplicated_hyps.
(* Goal: @eq (@Tpoint Tn) P' Q' *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
clear H14.
(* Goal: @eq (@Tpoint Tn) P' Q' *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
clear H19.

(* Goal: @eq (@Tpoint Tn) P' Q' *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
apply par_distincts in H6.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.

(* Goal: @eq (@Tpoint Tn) P' Q *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
eapply (l6_21 A B P Q); Col.
(* Goal: not (@Col Tn C A B) *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
intro.
(* Goal: False *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
apply H16.
(* Goal: @eq (@Tpoint Tn) P P' *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
apply(project_id A B X Y P P'); Col.

(* Goal: @eq (@Tpoint Tn) P Q' *)
subst Q'.

(* Goal: @eq (@Tpoint Tn) P' Q *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
eapply (l6_21 A B P Q); Col.
(* Goal: not (@Col Tn C A B) *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
intro.
(* Goal: False *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
apply H16.
(* Goal: @eq (@Tpoint Tn) P P' *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
apply(project_id A B X Y P P'); Col.

(* Goal: @eq (@Tpoint Tn) P' Q' *)
induction H6.
(* Goal: @eq (@Tpoint Tn) P' Q' *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
apply par_distincts in H6.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.

(* Goal: @eq (@Tpoint Tn) P' Q' *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
assert(Col P Q Q' /\ Col Q Q Q').
(* Goal: and (@Col Tn P Q Q') (@Col Tn Q Q Q') *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
apply(parallel_uniqueness X Y Q Q' P Q Q); Col.
(* Goal: not (@Par Tn A B X Y) *)
(* Goal: @Col Tn A B P' *)
(* Goal: or (@Par Tn P P' X Y) (@eq (@Tpoint Tn) P P') *)
(* Goal: and (@Proj Tn P P' A B X Y) (forall (x' : @Tpoint Tn) (_ : @Proj Tn P x' A B X Y), @eq (@Tpoint Tn) P' x') *)
Par.
(* Goal: not (@Par Tn A B X Y) *)
(* Goal: @Col Tn A B P' *)
(* Goal: or (@Par Tn P P' X Y) (@eq (@Tpoint Tn) P P') *)
(* Goal: and (@Proj Tn P P' A B X Y) (forall (x' : @Tpoint Tn) (_ : @Proj Tn P x' A B X Y), @eq (@Tpoint Tn) P' x') *)
Par.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.
(* Goal: @eq (@Tpoint Tn) P' Q' *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
clear H17.

(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
subst P'.
(* Goal: @eq (@Tpoint Tn) P Q' *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
eapply (l6_21 A B Q P); Col.
(* Goal: not (@Col Tn C A B) *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
intro.
(* Goal: False *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
apply H14.
(* Goal: @eq (@Tpoint Tn) Q Q' *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
apply(project_id A B X Y Q Q'); Col.

(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
subst P'.
(* Goal: @eq (@Tpoint Tn) P Q' *)
subst Q'.

(* Goal: @eq (@Tpoint Tn) P Q *)
apply False_ind.
(* Goal: False *)
apply H4.

(* Goal: @Par Tn A B X Y *)
induction(eq_dec_points A P).
(* Goal: or (not (@eq (@Tpoint Tn) P A)) (not (@eq (@Tpoint Tn) P B)) *)
(* Goal: or (not (@eq (@Tpoint Tn) P A)) (not (@eq (@Tpoint Tn) P B)) *)
subst P.

(* Goal: @Par Tn P A X Y *)
eapply (par_col_par_2 _ Q); Col.

(* Goal: @Par Tn A B X Y *)
eapply (par_col_par_2 _ P); Col.
(* Goal: @Par Tn A P X Y *)
apply par_left_comm.
(* Goal: @Par Tn P A X Y *)
eapply (par_col_par_2 _ Q); Col.
(* Goal: @Col Tn P Q A *)
ColR.
Qed.

Lemma ker_col : forall P Q P' A B X Y, Proj P P' A B X Y -> Proj Q P' A B X Y -> Col P Q P'.
Proof.
(* Goal: forall (P P' A B : @Tpoint Tn) (_ : @Projp Tn P P' A B), @Projp Tn P' P' A B *)
intros.
(* Goal: @Proj Tn P' P' A B X Y *)
unfold Proj in *.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.
(* Goal: @eq (@Tpoint Tn) P' Q' *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
clean_duplicated_hyps.
induction H8; induction H4; try(subst P';Col).
assert(Par P P' Q P').
eapply par_trans.
(* Goal: False *)
apply H0.
(* Goal: not (@Par Tn A B X Y) *)
(* Goal: @Col Tn A B P' *)
(* Goal: or (@Par Tn P P' X Y) (@eq (@Tpoint Tn) P P') *)
(* Goal: and (@Proj Tn P P' A B X Y) (forall (x' : @Tpoint Tn) (_ : @Proj Tn P x' A B X Y), @eq (@Tpoint Tn) P' x') *)
Par.
induction H2.
(* Goal: @eq (@Tpoint Tn) P Q *)
apply False_ind.
(* Goal: False *)
(* Goal: @eq (@Tpoint Tn) P P' *)
apply H2.
exists P'; Col.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
Col.
Qed.


Lemma ker_par : forall P Q P' A B X Y, P <> Q -> Proj P P' A B X Y -> Proj Q P' A B X Y -> Par P Q X Y.
Proof.
(* Goal: forall (P P' A B : @Tpoint Tn) (_ : @Projp Tn P P' A B), @Projp Tn P' P' A B *)
intros.
assert(Col P Q P').
eapply ker_col.
(* Goal: False *)
apply H0.
apply H1.

(* Goal: @Proj Tn P' P' A B X Y *)
unfold Proj in *.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.
(* Goal: @eq (@Tpoint Tn) P' Q' *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
clean_duplicated_hyps.
(* Goal: @eq (@Tpoint Tn) P' Q' *)
induction H10; induction H6.
eapply (par_col_par_2 _ P').
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
Col.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
subst P'.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
subst P'.
(* Goal: not (@Par Tn A B X Y) *)
(* Goal: @Col Tn A B P' *)
(* Goal: or (@Par Tn P P' X Y) (@eq (@Tpoint Tn) P P') *)
(* Goal: and (@Proj Tn P P' A B X Y) (forall (x' : @Tpoint Tn) (_ : @Proj Tn P x' A B X Y), @eq (@Tpoint Tn) P' x') *)
Par.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
subst P'.
(* Goal: @eq (@Tpoint Tn) P Q *)
apply False_ind.
(* Goal: False *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
apply H.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
auto.
Qed.

Lemma project_uniqueness : forall P P' Q' A B X Y, Proj P P' A B X Y -> Proj P Q' A B X Y -> P' = Q'.
Proof.
(* Goal: forall (P P' A B : @Tpoint Tn) (_ : @Projp Tn P P' A B), @Projp Tn P' P' A B *)
intros.
(* Goal: @eq (@Tpoint Tn) P' Q' *)
assert(HH:=H).
(* Goal: @eq (@Tpoint Tn) P' Q' *)
assert(HH0:=H0).
(* Goal: @eq (@Tpoint Tn) P' Q' *)
unfold Proj in HH.
(* Goal: @eq (@Tpoint Tn) P' Q' *)
unfold Proj in HH0.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.
(* Goal: @eq (@Tpoint Tn) P' Q' *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
clean_duplicated_hyps.

induction H10; induction H5.

(* Goal: @Proj Tn P P' A B X Y *)
apply par_distincts in H1.
apply par_distincts in H2.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.
clear H5.

assert(Col P P P' /\ Col Q' P P').
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
apply(parallel_uniqueness  X Y P P' P Q' P); Col.
(* Goal: not (@Par Tn A B X Y) *)
(* Goal: @Col Tn A B P' *)
(* Goal: or (@Par Tn P P' X Y) (@eq (@Tpoint Tn) P P') *)
(* Goal: and (@Proj Tn P P' A B X Y) (forall (x' : @Tpoint Tn) (_ : @Proj Tn P x' A B X Y), @eq (@Tpoint Tn) P' x') *)
Par.
(* Goal: not (@Par Tn A B X Y) *)
(* Goal: @Col Tn A B P' *)
(* Goal: or (@Par Tn P P' X Y) (@eq (@Tpoint Tn) P P') *)
(* Goal: and (@Proj Tn P P' A B X Y) (forall (x' : @Tpoint Tn) (_ : @Proj Tn P x' A B X Y), @eq (@Tpoint Tn) P' x') *)
Par.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.
clear H3.

(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
apply (l6_21 A B P P'); Col.
(* Goal: not (@Col Tn C A B) *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
intro.
apply H10.
eapply project_id.
(* Goal: False *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
apply H.
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
Col.
(* Goal: @eq (@Tpoint Tn) P Q' *)
subst Q'.
apply sym_equal.
eapply project_id.
(* Goal: False *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
apply H.
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
Col.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
subst P'.
eapply project_id.
(* Goal: False *)
apply H0.
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
Col.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
subst P'.
(* Goal: @eq (@Tpoint Tn) P Q' *)
subst Q'.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
auto.
Qed.

Lemma project_existence : forall P A B X Y,
 X<>Y -> A<>B ->
 ~ Par X Y A B ->
 exists! P', Proj P P' A B X Y.
Proof.
(* Goal: forall (P P' A B : @Tpoint Tn) (_ : @Projp Tn P P' A B), @Projp Tn P' P' A B *)
intros.
(* Goal: @ex (@Tpoint Tn) (@unique (@Tpoint Tn) (fun P' : @Tpoint Tn => @Proj Tn P P' A B X Y)) *)
assert (T:=parallel_existence X Y P H).
(* Goal: @ex (@Tpoint Tn) (@unique (@Tpoint Tn) (fun P' : @Tpoint Tn => @Proj Tn P P' A B X Y)) *)
decompose [ex and] T;clear T.
assert (~ Par x x0 A B) by (
 intro;
 assert (Par X Y A B) by ( eapply par_trans;eauto; intuition);
 intuition).

(* Goal: @ex (@Tpoint Tn) (@unique (@Tpoint Tn) (fun P' : @Tpoint Tn => @Proj Tn P P' A B X Y)) *)
apply (not_par_inter_exists x x0 A B) in H4.
(* Goal: @ex (@Tpoint Tn) (@unique (@Tpoint Tn) (fun P' : @Tpoint Tn => @Proj Tn P P' A B X Y)) *)
DecompExAnd H4 P'.
(* Goal: @ex (@Tpoint Tn) (@unique (@Tpoint Tn) (fun P' : @Tpoint Tn => @Proj Tn P P' A B X Y)) *)
exists P'.
(* Goal: @unique (@Tpoint Tn) (fun P' : @Tpoint Tn => @Proj Tn P P' A B X Y) P' *)
unfold unique.


(* Goal: and (@Proj Tn P P' A B X Y) (forall (x' : @Tpoint Tn) (_ : @Proj Tn P x' A B X Y), @eq (@Tpoint Tn) P' x') *)
assert (Proj P P' A B X Y).
(* Goal: @Proj Tn P P' A B X Y *)
unfold Proj.
(* Goal: and (not (@eq (@Tpoint Tn) A B)) (and (not (@eq (@Tpoint Tn) X Y)) (and (not (@Par Tn A B X Y)) (and (@Col Tn A B P') (or (@Par Tn P P' X Y) (@eq (@Tpoint Tn) P P'))))) *)
(* Goal: and (@Proj Tn P P' A B X Y) (forall (x' : @Tpoint Tn) (_ : @Proj Tn P x' A B X Y), @eq (@Tpoint Tn) P' x') *)
repeat split.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.
(* Goal: not (@Par Tn A B X Y) *)
(* Goal: @Col Tn A B P' *)
(* Goal: or (@Par Tn P P' X Y) (@eq (@Tpoint Tn) P P') *)
(* Goal: and (@Proj Tn P P' A B X Y) (forall (x' : @Tpoint Tn) (_ : @Proj Tn P x' A B X Y), @eq (@Tpoint Tn) P' x') *)
Par.
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
Col.
(* Goal: or (@Par Tn P P' X Y) (@eq (@Tpoint Tn) P P') *)
(* Goal: and (@Proj Tn P P' A B X Y) (forall (x' : @Tpoint Tn) (_ : @Proj Tn P x' A B X Y), @eq (@Tpoint Tn) P' x') *)
induction (eq_dec_points P P').
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
tauto.
(* Goal: or (not (@eq (@Tpoint Tn) P A)) (not (@eq (@Tpoint Tn) P B)) *)
left.
(* Goal: @Par Tn P P' X Y *)
(* Goal: and (@Proj Tn P P' A B X Y) (forall (x' : @Tpoint Tn) (_ : @Proj Tn P x' A B X Y), @eq (@Tpoint Tn) P' x') *)
apply par_symmetry.
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
apply par_col2_par with x x0;Col.

(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
split.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.

(* Goal: forall (P P' A B : @Tpoint Tn) (_ : @Projp Tn P P' A B), @Projp Tn P' P' A B *)
intros.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
eapply project_uniqueness;eauto.
Qed.

Lemma project_col_eq : forall P Q P' Q' A B X Y,
 P <> P' ->
 Col P Q P' ->
 Proj P P' A B X Y ->
 Proj Q Q' A B X Y ->
 P' = Q'.
Proof.
(* Goal: forall (P P' A B : @Tpoint Tn) (_ : @Projp Tn P P' A B), @Projp Tn P' P' A B *)
intros.
induction(eq_dec_points P Q).
subst Q.
eapply project_uniqueness.
apply H1.
(* Goal: False *)
(* Goal: @eq (@Tpoint Tn) P P' *)
apply H2.
eapply project_par.
apply H1.
(* Goal: False *)
(* Goal: @eq (@Tpoint Tn) P P' *)
apply H2.
(* Goal: @Proj Tn P' P' A B X Y *)
unfold Proj in *.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.
induction H11; induction H7.
(* Goal: @Par Tn A B X Y *)
(* Goal: @eq (@Tpoint Tn) P P' *)
eapply (par_col_par_2 _ P'); Col.
(* Goal: @eq (@Tpoint Tn) P Q' *)
subst Q'.
(* Goal: @Par Tn A B X Y *)
(* Goal: @eq (@Tpoint Tn) P P' *)
eapply (par_col_par_2 _ P'); Col.
(* Goal: not (@Col Tn A B P) *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
contradiction.
(* Goal: not (@Col Tn A B P) *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
contradiction.
Qed.


Lemma par_col_project :
 forall P P' A B X Y ,
  A <> B ->
  ~ Par A B X Y ->
  Par P P' X Y ->
  Col A B P' ->
  Proj P P' A B X Y.
Proof.
(* Goal: forall (P P' A B : @Tpoint Tn) (_ : @Projp Tn P P' A B), @Projp Tn P' P' A B *)
intros.
(* Goal: @Proj Tn P P' A B X Y *)
apply par_distincts in H1.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.
(* Goal: @Proj Tn P P' A B X Y *)
unfold Proj.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
repeat split;auto.
Qed.


Lemma project_preserves_bet :
 forall A B X Y P Q R P' Q' R',
  Bet P Q R ->
  Proj P P' A B X Y ->
  Proj Q Q' A B X Y ->
  Proj R R' A B X Y ->
  Bet P' Q' R'.
Proof.
(* Goal: forall (P P' A B : @Tpoint Tn) (_ : @Projp Tn P P' A B), @Projp Tn P' P' A B *)
intros.
(* Goal: @eq (@Tpoint Tn) P' Q' *)
assert(HH0:= H0).
assert(HH1:=H1).
assert(HH2:=H2).
(* Goal: @eq (@Tpoint Tn) P' Q' *)
unfold Proj in HH0.
unfold Proj in HH1.
unfold Proj in HH2.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.
(* Goal: @eq (@Tpoint Tn) P' Q' *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
clean_duplicated_hyps.

assert(Col P' Q' R').
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
apply (col3 A B); Col.

induction(eq_dec_points P Q).
assert(P' = Q').
subst Q.
eapply project_uniqueness.
(* Goal: False *)
apply H0.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.
(* Goal: @eq (@Tpoint Tn) P Q' *)
subst Q'.
Between.

induction (eq_dec_points R Q).
assert(R'=Q').
subst Q.
eapply project_uniqueness.
(* Goal: False *)
(* Goal: @eq (@Tpoint Tn) P P' *)
apply H2.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.
(* Goal: @eq (@Tpoint Tn) P Q' *)
subst Q'.
Between.

induction(eq_dec_points P' Q').
(* Goal: @eq (@Tpoint Tn) P Q' *)
subst Q'.
Between.
induction(eq_dec_points R' Q').
(* Goal: @eq (@Tpoint Tn) P Q' *)
subst Q'.
Between.

induction H17.
apply par_distincts in H10.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.

induction H12.
apply par_distincts in H12.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.
clear H20.

assert(Par P P' Q Q').
eapply par_trans.
apply H10.
(* Goal: not (@Par Tn A B X Y) *)
(* Goal: @Col Tn A B P' *)
(* Goal: or (@Par Tn P P' X Y) (@eq (@Tpoint Tn) P P') *)
(* Goal: and (@Proj Tn P P' A B X Y) (forall (x' : @Tpoint Tn) (_ : @Proj Tn P x' A B X Y), @eq (@Tpoint Tn) P' x') *)
Par.

assert(Par_strict  Q Q' P P').
induction H20.
apply par_strict_symmetry.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.
assert(Q'=P').

(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
apply (project_col_eq Q P Q' P' A B X Y); Col.
(* Goal: @eq (@Tpoint Tn) P Q' *)
subst Q'.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
tauto.

assert(OS  Q Q' P P').

eapply (par_strict_one_side).
apply H21.
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
Col.

induction H7.
assert(Par R R' Q Q').
eapply par_trans.
apply H7.
(* Goal: not (@Par Tn A B X Y) *)
(* Goal: @Col Tn A B P' *)
(* Goal: or (@Par Tn P P' X Y) (@eq (@Tpoint Tn) P P') *)
(* Goal: and (@Proj Tn P P' A B X Y) (forall (x' : @Tpoint Tn) (_ : @Proj Tn P x' A B X Y), @eq (@Tpoint Tn) P' x') *)
Par.
assert(Par_strict Q Q' R R' ).
induction H23.
apply par_strict_symmetry.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.
assert(Q'=R').

(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
apply(project_col_eq Q R Q' R' A B X Y); Col.
(* Goal: @eq (@Tpoint Tn) P Q' *)
subst Q'.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
tauto.
assert(OS Q Q' R R').
eapply (par_strict_one_side).
apply H24.
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
Col.

assert(TS Q Q' P R).
(* Goal: and (not (@eq (@Tpoint Tn) A B)) (and (not (@eq (@Tpoint Tn) X Y)) (and (not (@Par Tn A B X Y)) (and (@Col Tn A B P') (or (@Par Tn P P' X Y) (@eq (@Tpoint Tn) P P'))))) *)
(* Goal: and (@Proj Tn P P' A B X Y) (forall (x' : @Tpoint Tn) (_ : @Proj Tn P x' A B X Y), @eq (@Tpoint Tn) P' x') *)
repeat split.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
auto.
(* Goal: not (@Col Tn C A B) *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
intro.
apply H21.
exists P.
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
split; Col.
(* Goal: not (@Col Tn C A B) *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
intro.
apply H24.
exists R.
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
split; Col.
exists Q.
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
split; Col.

assert(TS Q Q' P' R').
eapply l9_8_2.
2: apply H22.
apply l9_2.
eapply l9_8_2.
apply l9_2.
apply H26.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.

unfold TS in H27.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.
ex_and H29 QQ.

assert(QQ=Q').
assert(Col P' QQ R').
apply bet_col.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
eapply (l6_21 Q Q' P' R'); Col.

(* Goal: not (@Col Tn C A B) *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
intro.
subst R'.
apply between_equality in H30.
subst QQ.
(* Goal: not (@Col Tn A B P) *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
contradiction.
Between.
subst QQ.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.

subst R'.

assert(TS Q Q' P' R).

eapply l9_8_2.
2:apply H22.
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
repeat split; Col.
(* Goal: not (@Col Tn C A B) *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
intro.
assert(Q'=P').
eapply project_col_eq.
apply H19.
2: apply H1.
(* Goal: False *)
2:apply H0.
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
Col.
(* Goal: @eq (@Tpoint Tn) P Q' *)
subst Q'.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
tauto.
(* Goal: not (@Col Tn C A B) *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
intro.
assert(Q' = R).
eapply project_col_eq.
apply H19.
2:apply H1.
(* Goal: False *)
(* Goal: @eq (@Tpoint Tn) P P' *)
2:apply H2.
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
Col.
(* Goal: @eq (@Tpoint Tn) P Q' *)
subst Q'.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
tauto.
exists Q.
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
split; Col.
unfold TS in H7.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.
ex_and H24 QQ.

assert(QQ=Q').
assert(Col P' QQ R).
apply bet_col.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
eapply (l6_21 Q Q' P' R); Col.

(* Goal: not (@Col Tn C A B) *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
intro.
subst R.
apply between_equality in H25.
subst QQ.
(* Goal: not (@Col Tn A B P) *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
contradiction.
Between.
subst QQ.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.
(* Goal: @eq (@Tpoint Tn) P Q' *)
subst Q'.

induction H7.

assert(HH:=parallel_existence X Y Q H14).
ex_and HH Qx.
ex_and H12 Qy.

assert(Par Qx Qy P P').
eapply par_trans.
(* Goal: @Par Tn P P' X Y *)
(* Goal: and (@Proj Tn P P' A B X Y) (forall (x' : @Tpoint Tn) (_ : @Proj Tn P x' A B X Y), @eq (@Tpoint Tn) P' x') *)
apply par_symmetry.
apply H19.
(* Goal: not (@Par Tn A B X Y) *)
(* Goal: @Col Tn A B P' *)
(* Goal: or (@Par Tn P P' X Y) (@eq (@Tpoint Tn) P P') *)
(* Goal: and (@Proj Tn P P' A B X Y) (forall (x' : @Tpoint Tn) (_ : @Proj Tn P x' A B X Y), @eq (@Tpoint Tn) P' x') *)
Par.

assert(Par_strict Qx Qy P P').
induction H21.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.
assert(P' = Q).

induction(eq_dec_points Qx Q).
subst Qx.

(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
eapply(project_col_eq P Qy P' Q A B X Y); Col.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
apply par_col_project; auto.
(* Goal: @Par Tn A P X Y *)
apply par_left_comm.
(* Goal: not (@Par Tn A B X Y) *)
(* Goal: @Col Tn A B P' *)
(* Goal: or (@Par Tn P P' X Y) (@eq (@Tpoint Tn) P P') *)
(* Goal: and (@Proj Tn P P' A B X Y) (forall (x' : @Tpoint Tn) (_ : @Proj Tn P x' A B X Y), @eq (@Tpoint Tn) P' x') *)
Par.

(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
eapply(project_col_eq P Qx P' Q A B X Y); Col.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
apply par_col_project; auto.

(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
eapply (par_col_par_2 _ Qy); Col.
(* Goal: not (@Par Tn A B X Y) *)
(* Goal: @Col Tn A B P' *)
(* Goal: or (@Par Tn P P' X Y) (@eq (@Tpoint Tn) P P') *)
(* Goal: and (@Proj Tn P P' A B X Y) (forall (x' : @Tpoint Tn) (_ : @Proj Tn P x' A B X Y), @eq (@Tpoint Tn) P' x') *)
Par.
(* Goal: not (@Col Tn A B P) *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
contradiction.
assert(OS Qx Qy P P').
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
eapply (par_strict_one_side _ _ _ P'); Col.

assert(Par Qx Qy R R').
eapply par_trans.
(* Goal: @Par Tn P P' X Y *)
(* Goal: and (@Proj Tn P P' A B X Y) (forall (x' : @Tpoint Tn) (_ : @Proj Tn P x' A B X Y), @eq (@Tpoint Tn) P' x') *)
apply par_symmetry.
apply H19.
(* Goal: not (@Par Tn A B X Y) *)
(* Goal: @Col Tn A B P' *)
(* Goal: or (@Par Tn P P' X Y) (@eq (@Tpoint Tn) P P') *)
(* Goal: and (@Proj Tn P P' A B X Y) (forall (x' : @Tpoint Tn) (_ : @Proj Tn P x' A B X Y), @eq (@Tpoint Tn) P' x') *)
Par.

assert(Par_strict Qx Qy R R').
induction H24.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.
assert(R' = Q).

induction(eq_dec_points Qx Q).
subst Qx.

(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
eapply(project_col_eq R Qy R' Q A B X Y); Col.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
apply par_col_project; auto.
(* Goal: @Par Tn A P X Y *)
apply par_left_comm.
(* Goal: not (@Par Tn A B X Y) *)
(* Goal: @Col Tn A B P' *)
(* Goal: or (@Par Tn P P' X Y) (@eq (@Tpoint Tn) P P') *)
(* Goal: and (@Proj Tn P P' A B X Y) (forall (x' : @Tpoint Tn) (_ : @Proj Tn P x' A B X Y), @eq (@Tpoint Tn) P' x') *)
Par.

(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
eapply(project_col_eq R Qx R' Q A B X Y); Col.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
apply par_col_project; auto.

(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
eapply (par_col_par_2 _ Qy); Col.
(* Goal: not (@Par Tn A B X Y) *)
(* Goal: @Col Tn A B P' *)
(* Goal: or (@Par Tn P P' X Y) (@eq (@Tpoint Tn) P P') *)
(* Goal: and (@Proj Tn P P' A B X Y) (forall (x' : @Tpoint Tn) (_ : @Proj Tn P x' A B X Y), @eq (@Tpoint Tn) P' x') *)
Par.
(* Goal: not (@Col Tn A B P) *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
contradiction.
assert(OS Qx Qy R R').
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
eapply (par_strict_one_side _ _ _ R'); Col.

assert(TS Qx Qy P R).
unfold TS.
(* Goal: and (not (@eq (@Tpoint Tn) A B)) (and (not (@eq (@Tpoint Tn) X Y)) (and (not (@Par Tn A B X Y)) (and (@Col Tn A B P') (or (@Par Tn P P' X Y) (@eq (@Tpoint Tn) P P'))))) *)
(* Goal: and (@Proj Tn P P' A B X Y) (forall (x' : @Tpoint Tn) (_ : @Proj Tn P x' A B X Y), @eq (@Tpoint Tn) P' x') *)
repeat split.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
auto.
(* Goal: not (@Col Tn C A B) *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
intro.
apply H22.
exists P.
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
split; Col.
(* Goal: not (@Col Tn C A B) *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
intro.
apply H25.
exists R.
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
split; Col.
exists Q.
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
split; Col.

assert(TS Qx Qy P' R').
eapply l9_8_2.
2:apply H23.
apply l9_2.
eapply l9_8_2.
eapply l9_2.
apply H27.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.
unfold TS in H28.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.
ex_and H30 QQ.

assert(QQ=Q).

assert(Col P' QQ R').
apply bet_col.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
eapply (l6_21 Qx Qy P' R'); Col.

(* Goal: not (@Col Tn C A B) *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
intro.
subst R'.
apply between_equality in H31.
subst QQ.
(* Goal: not (@Col Tn A B P) *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
contradiction.
Between.
subst QQ.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.


subst R'.

(* Goal: @eq (@Tpoint Tn) P Q *)
apply False_ind.
assert(~ Col A B P).
eapply project_not_col.
(* Goal: False *)
apply H0.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.
apply H7.

assert(Col A Q R).
(* Goal: @Col Tn P Q A *)
ColR.
assert(Col B Q R).
(* Goal: @Col Tn P Q A *)
ColR.

apply bet_col in H.
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
apply (col3 Q R); Col.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
subst P'.

induction H12.
induction H7.

apply par_distincts in H10.
apply par_distincts in H7.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.

assert(Par Q Q' R R').
eapply par_trans.
apply H10.
(* Goal: not (@Par Tn A B X Y) *)
(* Goal: @Col Tn A B P' *)
(* Goal: or (@Par Tn P P' X Y) (@eq (@Tpoint Tn) P P') *)
(* Goal: and (@Proj Tn P P' A B X Y) (forall (x' : @Tpoint Tn) (_ : @Proj Tn P x' A B X Y), @eq (@Tpoint Tn) P' x') *)
Par.
assert(Par_strict Q Q' R R').
induction H20.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.
(* Goal: @eq (@Tpoint Tn) P Q *)
apply False_ind.
apply H9.
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
eapply (project_col_eq R Q _ _ A B X Y); Col.
assert(OS Q Q' R R').
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
eapply (par_strict_one_side _ _ _ R'); Col.

assert(TS Q Q' P R').
apply l9_2.
eapply l9_8_2.
2:apply H22.
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
repeat split; Col.
(* Goal: not (@Col Tn C A B) *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
intro.
assert(Q'=R').
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
eapply (project_col_eq Q R _ _ A B X Y); Col.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
auto.
(* Goal: not (@Col Tn C A B) *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
intro.
assert(Q' = P).
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
eapply (project_col_eq Q P _ _ A B X Y); Col.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
auto.
exists Q.
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
split; Col.
Between.

unfold TS in H23.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.
ex_and H25 QQ.

assert(QQ=Q').
assert(Col P QQ R').
apply bet_col.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
eapply (l6_21 Q Q' P R'); Col.

(* Goal: not (@Col Tn C A B) *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
intro.
(* Goal: or (not (@eq (@Tpoint Tn) P A)) (not (@eq (@Tpoint Tn) P B)) *)
(* Goal: or (not (@eq (@Tpoint Tn) P A)) (not (@eq (@Tpoint Tn) P B)) *)
subst P.
apply between_equality in H26.
subst QQ.
(* Goal: not (@Col Tn A B P) *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
contradiction.
Between.
subst QQ.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.

subst R'.
apply par_distincts in H10.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.
assert(Q' = Q).

(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
eapply (l6_21 P R Q Q'); Col.
assert_cols.
(* Goal: not (@Col Tn C A B) *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
intro.
assert(~Col A B Q).
eapply project_not_col.
apply H1.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
auto.
assert(Col A P R).
(* Goal: @Col Tn P Q A *)
ColR.
assert(Col B P R).
(* Goal: @Col Tn P Q A *)
ColR.
apply H19.
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
eapply (col3 P R); Col.
(* Goal: not (@Col Tn C A B) *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
intro.
subst R.
apply between_identity in H.
(* Goal: not (@Col Tn A B P) *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
contradiction.
(* Goal: @eq (@Tpoint Tn) P Q' *)
subst Q'.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.
(* Goal: @eq (@Tpoint Tn) P Q' *)
subst Q'.
induction H7.

apply par_distincts in H7.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.

assert(R = R').

(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
eapply (l6_21 P Q R R'); Col.
apply bet_col in H.
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
Col.
(* Goal: not (@Col Tn C A B) *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
intro.
assert(~Col A B R).
eapply project_not_col.
(* Goal: False *)
(* Goal: @eq (@Tpoint Tn) P P' *)
apply H2.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
auto.
assert(Col A P Q).
(* Goal: @Col Tn P Q A *)
ColR.
assert(Col B P Q).
(* Goal: @Col Tn P Q A *)
ColR.
apply H18.
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
eapply (col3 P Q); Col.
(* Goal: not (@Col Tn A B P) *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
contradiction.
subst R'.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.
Qed.

Lemma triangle_par :
 forall A B C A' B' C',
 ~ Col A B C ->
  Par A B A' B' ->
  Par B C B' C' ->
  Par A C A' C' ->
 CongA A B C A' B' C'.
Proof.
(* Goal: forall (P P' A B : @Tpoint Tn) (_ : @Projp Tn P P' A B), @Projp Tn P' P' A B *)
intros.

assert(HH:=midpoint_existence B B').
ex_and HH M.
prolong A' M A'' A' M.
prolong C' M C'' C' M.

assert(Midpoint M A' A'')
 by (split;Cong).
assert(Midpoint M C' C'')
 by (split;Cong).

assert(A' <> B').
(* Goal: not (@Col Tn C A B) *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
intro.
subst A'.
apply par_distincts in H0.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
tauto.

assert(C' <> B').
(* Goal: not (@Col Tn C A B) *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
intro.
subst C'.
(* Goal: @Proj Tn P P' A B X Y *)
apply par_distincts in H1.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
tauto.

assert(Par B' C' B C'').
apply (l12_17 _ _ _ _ M); Midpoint.

assert(Col B B C /\ Col C'' B C).
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
apply(parallel_uniqueness B' C' B C B C'' B); Col.
(* Goal: not (@Par Tn A B X Y) *)
(* Goal: @Col Tn A B P' *)
(* Goal: or (@Par Tn P P' X Y) (@eq (@Tpoint Tn) P P') *)
(* Goal: and (@Proj Tn P P' A B X Y) (forall (x' : @Tpoint Tn) (_ : @Proj Tn P x' A B X Y), @eq (@Tpoint Tn) P' x') *)
Par.

assert(Par B' A' B A'').
apply (l12_17 _ _ _ _ M); Midpoint.
assert(Col B B A /\ Col A'' B A).
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
apply(parallel_uniqueness B' A' B A B A'' B); Col.
(* Goal: @Par Tn P P' X Y *)
(* Goal: and (@Proj Tn P P' A B X Y) (forall (x' : @Tpoint Tn) (_ : @Proj Tn P x' A B X Y), @eq (@Tpoint Tn) P' x') *)
apply par_symmetry.
(* Goal: @Par Tn C B C' B' *)
apply par_comm.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.

(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.
clear H13.
clear H15.

assert(CongA A' B' C' A'' B C'').

apply (symmetry_preserves_conga _ _ _ _ _ _ M); Midpoint.
eapply conga_trans.
2: apply conga_sym.
2:apply H13.

show_distinct B A''.
assert_diffs;intuition.

show_distinct B C''.
assert_diffs;intuition.

assert(A <> B).
apply par_distincts in H0.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
tauto.
assert(B <> C).
(* Goal: @Proj Tn P P' A B X Y *)
apply par_distincts in H1.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
tauto.

assert(Par A C A'' C'').
eapply par_trans.
(* Goal: False *)
(* Goal: @eq (@Tpoint Tn) P P' *)
apply H2.
eapply (l12_17 _ _ _ _ M); Midpoint.

(* Goal: not (@Col Tn C A B) *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
intro.
subst C'.
apply par_distincts in H2.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
tauto.

apply par_distincts in H21.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.


induction H17.
assert(Par_strict A C A'' C'').
induction H21.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.
(* Goal: @eq (@Tpoint Tn) P Q *)
apply False_ind.
(* Goal: False *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
apply H.

assert(C <> C'').
(* Goal: not (@Col Tn C A B) *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
intro.
subst C''.
apply between_identity in H17.
subst C.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
tauto.

assert(Col A C C'').
(* Goal: @Col Tn P Q A *)
ColR.
apply bet_col in H17.
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
apply (col3 C C''); Col.

induction H16.

apply(l11_14 A B C A'' C''); Between.

(* Goal: @eq (@Tpoint Tn) P Q *)
apply False_ind.

induction (eq_dec_points A A'').
subst A''.
apply H24.
exists A.
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
split; Col.

induction H16.

assert(TS A C A'' B).
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
repeat split; Col.
(* Goal: not (@Col Tn C A B) *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
intro.
(* Goal: False *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
apply H.
apply bet_col in H16.
apply bet_col in H17.
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
eapply (col3 A A''); Col.
exists A.
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
split; Col.
Between.

assert(OS A C B C'').
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
eapply (out_one_side_1 _ _ _ _ C); Col.
unfold Out.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
repeat split; auto.
(* Goal: not (@Col Tn C A B) *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
intro.
subst C''.
apply between_identity in H17.
subst C.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
tauto.
(* Goal: or (not (@eq (@Tpoint Tn) P A)) (not (@eq (@Tpoint Tn) P B)) *)
left.
Between.
assert(TS A C A'' C'').
apply l9_2.
eapply l9_8_2.
apply l9_2.
apply H26.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.
unfold TS in H28.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.
ex_and H30 T.
apply H24.
exists T.
apply bet_col in H31.
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
split; Col.

assert(TS A'' C'' A B).
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
repeat split; Col.
(* Goal: not (@Col Tn C A B) *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
intro.
(* Goal: False *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
apply H.
apply bet_col in H16.
apply bet_col in H17.

assert(Col A'' C'' B).
(* Goal: @Col Tn P Q A *)
ColR.
assert(Col A'' C'' C).
(* Goal: @Col Tn P Q A *)
ColR.
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
eapply (col3 A'' C''); Col.

(* Goal: not (@Col Tn C A B) *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
intro.
apply bet_col in H16.
apply bet_col in H17.
(* Goal: False *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
apply H.

assert(Col B C A'').
(* Goal: @Col Tn P Q A *)
ColR.
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
apply (col3 B A''); Col.

exists A''.
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
split; Col.

assert(OS A'' C'' B C).
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
apply out_one_side_1 with C''; Col.
(* Goal: not (@Col Tn C A B) *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
intro.
(* Goal: False *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
apply H.


apply bet_col in H16.
apply bet_col in H17.
assert(Col A'' B C).
(* Goal: @Col Tn P Q A *)
ColR.
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
apply (col3 A'' B); Col.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
repeat split; auto.
(* Goal: not (@Col Tn C A B) *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
intro.
subst.
unfold Par_strict in H24.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.
apply H29.
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
exists C''; Col.

assert(TS A'' C'' A C).
apply l9_2.
eapply l9_8_2.
apply l9_2.
apply H26.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.
unfold TS in H28.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.
ex_and H30 T.
apply H24.
exists T.
apply bet_col in H31.
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
split; Col.

induction H17.
induction H16.

assert(Par_strict A C A'' C'').
induction H21.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.
(* Goal: @eq (@Tpoint Tn) P Q *)
apply False_ind.
(* Goal: False *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
apply H.

assert(A <> A'').
(* Goal: not (@Col Tn C A B) *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
intro.
subst A''.
apply between_identity in H16.
(* Goal: not (@Col Tn A B P) *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
contradiction.

assert(Col C A A'').
(* Goal: @Col Tn P Q A *)
ColR.
apply bet_col in H16.
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
apply (col3 A A''); Col.


(* Goal: @eq (@Tpoint Tn) P Q *)
apply False_ind.

induction (eq_dec_points C C'').
subst C''.
apply H24.
exists C.
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
split; Col.

assert(TS A C C'' B).
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
repeat split; Col.
(* Goal: not (@Col Tn C A B) *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
intro.
(* Goal: False *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
apply H.
apply bet_col in H16.
apply bet_col in H17.
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
eapply (col3 C C''); Col.
exists C.
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
split; Col.
Between.

assert(OS A C B A'').
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
eapply (out_one_side _ _ _ _); Col.
unfold Out.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
repeat split; auto.
(* Goal: not (@Col Tn C A B) *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
intro.
subst A''.
apply between_identity in H16.
(* Goal: not (@Col Tn A B P) *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
contradiction.
(* Goal: or (not (@eq (@Tpoint Tn) P A)) (not (@eq (@Tpoint Tn) P B)) *)
left.
Between.
assert(TS A C A'' C'').

eapply l9_8_2.
apply l9_2.
apply H26.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.
unfold TS in H28.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.
ex_and H30 T.
apply H24.
exists T.
apply bet_col in H31.
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
split; Col.

induction H16.



eapply (out_conga A B C A B C).
apply conga_refl.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
auto.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
auto.
apply out_trivial.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
auto.
apply out_trivial.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
auto.
unfold Out.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
repeat split; auto.
unfold Out.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
repeat split; auto.

eapply (out_conga A B C A B C).
apply conga_refl.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
auto.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
auto.
apply out_trivial.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
auto.
apply out_trivial.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
auto.
unfold Out.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
repeat split; auto.
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
right.
Between.
unfold Out.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
repeat split; auto.

induction H16.

assert(Par_strict A C A'' C'').
induction H21.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.
(* Goal: @eq (@Tpoint Tn) P Q *)
apply False_ind.
(* Goal: False *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
apply H.

assert(A <> A'').
(* Goal: not (@Col Tn C A B) *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
intro.
subst A''.
apply between_identity in H16.
(* Goal: not (@Col Tn A B P) *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
contradiction.

assert(Col C A A'').
(* Goal: @Col Tn P Q A *)
ColR.
apply bet_col in H16.
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
apply (col3 A A''); Col.

(* Goal: @eq (@Tpoint Tn) P Q *)
apply False_ind.

induction (eq_dec_points C C'').
subst C''.
apply H24.
exists C.
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
split; Col.


assert(TS A'' C'' C B).
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
repeat split; Col.
(* Goal: not (@Col Tn C A B) *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
intro.
(* Goal: False *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
apply H.
apply bet_col in H16.
apply bet_col in H17.

assert(Col A'' C'' B).
(* Goal: @Col Tn P Q A *)
ColR.
assert(Col A'' C'' A).
(* Goal: @Col Tn P Q A *)
ColR.
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
eapply (col3 A'' C''); Col.

(* Goal: not (@Col Tn C A B) *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
intro.
apply bet_col in H16.
apply bet_col in H17.
(* Goal: False *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
apply H.

assert(Col B C A'').
(* Goal: @Col Tn P Q A *)
ColR.
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
apply (col3 B A''); Col.

exists C''.
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
split; Col.

assert(OS A'' C'' B A).
apply out_one_side.
(* Goal: or (not (@eq (@Tpoint Tn) P A)) (not (@eq (@Tpoint Tn) P B)) *)
left.
(* Goal: not (@Col Tn C A B) *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
intro.
(* Goal: False *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
apply H.

apply bet_col in H16.
apply bet_col in H17.
assert(Col C B A'').
(* Goal: @Col Tn P Q A *)
ColR.
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
apply (col3 A'' B); Col.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
repeat split; auto.

(* Goal: not (@Col Tn C A B) *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
intro.
subst.
unfold Par_strict in H24.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.
apply H29.
exists A''.
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
Col.

assert(TS A'' C'' A C).
eapply l9_8_2.
apply l9_2.
apply H26.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.
unfold TS in H28.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.
ex_and H30 T.
apply H24.
exists T.
apply bet_col in H31.
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
split; Col.

induction H16.

eapply (out_conga A B C A B C).
apply conga_refl.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
auto.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
auto.
apply out_trivial.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
auto.
apply out_trivial.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
auto.
unfold Out.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
repeat split; auto.
unfold Out.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
repeat split; auto.
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
right.
Between.

eapply (out_conga A B C A B C).
apply conga_refl.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
auto.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
auto.
apply out_trivial.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
auto.
apply out_trivial.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
auto.
unfold Out.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
repeat split; auto.
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
right.
Between.
unfold Out.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
repeat split; auto.
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
right.
Between.
Qed.

Lemma par3_conga3 :
 forall A B C A' B' C',
 ~ Col A B C ->
 Par A B A' B' ->
 Par B C B' C' ->
 Par A C A' C' ->
 CongA_3 A B C A' B' C'.
Proof.
(* Goal: forall (P P' A B : @Tpoint Tn) (_ : @Projp Tn P P' A B), @Projp Tn P' P' A B *)
intros.
(* Goal: @CongA_3 Tn A B C A' B' C' *)
unfold CongA_3.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
split.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
apply triangle_par; auto.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
split.
(* Goal: @CongA Tn C A B C' A' B' *)
apply triangle_par.
(* Goal: not (@Col Tn C A B) *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
intro.
(* Goal: False *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
apply H.
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
Col.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
auto.
(* Goal: @Par Tn C B C' B' *)
apply par_comm.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
auto.
(* Goal: @Par Tn C B C' B' *)
apply par_comm.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
auto.
(* Goal: @CongA Tn C A B C' A' B' *)
apply triangle_par.
(* Goal: not (@Col Tn C A B) *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
intro.
(* Goal: False *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
apply H.
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
Col.
(* Goal: @Par Tn C B C' B' *)
apply par_comm.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
auto.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
auto.
(* Goal: @Par Tn C B C' B' *)
apply par_comm.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
auto.
Qed.

Lemma cong_conga3_cong3 :
 forall A B C A' B' C',
 ~ Col A B C ->
 Cong A B A' B' ->
 CongA_3 A B C A' B' C' ->
 Cong_3 A B C A' B' C'.
Proof.
(* Goal: forall (P P' A B : @Tpoint Tn) (_ : @Projp Tn P P' A B), @Projp Tn P' P' A B *)
intros.
(* Goal: @Cong_3 Tn A B C A' B' C' *)
unfold CongA_3 in H1.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.
(* Goal: @Cong_3 Tn A B C A' B' C' *)
assert(Cong A C A' C' /\ Cong B C B' C' /\ CongA C A B C' A' B').
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
apply( l11_50_2 A B C A' B' C' H); auto.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
repeat split; auto.
Qed.

Lemma project_par_eqv :
 forall P P' Q Q' A B X Y,
 Proj P P' A B X Y ->
 Proj Q Q' A B X Y ->
 Par P Q A B ->
 EqV P Q P' Q'.
Proof.
(* Goal: forall (P P' A B : @Tpoint Tn) (_ : @Projp Tn P P' A B), @Projp Tn P' P' A B *)
intros.
(* Goal: @eq (@Tpoint Tn) P' Q' *)
assert(HH:=H).
(* Goal: @eq (@Tpoint Tn) P' Q' *)
assert(HH0:=H0).
(* Goal: @eq (@Tpoint Tn) P' Q' *)
unfold Proj in HH.
(* Goal: @eq (@Tpoint Tn) P' Q' *)
unfold Proj in HH0.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.
unfold EqV.
(* Goal: @Proj Tn P P' A B X Y *)
apply par_distincts in H1.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.

(* Goal: or (not (@eq (@Tpoint Tn) P A)) (not (@eq (@Tpoint Tn) P B)) *)
left.
induction H1.

(* Goal: @eq (@Tpoint Tn) P' Q' *)
induction H6; induction H11.
assert(Par P P' Q Q').
eapply par_trans.
apply H11.
(* Goal: not (@Par Tn A B X Y) *)
(* Goal: @Col Tn A B P' *)
(* Goal: or (@Par Tn P P' X Y) (@eq (@Tpoint Tn) P P') *)
(* Goal: and (@Proj Tn P P' A B X Y) (forall (x' : @Tpoint Tn) (_ : @Proj Tn P x' A B X Y), @eq (@Tpoint Tn) P' x') *)
Par.

assert(Par P' Q' A B ).
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
right.
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
repeat split; Col.
(* Goal: not (@Col Tn C A B) *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
intro.
(* Goal: @eq (@Tpoint Tn) P Q' *)
subst Q'.

induction H14.
(* Goal: False *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
apply H14.
(* Goal: @ex (@Tpoint Tn) (@unique (@Tpoint Tn) (fun P' : @Tpoint Tn => @Proj Tn P P' A B X Y)) *)
exists P'.
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
split; Col.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.

apply H1.
(* Goal: @ex (@Tpoint Tn) (@unique (@Tpoint Tn) (fun P' : @Tpoint Tn => @Proj Tn P P' A B X Y)) *)
exists P'.
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
split; Col.

(* Goal: @eq (@Tpoint Tn) P' Q' *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
clean_duplicated_hyps.

assert(Par P Q P' Q').
eapply par_trans.
(* Goal: or (not (@eq (@Tpoint Tn) P A)) (not (@eq (@Tpoint Tn) P B)) *)
left.
apply H1.
(* Goal: not (@Par Tn A B X Y) *)
(* Goal: @Col Tn A B P' *)
(* Goal: or (@Par Tn P P' X Y) (@eq (@Tpoint Tn) P P') *)
(* Goal: and (@Proj Tn P P' A B X Y) (forall (x' : @Tpoint Tn) (_ : @Proj Tn P x' A B X Y), @eq (@Tpoint Tn) P' x') *)
Par.

assert(Par_strict P Q P' Q').
apply par_symmetry in H2.
induction H2.
apply par_strict_symmetry.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.
(* Goal: @eq (@Tpoint Tn) P Q *)
apply False_ind.
apply H1.
(* Goal: @ex (@Tpoint Tn) (@unique (@Tpoint Tn) (fun P' : @Tpoint Tn => @Proj Tn P P' A B X Y)) *)
exists P'.
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
split; Col.

apply plg_to_parallelogram.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
apply pars_par_plg; auto.
apply par_strict_right_comm.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.

(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
subst P'.
(* Goal: @eq (@Tpoint Tn) P Q *)
apply False_ind.
apply H1.
exists P.
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
split; Col.
(* Goal: @eq (@Tpoint Tn) P Q' *)
subst Q'.
(* Goal: @eq (@Tpoint Tn) P Q *)
apply False_ind.
apply H1.
exists Q.
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
split; Col.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
subst P'.
(* Goal: @eq (@Tpoint Tn) P Q' *)
subst Q'.
apply plg_trivial.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.

(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.
assert(P = P' /\ Q = Q').
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
split; eapply (project_id A B X Y); Col.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
subst P'.
(* Goal: @eq (@Tpoint Tn) P Q' *)
subst Q'.
apply plg_trivial.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.
Qed.



Lemma eqv_project_eq_eq :
 forall P Q R S P' Q' S' A B X Y,
  EqV P Q R S ->
  Proj P P' A B X Y ->
  Proj Q Q' A B X Y ->
  Proj R P' A B X Y ->
  Proj S S' A B X Y ->
  Q' = S'.
Proof.
(* Goal: forall (P P' A B : @Tpoint Tn) (_ : @Projp Tn P P' A B), @Projp Tn P' P' A B *)
intros.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.

induction(eq_dec_points P Q).
subst Q.
apply null_vector in H.
subst S.

assert(Q' = P').
eapply project_uniqueness.
apply H1.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.
(* Goal: @eq (@Tpoint Tn) P Q' *)
subst Q'.

eapply project_uniqueness.
(* Goal: False *)
(* Goal: @eq (@Tpoint Tn) P P' *)
apply H2.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.

assert(R <> S).
(* Goal: not (@Col Tn C A B) *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
intro.
subst S.
(* Goal: False *)
apply H4.
eapply null_vector.
apply eqv_sym in H.
(* Goal: False *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
apply H.
assert(EqV P R Q S).
apply eqv_permut.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.

induction(eq_dec_points P R).
subst R.
apply null_vector in H6.
subst S.
eapply project_uniqueness.
apply H1.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.

assert( Q <> S).
(* Goal: not (@Col Tn C A B) *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
intro.
subst S.
apply eqv_sym in H6.
apply null_vector in H6.
(* Goal: not (@Col Tn A B P) *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
contradiction.

eapply project_par.
apply H1.
apply H3.

eapply par_trans.
(* Goal: @Par Tn P P' X Y *)
(* Goal: and (@Proj Tn P P' A B X Y) (forall (x' : @Tpoint Tn) (_ : @Proj Tn P x' A B X Y), @eq (@Tpoint Tn) P' x') *)
apply par_symmetry.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
apply eqv_par in H6; auto.
apply H6.
(* Goal: @Par Tn P P' X Y *)
unfold Proj in H0.
unfold Proj in H2.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.
induction H16; induction H12.

assert(Col R P P' /\ Col P' P P').

(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
apply(parallel_uniqueness X Y P P' R P' P'); Col.
(* Goal: not (@Par Tn A B X Y) *)
(* Goal: @Col Tn A B P' *)
(* Goal: or (@Par Tn P P' X Y) (@eq (@Tpoint Tn) P P') *)
(* Goal: and (@Proj Tn P P' A B X Y) (forall (x' : @Tpoint Tn) (_ : @Proj Tn P x' A B X Y), @eq (@Tpoint Tn) P' x') *)
Par.
(* Goal: not (@Par Tn A B X Y) *)
(* Goal: @Col Tn A B P' *)
(* Goal: or (@Par Tn P P' X Y) (@eq (@Tpoint Tn) P P') *)
(* Goal: and (@Proj Tn P P' A B X Y) (forall (x' : @Tpoint Tn) (_ : @Proj Tn P x' A B X Y), @eq (@Tpoint Tn) P' x') *)
Par.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.
clear H18.

(* Goal: @Par Tn A B X Y *)
(* Goal: @eq (@Tpoint Tn) P P' *)
eapply (par_col_par_2 _ P'); Col.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
subst P'.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
subst P'.
(* Goal: not (@Par Tn A B X Y) *)
(* Goal: @Col Tn A B P' *)
(* Goal: or (@Par Tn P P' X Y) (@eq (@Tpoint Tn) P P') *)
(* Goal: and (@Proj Tn P P' A B X Y) (forall (x' : @Tpoint Tn) (_ : @Proj Tn P x' A B X Y), @eq (@Tpoint Tn) P' x') *)
Par.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
subst P'.
subst R.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
tauto.
Qed.


Lemma eqv_eq_project :
  forall P Q R S P' Q' A B X Y,
  EqV P Q R S ->
  Proj P P' A B X Y ->
  Proj Q Q' A B X Y ->
  Proj R P' A B X Y ->
  Proj S Q' A B X Y.
Proof.
(* Goal: forall (P P' A B : @Tpoint Tn) (_ : @Projp Tn P P' A B), @Projp Tn P' P' A B *)
intros.
assert(HH1:=H1).
unfold Proj in HH1.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
repeat split; Col.
apply eqv_permut in H.

induction(eq_dec_points S Q').
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
right.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.
(* Goal: or (not (@eq (@Tpoint Tn) P A)) (not (@eq (@Tpoint Tn) P B)) *)
left.

induction(eq_dec_points P R).
subst R.
apply null_vector in H.
subst S.
unfold Proj in H1.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.
(* Goal: @eq (@Tpoint Tn) P' Q' *)
induction H11.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.
(* Goal: not (@Col Tn A B P) *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
contradiction.

(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
apply eqv_par in H; auto.

assert(Col P R P').
eapply ker_col.
(* Goal: False *)
apply H0.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.

(* Goal: @Par Tn P P' X Y *)
unfold Proj in H0.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.

induction H14.
assert(Par P R X Y).
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
apply (par_col_par_2 _ P'); Col.

induction H7.

assert(Col Q Q Q' /\ Col S Q Q').
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
apply(parallel_uniqueness X Y Q Q' Q S Q); Col.
(* Goal: not (@Par Tn A B X Y) *)
(* Goal: @Col Tn A B P' *)
(* Goal: or (@Par Tn P P' X Y) (@eq (@Tpoint Tn) P P') *)
(* Goal: and (@Proj Tn P P' A B X Y) (forall (x' : @Tpoint Tn) (_ : @Proj Tn P x' A B X Y), @eq (@Tpoint Tn) P' x') *)
Par.
eapply par_trans.
(* Goal: False *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
2: apply H.
(* Goal: not (@Par Tn A B X Y) *)
(* Goal: @Col Tn A B P' *)
(* Goal: or (@Par Tn P P' X Y) (@eq (@Tpoint Tn) P P') *)
(* Goal: and (@Proj Tn P P' A B X Y) (forall (x' : @Tpoint Tn) (_ : @Proj Tn P x' A B X Y), @eq (@Tpoint Tn) P' x') *)
Par.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.
(* Goal: @Par Tn A P X Y *)
apply par_left_comm.
(* Goal: @Par Tn P A X Y *)
eapply (par_col_par_2 _ Q); Col.
(* Goal: not (@Par Tn A B X Y) *)
(* Goal: @Col Tn A B P' *)
(* Goal: or (@Par Tn P P' X Y) (@eq (@Tpoint Tn) P P') *)
(* Goal: and (@Proj Tn P P' A B X Y) (forall (x' : @Tpoint Tn) (_ : @Proj Tn P x' A B X Y), @eq (@Tpoint Tn) P' x') *)
Par.

(* Goal: @eq (@Tpoint Tn) P Q' *)
subst Q'.
eapply par_trans.
(* Goal: @Par Tn A P X Y *)
apply par_left_comm.
(* Goal: @Par Tn P P' X Y *)
(* Goal: and (@Proj Tn P P' A B X Y) (forall (x' : @Tpoint Tn) (_ : @Proj Tn P x' A B X Y), @eq (@Tpoint Tn) P' x') *)
apply par_symmetry.
(* Goal: False *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
apply H.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
subst P'.

assert(Par P R X Y).
unfold Proj in H2.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.
induction H17.
(* Goal: not (@Par Tn A B X Y) *)
(* Goal: @Col Tn A B P' *)
(* Goal: or (@Par Tn P P' X Y) (@eq (@Tpoint Tn) P P') *)
(* Goal: and (@Proj Tn P P' A B X Y) (forall (x' : @Tpoint Tn) (_ : @Proj Tn P x' A B X Y), @eq (@Tpoint Tn) P' x') *)
Par.
subst R.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
tauto.


induction H7.
assert(Col Q Q Q' /\ Col S Q Q').
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
apply(parallel_uniqueness X Y Q Q' Q S Q); Col.
(* Goal: not (@Par Tn A B X Y) *)
(* Goal: @Col Tn A B P' *)
(* Goal: or (@Par Tn P P' X Y) (@eq (@Tpoint Tn) P P') *)
(* Goal: and (@Proj Tn P P' A B X Y) (forall (x' : @Tpoint Tn) (_ : @Proj Tn P x' A B X Y), @eq (@Tpoint Tn) P' x') *)
Par.
eapply par_trans.
(* Goal: @Par Tn P P' X Y *)
(* Goal: and (@Proj Tn P P' A B X Y) (forall (x' : @Tpoint Tn) (_ : @Proj Tn P x' A B X Y), @eq (@Tpoint Tn) P' x') *)
apply par_symmetry.
(* Goal: False *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
apply H14.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
apply (par_col_par_2 _ Q); Col.
eapply par_trans.
(* Goal: @Par Tn A P X Y *)
apply par_left_comm.
(* Goal: @Par Tn P P' X Y *)
(* Goal: and (@Proj Tn P P' A B X Y) (forall (x' : @Tpoint Tn) (_ : @Proj Tn P x' A B X Y), @eq (@Tpoint Tn) P' x') *)
apply par_symmetry.
(* Goal: False *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
apply H.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.
(* Goal: @eq (@Tpoint Tn) P Q' *)
subst Q'.
eapply par_trans.
(* Goal: @Par Tn P P' X Y *)
(* Goal: and (@Proj Tn P P' A B X Y) (forall (x' : @Tpoint Tn) (_ : @Proj Tn P x' A B X Y), @eq (@Tpoint Tn) P' x') *)
apply par_symmetry.
apply par_right_comm.
(* Goal: False *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
apply H.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.
Qed.


Lemma project_par_dir : forall P P' A B X Y, P <> P' -> Proj P P' A B X Y -> Par P P' X Y.
(* Goal: forall (P P' A B : @Tpoint Tn) (_ : @Projp Tn P P' A B), @Projp Tn P' P' A B *)
intros.
(* Goal: @Par Tn P P' X Y *)
unfold Proj in H0.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
induction H4; tauto.
Qed.

Lemma project_idem : forall P P' A B X Y, Proj P P' A B X Y -> Proj P' P' A B X Y.
(* Goal: forall (P P' A B : @Tpoint Tn) (_ : @Projp Tn P P' A B), @Projp Tn P' P' A B *)
intros.
(* Goal: @Proj Tn P' P' A B X Y *)
unfold Proj in *.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
repeat split; Col.
Qed.

Lemma eqv_cong : forall A B C D, EqV A B C D -> Cong A B C D.
(* Goal: forall (P P' A B : @Tpoint Tn) (_ : @Projp Tn P P' A B), @Projp Tn P' P' A B *)
intros.
(* Goal: @Cong Tn A B C D *)
unfold EqV in H.
(* Goal: @Cong Tn A B C D *)
induction H.
(* Goal: @Cong Tn A B C D *)
(* Goal: @Cong Tn A B C D *)
apply plg_cong.
(* Goal: @Parallelogram Tn A C D B *)
(* Goal: @Cong Tn A B C D *)
apply plg_permut.
(* Goal: @Parallelogram Tn B A C D *)
(* Goal: @Cong Tn A B C D *)
apply plg_comm2.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.
(* Goal: @Cong Tn A B C D *)
subst B.
(* Goal: @Cong Tn A A C D *)
subst D.
(* Goal: @Cong Tn A A C C *)
Cong.
Qed.

Lemma project_preserves_eqv :
 forall P Q R S P' Q' R' S' A B X Y, EqV P Q R S ->
  Proj P P' A B X Y ->
  Proj Q Q' A B X Y ->
  Proj R R' A B X Y ->
  Proj S S' A B X Y ->
  EqV P' Q' R' S'.
Proof.
(* Goal: forall (P P' A B : @Tpoint Tn) (_ : @Projp Tn P P' A B), @Projp Tn P' P' A B *)
intros.

induction (eq_dec_points P Q).
subst Q.
apply null_vector in H.
subst S.
assert(R'=S').
eapply project_uniqueness.
(* Goal: False *)
(* Goal: @eq (@Tpoint Tn) P P' *)
apply H2.
apply H3.
subst S'.
assert(P' = Q').
eapply project_uniqueness.
(* Goal: False *)
apply H0.
apply H1.
(* Goal: @eq (@Tpoint Tn) P Q' *)
subst Q'.
apply eqv_trivial.

assert(R <> S).
(* Goal: not (@Col Tn C A B) *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
intro.
subst S.
apply eqv_sym in H.
apply null_vector in H.
(* Goal: not (@Col Tn A B P) *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
contradiction.

induction (par_dec P Q A B).

assert(EqV P Q P' Q').
eapply project_par_eqv.
(* Goal: False *)
apply H0.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.

assert(EqV R S R' S').
eapply project_par_eqv.
(* Goal: False *)
(* Goal: @eq (@Tpoint Tn) P P' *)
apply H2.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.

eapply par_trans.
(* Goal: @Par Tn P P' X Y *)
(* Goal: and (@Proj Tn P P' A B X Y) (forall (x' : @Tpoint Tn) (_ : @Proj Tn P x' A B X Y), @eq (@Tpoint Tn) P' x') *)
apply par_symmetry.
apply eqv_par.
(* Goal: False *)
apply H4.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.
eapply eqv_trans.
apply eqv_sym.
apply H7.
eapply eqv_trans.
(* Goal: False *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
apply H.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.

induction (par_dec P Q X Y).
assert(P' = Q').
eapply project_par.
(* Goal: False *)
apply H0.
apply H1.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.

assert(Par R S X Y).
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
apply eqv_par in H; auto.
eapply par_trans.
(* Goal: @Par Tn P P' X Y *)
(* Goal: and (@Proj Tn P P' A B X Y) (forall (x' : @Tpoint Tn) (_ : @Proj Tn P x' A B X Y), @eq (@Tpoint Tn) P' x') *)
apply par_symmetry.
(* Goal: False *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
apply H.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.
assert(R' = S').
eapply project_par.
(* Goal: False *)
(* Goal: @eq (@Tpoint Tn) P P' *)
apply H2.
apply H3.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.
(* Goal: @eq (@Tpoint Tn) P Q' *)
subst Q'.
subst S'.
apply eqv_trivial.

assert(P' <> Q').
(* Goal: not (@Col Tn C A B) *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
intro.
(* Goal: @eq (@Tpoint Tn) P Q' *)
subst Q'.
apply H7.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
eapply (ker_par P Q P' A B); auto.

assert(~ Par R S X Y).
(* Goal: not (@Col Tn C A B) *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
intro.
apply H7.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
apply eqv_par in H; auto.
eapply par_trans.
(* Goal: False *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
apply H.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.

assert(R' <> S').
(* Goal: not (@Col Tn C A B) *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
intro.
subst S'.
apply H9.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
eapply (ker_par R S R' A B); auto.


assert(HH1:= vector_construction P Q P').
ex_and HH1 Q''.
assert(HH1:= vector_construction R S R').
ex_and HH1 S''.

assert(EqV P' Q'' R' S'').
eapply eqv_trans.
apply eqv_sym.
apply H11.
eapply eqv_trans.
(* Goal: False *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
apply H.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.

assert(Q' <> Q'').
(* Goal: not (@Col Tn C A B) *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
intro.
apply H6.
subst Q''.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
apply eqv_par in H; auto.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
apply eqv_par in H11; auto.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
apply eqv_par in H12; auto.
assert(P' <> Q').
(* Goal: not (@Col Tn C A B) *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
intro.
(* Goal: @eq (@Tpoint Tn) P Q' *)
subst Q'.
(* Goal: @eq (@Tpoint Tn) P' Q' *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
apply par_distincts in H11.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
tauto.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
apply eqv_par in H13; auto.
assert(Par P' Q' A B).
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
right.
(* Goal: @Proj Tn P' P' A B X Y *)
unfold Proj in *.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
repeat split; Col.

eapply par_trans.
(* Goal: False *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
apply H.
eapply par_trans.
apply H12.
eapply par_trans.
(* Goal: @Par Tn P P' X Y *)
(* Goal: and (@Proj Tn P P' A B X Y) (forall (x' : @Tpoint Tn) (_ : @Proj Tn P x' A B X Y), @eq (@Tpoint Tn) P' x') *)
apply par_symmetry.
apply H13.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.

assert(S' <> S'').
(* Goal: not (@Col Tn C A B) *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
intro.
subst S''.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
apply eqv_par in H; auto.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
apply eqv_par in H11; auto.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
apply eqv_par in H12; auto.
assert(R' <> S').
(* Goal: not (@Col Tn C A B) *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
intro.
subst S'.
apply par_distincts in H12.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
tauto.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
apply eqv_par in H13; auto.
assert(Par R' S' A B).
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
right.
(* Goal: @Proj Tn P' P' A B X Y *)
unfold Proj in *.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
repeat split; Col.
apply H6.

eapply par_trans.
(* Goal: False *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
apply H.
eapply par_trans.
apply H12.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.
(* Goal: not (@Col Tn C A B) *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
intro.
subst Q''.
apply null_vector in H13.
subst S'.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
tauto.

assert(HP1:=eqv_permut P Q P' Q'' H11).
assert(HP2:=eqv_permut R S R'  S'' H12).
assert(HP3:=eqv_permut P' Q'' R'  S'' H13).

assert(Proj Q'' Q' A B X Y).
eapply eqv_eq_project.
apply H11.
(* Goal: False *)
apply H0.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.
eapply project_idem.
(* Goal: False *)
apply H0.

assert(Proj S'' S' A B X Y).
eapply eqv_eq_project.
apply H12.
(* Goal: False *)
(* Goal: @eq (@Tpoint Tn) P P' *)
apply H2.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.
eapply project_idem.
(* Goal: False *)
(* Goal: @eq (@Tpoint Tn) P P' *)
apply H2.
assert(HH1:= H16).
assert(HH2:= H17).
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
eapply project_par_dir in HH1; auto.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
apply project_par_dir in HH2; auto.

assert(Par Q'' Q' S'' S').
eapply par_trans.
apply HH1.
(* Goal: not (@Par Tn A B X Y) *)
(* Goal: @Col Tn A B P' *)
(* Goal: or (@Par Tn P P' X Y) (@eq (@Tpoint Tn) P P') *)
(* Goal: and (@Proj Tn P P' A B X Y) (forall (x' : @Tpoint Tn) (_ : @Proj Tn P x' A B X Y), @eq (@Tpoint Tn) P' x') *)
Par.
assert(~ Col A B Q'').
apply(project_not_col A B X Y Q'' Q' H16).
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
auto.
assert(~ Col P' Q'' Q').
(* Goal: not (@Col Tn C A B) *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
intro.
apply H19.
(* Goal: @Proj Tn P' P' A B X Y *)
unfold Proj in *.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.
assert(Col P' Q' A).
(* Goal: @Col Tn P Q A *)
ColR.
assert(Col P' Q' B).
(* Goal: @Col Tn P Q A *)
ColR.
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
apply (col3 P' Q'); Col.

assert(Cong_3 P' Q'' Q' R' S'' S').
eapply cong_conga3_cong3.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.

apply eqv_cong.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.

eapply par3_conga3.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.
apply eqv_par.
(* Goal: not (@Col Tn C A B) *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
intro.
subst Q''.
apply H20.
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
Col.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
right.
(* Goal: @Proj Tn P' P' A B X Y *)
unfold Proj in *.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
repeat split; try assumption.

(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
apply (col3 A B); Col.
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
apply (col3 A B); Col.

assert(EqV Q'' Q' S'' S').
unfold EqV.
(* Goal: or (not (@eq (@Tpoint Tn) P A)) (not (@eq (@Tpoint Tn) P B)) *)
left.

induction(eq_dec_points Q' S').
subst S'.

assert(P' = R').

(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
apply (eqv_project_eq_eq Q'' P' S'' R' Q' P' R' A B X Y); auto.
apply eqv_comm.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.
eapply project_idem.
(* Goal: False *)
apply H0.
eapply project_idem.
(* Goal: False *)
(* Goal: @eq (@Tpoint Tn) P P' *)
apply H2.
subst R'.
apply null_vector in HP3.
subst S''.
apply plg_trivial.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
auto.


induction(eq_dec_points P' R').
subst R'.
apply null_vector in  HP3.
subst S''.

assert(Q' = S').
eapply eqv_project_eq_eq.
apply H13.
(* Goal: False *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
2:apply H16.
eapply project_idem.
(* Goal: False *)
apply H0.
eapply project_idem.
(* Goal: False *)
apply H0.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.
subst S'.
apply plg_trivial.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
auto.

apply plg_to_parallelogram.
unfold Plg.

(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
split.
(* Goal: or (not (@eq (@Tpoint Tn) P A)) (not (@eq (@Tpoint Tn) P B)) *)
left.
(* Goal: not (@Col Tn C A B) *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
intro.
subst Q''.
apply H19.
(* Goal: @Proj Tn P' P' A B X Y *)
unfold Proj in *.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
Col.

eapply par_cong_mid_os.
induction H18.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.
(* Goal: @eq (@Tpoint Tn) P Q *)
apply False_ind.

assert(~ Col A B S'').
apply(project_not_col A B X Y S'' S' H17).
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
auto.

apply H27.

(* Goal: @Proj Tn P' P' A B X Y *)
unfold Proj in *.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.
assert(Col Q' S' A).
(* Goal: @Col Tn P Q A *)
ColR.
assert(Col Q' S' B).
(* Goal: @Col Tn P Q A *)
ColR.
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
apply (col3 Q' S'); Col.
unfold Cong_3 in H21.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.
(* Goal: @Cong Tn A A C C *)
Cong.
unfold EqV in H13.
induction H13.

apply plg_permut in H13.

assert(Parallelogram_strict  R' P' Q'' S'').
apply plg_sym in H13.
induction H13.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.
unfold Parallelogram_flat in H13.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.
(* Goal: @eq (@Tpoint Tn) P Q *)
apply False_ind.
apply H19.

(* Goal: @Proj Tn P' P' A B X Y *)
unfold Proj in *.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.

assert(Col P' R' A).
(* Goal: @Col Tn P Q A *)
ColR.
assert(Col P' R' B).
(* Goal: @Col Tn P Q A *)
ColR.
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
apply (col3 P' R'); Col.

assert(HH:= plgs_par_strict R' P' Q'' S'' H24).
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.

assert(Par_strict Q'' S'' Q' S').
eapply par_strict_col2_par_strict.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
auto.
apply par_strict_symmetry.
apply H25.
(* Goal: @Proj Tn P' P' A B X Y *)
unfold Proj in *.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
apply (col3 A B); Col.
(* Goal: @Proj Tn P' P' A B X Y *)
unfold Proj in *.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
apply (col3 A B); Col.
apply l12_6.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.

(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.
subst Q''.
(* Goal: @eq (@Tpoint Tn) P Q *)
apply False_ind.
apply H20.
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
Col.

eapply eqv_sum.
apply H13.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.
Qed.

Lemma perp_projp : forall P P' A B, Perp_at P' A B P P' -> Projp P P' A B.
(* Goal: forall (P P' A B : @Tpoint Tn) (_ : @Projp Tn P P' A B), @Projp Tn P' P' A B *)
intros.
(* Goal: @Projp Tn P P' A B *)
unfold Projp.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
split.
(* Goal: @Perp Tn A B P P' *)
apply l8_14_2_1a in H.
(* Goal: not (@eq (@Tpoint Tn) A B) *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P P')) (and (@Col Tn A B P) (@eq (@Tpoint Tn) P P')) *)
apply perp_not_eq_1 in H.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.
(* Goal: or (not (@eq (@Tpoint Tn) P A)) (not (@eq (@Tpoint Tn) P B)) *)
left.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
split.
(* Goal: @Col Tn A B P' *)
(* Goal: @Perp Tn A B P P' *)
apply perp_in_col in H.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.
(* Goal: @Perp Tn A B P P' *)
apply l8_14_2_1a in H.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.
Qed.

Lemma proj_distinct : forall P P' A B, Projp P P' A B -> P' <> A \/ P' <> B.
(* Goal: forall (P P' A B : @Tpoint Tn) (_ : @Projp Tn P P' A B), @Projp Tn P' P' A B *)
intros.
(* Goal: or (not (@eq (@Tpoint Tn) P' A)) (not (@eq (@Tpoint Tn) P' B)) *)
unfold Projp in H.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
induction H0.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.
(* Goal: or (not (@eq (@Tpoint Tn) P' A)) (not (@eq (@Tpoint Tn) P' B)) *)
(* Goal: or (not (@eq (@Tpoint Tn) P' A)) (not (@eq (@Tpoint Tn) P' B)) *)
induction(eq_dec_points P' A).
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
subst P'.
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
right.
(* Goal: not (@eq (@Tpoint Tn) A B) *)
(* Goal: or (not (@eq (@Tpoint Tn) P' A)) (not (@eq (@Tpoint Tn) P' B)) *)
(* Goal: or (not (@eq (@Tpoint Tn) P' A)) (not (@eq (@Tpoint Tn) P' B)) *)
apply perp_not_eq_1 in H1.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.
(* Goal: or (not (@eq (@Tpoint Tn) P A)) (not (@eq (@Tpoint Tn) P B)) *)
left.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.

(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
subst P'.
(* Goal: or (not (@eq (@Tpoint Tn) P A)) (not (@eq (@Tpoint Tn) P B)) *)
induction(eq_dec_points P A).
(* Goal: or (not (@eq (@Tpoint Tn) P A)) (not (@eq (@Tpoint Tn) P B)) *)
(* Goal: or (not (@eq (@Tpoint Tn) P A)) (not (@eq (@Tpoint Tn) P B)) *)
subst P.
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
right.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.
(* Goal: or (not (@eq (@Tpoint Tn) P A)) (not (@eq (@Tpoint Tn) P B)) *)
left.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.
Qed.

Lemma projp_is_project :
 forall P P' A B,
  Projp P P' A B ->
  exists X, exists Y, Proj P P' A B X Y.
Proof.
(* Goal: forall (P P' A B : @Tpoint Tn) (_ : @Projp Tn P P' A B), @Projp Tn P' P' A B *)
intros.

assert(A <> B).
(* Goal: or (not (@eq (@Tpoint Tn) P' A)) (not (@eq (@Tpoint Tn) P' B)) *)
unfold Projp in H.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
tauto.
assert(HH:=perp_vector A B H0).
ex_and HH X.
ex_and H1 Y.
exists X.
exists Y.

assert(X <> Y).
apply perp_not_eq_2 in H2.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.

(* Goal: @Proj Tn P P' A B X Y *)
unfold Proj.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
repeat split; auto.
apply perp_not_par.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.
(* Goal: or (not (@eq (@Tpoint Tn) P' A)) (not (@eq (@Tpoint Tn) P' B)) *)
unfold Projp in H.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.
induction H3.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
tauto.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
subst P'.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.

(* Goal: or (not (@eq (@Tpoint Tn) P' A)) (not (@eq (@Tpoint Tn) P' B)) *)
unfold Projp in H.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.
induction H3.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.
(* Goal: or (not (@eq (@Tpoint Tn) P A)) (not (@eq (@Tpoint Tn) P B)) *)
left.
eapply l12_9_2D.
apply perp_sym.
(* Goal: False *)
apply H4.
Perp.
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
right.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
tauto.
Qed.

Lemma projp_is_project_perp :
 forall P P' A B,
 Projp P P' A B ->
 exists X, exists Y, Proj P P' A B X Y /\ Perp A B X Y.
Proof.
(* Goal: forall (P P' A B : @Tpoint Tn) (_ : @Projp Tn P P' A B), @Projp Tn P' P' A B *)
intros.

assert(A <> B).
(* Goal: or (not (@eq (@Tpoint Tn) P' A)) (not (@eq (@Tpoint Tn) P' B)) *)
unfold Projp in H.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
tauto.
assert(HH:=perp_vector A B H0).
ex_and HH X.
ex_and H1 Y.
exists X.
exists Y.

assert(X <> Y).
apply perp_not_eq_2 in H2.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
split.

(* Goal: @Proj Tn P P' A B X Y *)
unfold Proj.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
repeat split; auto.
apply perp_not_par.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.
(* Goal: or (not (@eq (@Tpoint Tn) P' A)) (not (@eq (@Tpoint Tn) P' B)) *)
unfold Projp in H.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.
induction H3.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
tauto.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
subst P'.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.

(* Goal: or (not (@eq (@Tpoint Tn) P' A)) (not (@eq (@Tpoint Tn) P' B)) *)
unfold Projp in H.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.
induction H3.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.
(* Goal: or (not (@eq (@Tpoint Tn) P A)) (not (@eq (@Tpoint Tn) P B)) *)
left.
eapply l12_9_2D.
apply perp_sym.
(* Goal: False *)
apply H4.
Perp.
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
right.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
tauto.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.
Qed.

Lemma projp_to_project :
 forall P P' A B X Y,
  Perp A B X Y ->
  Projp P P' A B ->
  Proj P P' A B X Y.
Proof.
(* Goal: forall (P P' A B : @Tpoint Tn) (_ : @Projp Tn P P' A B), @Projp Tn P' P' A B *)
intros.
(* Goal: @Proj Tn P P' A B X Y *)
unfold Proj.

(* Goal: and (not (@eq (@Tpoint Tn) A B)) (and (not (@eq (@Tpoint Tn) X Y)) (and (not (@Par Tn A B X Y)) (and (@Col Tn A B P') (or (@Par Tn P P' X Y) (@eq (@Tpoint Tn) P P'))))) *)
(* Goal: and (@Proj Tn P P' A B X Y) (forall (x' : @Tpoint Tn) (_ : @Proj Tn P x' A B X Y), @eq (@Tpoint Tn) P' x') *)
repeat split.
eapply perp_not_eq_1.
(* Goal: False *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
apply H.
eapply perp_not_eq_2.
(* Goal: False *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
apply H.
apply perp_not_par.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.
unfold Projp in H0.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.
induction H1.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
subst P'.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.
unfold Projp in H0.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.
induction H1.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.
(* Goal: or (not (@eq (@Tpoint Tn) P A)) (not (@eq (@Tpoint Tn) P B)) *)
left.
eapply l12_9_2D.
apply perp_sym.
(* Goal: False *)
(* Goal: @eq (@Tpoint Tn) P P' *)
apply H2.
Perp.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
right.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.
Qed.

Lemma project_to_projp :
 forall P P' A B X Y,
  Proj P P' A B X Y ->
  Perp A B X Y ->
  Projp P P' A B.
Proof.
(* Goal: forall (P P' A B : @Tpoint Tn) (_ : @Projp Tn P P' A B), @Projp Tn P' P' A B *)
intros.
(* Goal: @Col Tn A B P *)
unfold Proj in H.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.
(* Goal: @Projp Tn P P' A B *)
unfold Projp.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
split.
apply perp_not_eq_1 in H0.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.
(* Goal: not (@Col Tn A B P) *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
induction H4.
(* Goal: or (not (@eq (@Tpoint Tn) P A)) (not (@eq (@Tpoint Tn) P B)) *)
left.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
split.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.
apply perp_sym.

eapply par_perp__perp.
(* Goal: @Par Tn P P' X Y *)
(* Goal: and (@Proj Tn P P' A B X Y) (forall (x' : @Tpoint Tn) (_ : @Proj Tn P x' A B X Y), @eq (@Tpoint Tn) P' x') *)
apply par_symmetry.
(* Goal: False *)
apply H4.
Perp.
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
right.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
subst P'.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
split; auto.
Qed.

Lemma projp_project_to_perp :
 forall P P' A B X Y,
 P <> P' ->
 Projp P P' A B ->
 Proj P P' A B X Y ->
 Perp A B X Y.
Proof.
(* Goal: forall (P P' A B : @Tpoint Tn) (_ : @Projp Tn P P' A B), @Projp Tn P' P' A B *)
intros.
unfold Projp in H0.
unfold Proj in H1.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.
induction H6;
induction H5.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.
apply perp_sym.
eapply par_perp__perp.
apply H5.
Perp.
(* Goal: not (@Col Tn A B P) *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
contradiction.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.
(* Goal: not (@Col Tn A B P) *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
contradiction.
(* Goal: not (@Col Tn A B P) *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
contradiction.
Qed.

Lemma project_par_project :
 forall P P' A B X Y X' Y',
  Proj P P' A B X Y ->
  Par X Y X' Y' ->
  Proj P P' A B X' Y'.
Proof.
(* Goal: forall (P P' A B : @Tpoint Tn) (_ : @Projp Tn P P' A B), @Projp Tn P' P' A B *)
intros.
(* Goal: @Proj Tn P' P' A B X Y *)
unfold Proj in *.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.
apply par_distincts in H0.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
repeat split; Col.
(* Goal: not (@Col Tn C A B) *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
intro.
(* Goal: False *)
(* Goal: @eq (@Tpoint Tn) P P' *)
apply H2.
eapply par_trans.
apply H7.
(* Goal: not (@Par Tn A B X Y) *)
(* Goal: @Col Tn A B P' *)
(* Goal: or (@Par Tn P P' X Y) (@eq (@Tpoint Tn) P P') *)
(* Goal: and (@Proj Tn P P' A B X Y) (forall (x' : @Tpoint Tn) (_ : @Proj Tn P x' A B X Y), @eq (@Tpoint Tn) P' x') *)
Par.
(* Goal: not (@Col Tn A B P) *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
induction H4.
(* Goal: or (not (@eq (@Tpoint Tn) P A)) (not (@eq (@Tpoint Tn) P B)) *)
left.
eapply par_trans.
(* Goal: False *)
apply H4.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
right.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.
Qed.

Lemma project_project_par :
 forall P P' A B X Y X' Y',
 P <> P' ->
 Proj P P' A B X Y ->
 Proj P P' A B X' Y' ->
 Par X Y X' Y'.
Proof.
(* Goal: forall (P P' A B : @Tpoint Tn) (_ : @Projp Tn P P' A B), @Projp Tn P' P' A B *)
intros.
(* Goal: @Proj Tn P' P' A B X Y *)
unfold Proj in *.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.
induction H9;
induction H5;
(* Goal: not (@Col Tn A B P) *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
try contradiction.

eapply par_trans.
(* Goal: @Par Tn P P' X Y *)
(* Goal: and (@Proj Tn P P' A B X Y) (forall (x' : @Tpoint Tn) (_ : @Proj Tn P x' A B X Y), @eq (@Tpoint Tn) P' x') *)
apply par_symmetry.
apply H9.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.
Qed.

Lemma projp_id : forall P P' Q' A B, Projp P P' A B -> Projp P Q' A B -> P' = Q'.
(* Goal: forall (P P' A B : @Tpoint Tn) (_ : @Projp Tn P P' A B), @Projp Tn P' P' A B *)
intros.
(* Goal: @Par Tn A A' B B' *)
unfold Projp in *.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.
induction H1; induction H2.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
apply (l8_18_uniqueness A B P); Col.
(* Goal: @eq (@Tpoint Tn) P' P *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
apply perp_not_col2 in H4.
(* Goal: not (@Col Tn A B P) *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
induction H4.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.
(* Goal: not (@Col Tn A B P) *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
contradiction.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
subst P'.
(* Goal: @eq (@Tpoint Tn) P Q' *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
apply perp_not_col2 in H3.

(* Goal: not (@Col Tn A B P) *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
induction H3; contradiction.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.
(* Goal: @eq (@Tpoint Tn) P Q' *)
subst Q'.
(* Goal: @eq (@Tpoint Tn) P' P *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
apply perp_not_col2 in H4.
(* Goal: not (@Col Tn A B P) *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
(* Goal: @eq (@Tpoint Tn) P' Q' *)
induction H4; contradiction.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
subst P'.
(* Goal: @eq (@Tpoint Tn) P Q' *)
subst Q'.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
auto.
Qed.

Lemma projp_preserves_bet :
 forall A B C A' B' C' X Y,
  Bet A B C ->
  Projp A A' X Y ->
  Projp B B' X Y ->
  Projp C C' X Y ->
  Bet A' B' C'.
Proof.
(* Goal: forall (P P' A B : @Tpoint Tn) (_ : @Projp Tn P P' A B), @Projp Tn P' P' A B *)
intros.

eapply projp_is_project_perp in H0.
ex_and H0 T.
ex_and H3 U.

eapply (project_preserves_bet X Y T U A B C A' B' C').
(* Goal: False *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
apply H.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.
eapply projp_to_project in H1.
apply H1.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.
eapply projp_to_project in H2.
(* Goal: False *)
(* Goal: @eq (@Tpoint Tn) P P' *)
apply H2.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.
Qed.


Lemma projp_preserves_eqv :
 forall A B C A' B' C' D D' X Y,
 EqV A B C D ->
 Projp A A' X Y ->
 Projp B B' X Y ->
 Projp C C' X Y ->
 Projp D D' X Y ->
 EqV A' B' C' D'.
Proof.
(* Goal: forall (P P' A B : @Tpoint Tn) (_ : @Projp Tn P P' A B), @Projp Tn P' P' A B *)
intros.

eapply projp_is_project_perp in H0.
ex_and H0 T.
ex_and H4 U.

eapply (project_preserves_eqv A B C D A' B' C' D' X Y T U).
(* Goal: False *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
apply H.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.
eapply projp_to_project in H1.
apply H1.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
auto.
eapply projp_to_project in H2.
(* Goal: False *)
(* Goal: @eq (@Tpoint Tn) P P' *)
apply H2.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
auto.
eapply projp_to_project in H3.
apply H3.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
auto.
Qed.

Lemma projp_idem : forall P P' A B,
 Projp P P' A B ->
 Projp P' P' A B.
Proof.
(* Goal: forall (P P' A B : @Tpoint Tn) (_ : @Projp Tn P P' A B), @Projp Tn P' P' A B *)
intros.
(* Goal: @Par Tn A A' B B' *)
unfold Projp in *.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
split.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
auto.
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
induction H0.
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
right.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
split.
(* Goal: @Col Tn A B P' *)
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
assumption.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
auto.
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
right.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
spliter.
(* Goal: and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P') *)
subst P'.
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
tauto.
Qed.

Lemma projp2_col : forall A B C P Q,
  Projp P A B C -> Projp Q A B C -> Col A P Q.
Proof.
(* Goal: forall (A B C P Q : @Tpoint Tn) (_ : @Projp Tn P A B C) (_ : @Projp Tn Q A B C), @Col Tn A P Q *)
intros A B C P Q H1 H2.
destruct H1 as [H1 H3]; destruct H2 as [H2 H4];
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
induction H3; induction H4; spliter; treat_equalities; Col.
apply perp2__col with B C; Perp.
Qed.

Lemma projp_projp_perp : forall P P1 P2 Q1 Q2,
  P1 <> P2 -> Projp P1 P Q1 Q2 -> Projp P2 P Q1 Q2 -> Perp P1 P2 Q1 Q2.
Proof.
(* Goal: forall (P P1 P2 Q1 Q2 : @Tpoint Tn) (_ : not (@eq (@Tpoint Tn) P1 P2)) (_ : @Projp Tn P1 P Q1 Q2) (_ : @Projp Tn P2 P Q1 Q2), @Perp Tn P1 P2 Q1 Q2 *)
intros P P1 P2 Q1 Q2 HP1P2 H1 H2.
(* Goal: @Perp Tn P1 P2 Q1 Q2 *)
destruct H1 as [H H1]; clear H; destruct H2 as [H H2]; clear H.
elim H1; clear H1; intro H1; elim H2; clear H2; intro H2;
spliter; treat_equalities; Perp; [|intuition].
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
apply perp_sym; apply perp_col0 with P1 P; Perp; Col.
apply col_permutation_2; apply perp2__col with Q1 Q2; Perp.
Qed.

Lemma col_projp_eq : forall A B P P', Col A B P -> Projp P P' A B -> P = P'.
Proof.
(* Goal: forall (A B P P' : @Tpoint Tn) (_ : @Col Tn A B P) (_ : @Projp Tn P P' A B), @eq (@Tpoint Tn) P P' *)
intros A B P P' HCol1 HProjp.
destruct HProjp as [HDiff HProjp]; elim HProjp; clear HProjp; intro HProjp;
[exfalso;  destruct HProjp as [HCol2 HPerp]|spliter; auto].
(* Goal: False *)
apply perp_not_col2 in HPerp; induction HPerp; intuition.
Qed.

Lemma projp_col : forall A B P P', Projp P P' A B -> Col A B P'.
Proof.
intros A B P P' H; destruct H as [H' H]; clear H'.
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
induction H; spliter; treat_equalities; Col.
Qed.

Lemma perp_projp2_eq : forall A A' B B' C D,
  Projp A A' C D ->
  Projp B B' C D ->
  Perp A B C D ->
  A' = B'.
Proof.
intros A A' B B' C D HA' HB' HPerp.
destruct HA' as [H HA']; clear H; destruct HB' as [H HB']; clear H.
elim HA'; clear HA'; intro HA'; elim HB'; clear HB'; intro HB'.

(* Goal: @Cong Tn A B A' B' *)
  {
  destruct HA' as [HColA' HA']; destruct HB' as [HColB' HB'].
  elim (perp_not_col2 A B C D HPerp); intro HNC.

(* Goal: @Cong Tn A B A' B' *)
    {
    apply l6_21 with A B C D; Col; try (intro; assert_diffs; intuition).

(* Goal: @Cong Tn A B A' B' *)
      {
      assert (HPar : Par A B A A')
        by (apply l12_9_2D with C D; Perp).
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
      elim HPar; clear HPar; intro HPar; [exfalso; apply HPar; exists A|spliter]; Col.
      }

(* Goal: @Cong Tn A B A' B' *)
      {
      assert (HPar : Par A B B B')
        by (apply l12_9_2D with C D; Perp).
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
      elim HPar; clear HPar; intro HPar; [exfalso; apply HPar; exists B|spliter]; Col.
      }
    }

(* Goal: @Cong Tn A B A' B' *)
    {
    apply l6_21 with A B D C; Col; try (intro; assert_diffs; intuition).

(* Goal: @Cong Tn A B A' B' *)
      {
      assert (HPar : Par A B A A')
        by (apply l12_9_2D with C D; Perp).
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
      elim HPar; clear HPar; intro HPar; [exfalso; apply HPar; exists A|spliter]; Col.
      }

(* Goal: @Cong Tn A B A' B' *)
      {
      assert (HPar : Par A B B B')
        by (apply l12_9_2D with C D; Perp).
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
      elim HPar; clear HPar; intro HPar; [exfalso; apply HPar; exists B|spliter]; Col.
      }
    }
  }

(* Goal: @Cong Tn A B A' B' *)
  {
  destruct HB' as [HColB H]; treat_equalities.
  apply perp_sym in HPerp; elim (perp_not_col2 C D A B HPerp);
  intro HNC; [|intuition]; destruct HA' as [HColA' HA'].
  apply l6_21 with C D A B; Col; try (intro; assert_diffs; intuition).
  assert (HPar : Par A B A A')
    by (apply l12_9_2D with C D; Perp).
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
  elim HPar; clear HPar; intro HPar; [exfalso; apply HPar; exists A|spliter]; Col.
  }

(* Goal: @Cong Tn A B A' B' *)
  {
  destruct HA' as [HColA H]; treat_equalities.
  apply perp_sym in HPerp; elim (perp_not_col2 C D A B HPerp);
  intro HNC; [intuition|]; destruct HB' as [HColB' HB'].
  apply l6_21 with C D B A; Col; try (intro; assert_diffs; intuition).
  assert (HPar : Par A B B B')
    by (apply l12_9_2D with C D; Perp).
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
  elim HPar; clear HPar; intro HPar; [exfalso; apply HPar; exists B|spliter]; Col.
  }

(* Goal: @Cong Tn A B A' B' *)
  {
  spliter; treat_equalities; apply perp_sym in HPerp;
  elim (perp_not_col2 C D A B HPerp); intuition.
  }
Qed.

Lemma col_par_projp2_eq : forall L11 L12 L21 L22 P P' P'',
  Col L11 L12 P ->
  Par L11 L12 L21 L22 ->
  Projp P P' L21 L22 -> Projp P' P'' L11 L12 ->
  P = P''.
Proof.
intros L11 L12 L21 L22 P P' P'' HCol1 HPar HP' HP''.
destruct HP' as [HDiff1 HP']; destruct HP'' as [HDiff2 HP''].
elim HP'; clear HP'; intro HP'; elim HP''; clear HP''; intro HP''.

(* Goal: @Cong Tn A B A' B' *)
  {
  destruct HP' as [HCol2 HPerp1]; destruct HP'' as [HCol3 HPerp2].
  assert (H : Par P P' P' P'').
(* Goal: @Cong Tn A B A' B' *)
    {
    apply l12_9_2D with L11 L12; Perp.
(* Goal: not (@Par Tn A B X Y) *)
(* Goal: @Col Tn A B P' *)
(* Goal: or (@Par Tn P P' X Y) (@eq (@Tpoint Tn) P P') *)
(* Goal: and (@Proj Tn P P' A B X Y) (forall (x' : @Tpoint Tn) (_ : @Proj Tn P x' A B X Y), @eq (@Tpoint Tn) P' x') *)
    apply perp_sym; apply par_perp__perp with L21 L22; Par.
    }
  elim H; clear H; intro H; [exfalso; apply H; exists P'; Col|].
  destruct H as [HDiff3 [HDiff4 [HCol4 H]]]; clear H.
  elim (perp_not_col2 L11 L12 P' P'' HPerp2); [intro HNC|intuition].
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
  apply l6_21 with L11 L12 P' P; Col.
  }

(* Goal: @Cong Tn A B A' B' *)
  {
  destruct HP' as [HCol2 HPerp1]; destruct HP'' as [HCol3 HPerp2]; treat_equalities.
  assert (HPerp2 : Perp L11 L12 P' P)
    by (apply par_perp__perp with L21 L22; Par; Perp).
  elim (perp_not_col2 L11 L12 P' P HPerp2); [intro HNC|intuition].
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
  apply l6_21 with L11 L12 P' P; Col.
  }

(* Goal: @Cong Tn A B A' B' *)
  {
  destruct HP' as [HCol2 HPerp1]; destruct HP'' as [HCol3 HPerp2]; treat_equalities.
  elim (perp_not_col2 L11 L12 P P'' HPerp2); [intro HNC|intuition].
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
  apply l6_21 with L11 L12 P P''; Col.
  }

(* Goal: @Cong Tn A B A' B' *)
  {
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
  spliter; treat_equalities; auto.
  }
Qed.

Lemma col_2_par_projp2_cong : forall A A' B B' L11 L12 L21 L22,
  Col L11 L12 A' -> Col L11 L12 B' ->
  Par L11 L12 L21 L22 ->
  Projp A' A L21 L22 -> Projp B' B L21 L22 ->
  Cong A B A' B'.
Proof.
(* Goal: forall (A A' B B' L11 L12 L21 L22 : @Tpoint Tn) (_ : @Col Tn L11 L12 A') (_ : @Col Tn L11 L12 B') (_ : @Par Tn L11 L12 L21 L22) (_ : @Projp Tn A' A L21 L22) (_ : @Projp Tn B' B L21 L22), @Cong Tn A B A' B' *)
intros A A' B B' L11 L12 L21 L22 HColA' HColB' HPar HProjpA HProjpB.
(* Goal: not (@Par Tn A B X Y) *)
(* Goal: @Col Tn A B P' *)
(* Goal: or (@Par Tn P P' X Y) (@eq (@Tpoint Tn) P P') *)
(* Goal: and (@Proj Tn P P' A B X Y) (forall (x' : @Tpoint Tn) (_ : @Proj Tn P x' A B X Y), @eq (@Tpoint Tn) P' x') *)
elim HPar; clear HPar; intro HPar.

(* Goal: @Cong Tn A B A' B' *)
  {
  elim (eq_dec_points A' B'); intro HDiffA'B'; treat_equalities;
  [assert (A = B) by (apply projp_id with A' L21 L22; auto); treat_equalities; Cong|].
(* Goal: @Cong Tn A B A' B' *)
  elim (eq_dec_points A B); intro HDiffAB; treat_equalities.

(* Goal: @Cong Tn A B A' B' *)
    {
(* Goal: @Cong Tn A A A' B' *)
    assert (HCol : Col A A' B') by (apply projp2_col with L21 L22; auto).
(* Goal: @Cong Tn A A A' B' *)
    assert (HColA : Col L21 L22 A) by (apply projp_col with A'; auto).
    exfalso; apply HDiffA'B'; apply l6_21 with L11 L12 A A'; Col; intro;
(* Goal: @Col Tn A B C *)
(* Goal: @Par Tn C A C' A' *)
(* Goal: @Par Tn A B A' B' *)
(* Goal: @Par Tn C B C' B' *)
    treat_equalities; apply HPar; exists A; Col.
    }

(* Goal: @Cong Tn A B A' B' *)
    {
(* Goal: @Cong Tn A B A' B' *)
    assert (HPara : Plg A B B' A').
(* Goal: @Cong Tn A B A' B' *)
      {
(* Goal: @Plg Tn A B B' A' *)
      apply pars_par_plg.

(* Goal: @Cong Tn A B A' B' *)
        {
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
        apply par_strict_col2_par_strict with L11 L12; auto.
        apply par_strict_symmetry;
        apply par_strict_col2_par_strict with L21 L22; auto;
(* Goal: @eq (@Tpoint Tn) P' P' *)
(* Goal: or (and (@Col Tn A B P') (@Perp Tn A B P' P')) (and (@Col Tn A B P') (@eq (@Tpoint Tn) P' P')) *)
        [apply projp_col with A'|apply projp_col with B']; auto.
        }

(* Goal: @Cong Tn A B A' B' *)
        {
(* Goal: @Par Tn A A' B B' *)
        unfold Projp in *.
        destruct HProjpA as [H HElim]; clear H;
        elim HElim; clear HElim; intro H; destruct H as [HColA HPerp1];
        [|exfalso; apply HPar; exists A'; Col].
        destruct HProjpB as [H HElim]; clear H;
        elim HElim; clear HElim; intro H; destruct H as [HColB HPerp2];
        [|exfalso; apply HPar; exists B'; Col].
        apply l12_9_2D with L21 L22; Perp.
        }
      }
(* Goal: @Cong Tn A A C C *)
    apply plg_to_parallelogram in HPara; apply plg_cong in HPara; spliter; Cong.
    }
  }

(* Goal: @Cong Tn A B A' B' *)
  {
  assert (A = A')
    by (apply eq_sym; apply col_projp_eq with L21 L22; auto; spliter; ColR).
  assert (B = B')
    by (apply eq_sym; apply col_projp_eq with L21 L22; auto; spliter; ColR).
(* Goal: @Cong Tn A A C C *)
  treat_equalities; Cong.
  }
Qed.

End Projections.
