Require Export GeoCoq.Tarski_dev.Ch12_parallel_inter_dec.

Section Orientation.

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

Definition proj := fun  T A B P => A <> B /\ (~Col A B T /\ Perp A B T P /\ Col A B P \/ Col A B T /\ P = T).

Lemma proj_exists : forall A B T, A <> B -> exists P, proj T A B P.
(* Goal: forall (A B C : @Tpoint Tn) (_ : @Par Tn A B A C), @Col Tn A B C *)
intros.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => proj T A B P) *)
induction(col_dec A B T).
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => proj T A B P) *)
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => proj T A B P) *)
exists T.
(* Goal: proj T A B P *)
unfold proj.
(* Goal: iff (@Bet Tn M A' B') (@Bet Tn M A B) *)
split.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: or (and (not (@Col Tn Q P A)) (and (@Perp Tn Q P A A) (@Col Tn Q P A))) (and (@Col Tn Q P A) (@eq (@Tpoint Tn) A A)) *)
right.
split;
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => proj T A B P) *)
assert(HH:=l8_18_existence A B T H0).
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => proj T A B P) *)
ex_and HH P.
(* Goal: @ex (@Tpoint Tn) (fun E : @Tpoint Tn => and (@Bet Tn C E D) (@Cong Tn B A C E)) *)
exists P.
(* Goal: proj T A B P *)
unfold proj.
(* Goal: iff (@Bet Tn M A' B') (@Bet Tn M A B) *)
split.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: or (and (not (@Col Tn Q P A)) (and (@Perp Tn Q P A B) (@Col Tn Q P B))) (and (@Col Tn Q P A) (@eq (@Tpoint Tn) B A)) *)
(* Goal: or (and (not (@Col Tn Q P A)) (and (@Perp Tn Q P A B) (@Col Tn Q P B))) (and (@Col Tn Q P A) (@eq (@Tpoint Tn) B A)) *)
left.
(* Goal: and (not (@Col Tn A B P)) (and (not (@Col Tn A1 B1 P1)) (forall (C C1 B2 M B' C' K : @Tpoint Tn) (_ : @Perp Tn A B C A) (_ : proj P A C C) (_ : @Perp Tn A1 B1 C1 A1) (_ : proj P1 A1 C1 C1) (_ : @Out Tn A1 B1 B2) (_ : @Cong Tn A B A1 B2) (_ : @Midpoint Tn M A A1) (_ : @Midpoint Tn M B2 B') (_ : @Midpoint Tn M C1 C') (_ : @Midpoint Tn K B B'), or (@Bet Tn C A C') (@OS Tn A K C C'))) *)
repeat split;auto.
Qed.

Lemma proj_per : forall A B T P, A <> B -> proj T A B P -> Per T P A /\ Per T P B /\ Col A B P.
(* Goal: forall (A B C : @Tpoint Tn) (_ : @Par Tn A B A C), @Col Tn A B C *)
intros.
(* Goal: not (@Col Tn P Q A) *)
unfold proj in H0.
(* Goal: @Col Tn A B C *)
spliter.
(* Goal: not (@Col Tn P Q A) *)
induction H1.
(* Goal: @Col Tn A B C *)
spliter.
(* Goal: iff (@Bet Tn M A' B') (@Bet Tn M A B) *)
repeat split.

induction (eq_dec_points A P).
treat_equalities.
(* Goal: @Per Tn A1 C1 C1 *)
apply l8_5.

(* Goal: @Per Tn A B C *)
(* Goal: not (@eq (@Tpoint Tn) A C) *)
apply perp_in_per.
eauto with perp.

induction (eq_dec_points B P).
treat_equalities.

(* Goal: @Per Tn A1 C1 C1 *)
apply l8_5.

(* Goal: @Per Tn A B C *)
(* Goal: not (@eq (@Tpoint Tn) A C) *)
apply perp_in_per.
(* Goal: @Perp_at Tn C1 P1 C1 C1 A1 *)
(* Goal: @Per Tn P1 C1 A1 *)
apply perp_in_comm.
(* Goal: @Perp_at Tn C1 C1 P1 A1 C1 *)
(* Goal: @Per Tn P1 C1 A1 *)
apply perp_perp_in.
(* Goal: @Perp Tn C1 P1 A1 C1 *)
(* Goal: @Per Tn P1 C1 A1 *)
apply perp_sym.
eapply perp_col.
(* Goal: @Le Tn A B C D *)
assumption.

eauto with perp.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Col Tn A B C *)
spliter.
(* Goal: or (and (not (@Col Tn A C T)) (and (@Perp Tn A C T P) (@Col Tn A C P))) (and (@Col Tn A C T) (@eq (@Tpoint Tn) P T)) *)
subst T.
(* Goal: iff (@Bet Tn M A' B') (@Bet Tn M A B) *)
repeat split.
(* Goal: @Perp_at Tn B A B B C *)
(* Goal: not (@eq (@Tpoint Tn) A C) *)
Perp.
(* Goal: @Perp_at Tn B A B B C *)
(* Goal: not (@eq (@Tpoint Tn) A C) *)
Perp.
(* Goal: @Le Tn A B C D *)
assumption.
Qed.

Lemma proj_uniqueness : forall A B T P P', proj T A B P -> proj T A B P' -> P = P'.
(* Goal: forall (A B C : @Tpoint Tn) (_ : @Par Tn A B A C), @Col Tn A B C *)
intros.
(* Goal: @Col Tn A' B' C' *)
unfold proj in *.
(* Goal: @Col Tn A B C *)
spliter.
(* Goal: @eq (@Tpoint Tn) P P' *)
induction H1; induction H2; spliter; assert(Col A P P').
(* Goal: @Col Tn Q A B *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
ColR.
eapply (l8_18_uniqueness A B T P P');
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: or (and (not (@Col Tn A C T)) (and (@Perp Tn A C T P) (@Col Tn A C P))) (and (@Col Tn A C T) (@eq (@Tpoint Tn) P T)) *)
subst T.
(* Goal: False *)
contradiction.
(* Goal: False *)
contradiction.
(* Goal: @eq (@Tpoint Tn) P P' *)
subst P'.
(* Goal: @Col Tn Q A B *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
ColR.
(* Goal: @eq (@Tpoint Tn) P P' *)
subst P'.
(* Goal: False *)
contradiction.
(* Goal: or (and (not (@Col Tn A C T)) (and (@Perp Tn A C T P) (@Col Tn A C P))) (and (@Col Tn A C T) (@eq (@Tpoint Tn) P T)) *)
subst T.
(* Goal: @eq (@Tpoint Tn) P P' *)
subst P'.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: or (and (not (@Col Tn A C T)) (and (@Perp Tn A C T P) (@Col Tn A C P))) (and (@Col Tn A C T) (@eq (@Tpoint Tn) P T)) *)
subst T.
(* Goal: @eq (@Tpoint Tn) P P' *)
subst P'.
(* Goal: @eq (@Tpoint Tn) C' C' *)
reflexivity.
Qed.


Lemma proj_col : forall T P A B, proj T A B P -> Col P A B.
(* Goal: forall (A B C : @Tpoint Tn) (_ : @Par Tn A B A C), @Col Tn A B C *)
intros.
(* Goal: not (@eq (@Tpoint Tn) P Q) *)
unfold proj in H.
(* Goal: @Col Tn A B C *)
spliter.
(* Goal: @Col Tn A B C *)
induction H0; spliter.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: or (and (not (@Col Tn A C T)) (and (@Perp Tn A C T P) (@Col Tn A C P))) (and (@Col Tn A C T) (@eq (@Tpoint Tn) P T)) *)
subst T.
(* Goal: @Col Tn A B C *)
Col.
Qed.

Lemma proj_col_proj : forall A B C T P, proj T A B P -> A <> C -> Col A B C -> proj T A C P.
(* Goal: forall (A B C : @Tpoint Tn) (_ : @Par Tn A B A C), @Col Tn A B C *)
intros.
(* Goal: @Col Tn A' B' C' *)
unfold proj in *.
(* Goal: @Col Tn A B C *)
spliter.
(* Goal: @Col Tn A B C *)
induction H2; repeat split; auto; spliter.
(* Goal: or (and (not (@Col Tn Q P A)) (and (@Perp Tn Q P A B) (@Col Tn Q P B))) (and (@Col Tn Q P A) (@eq (@Tpoint Tn) B A)) *)
(* Goal: or (and (not (@Col Tn Q P A)) (and (@Perp Tn Q P A B) (@Col Tn Q P B))) (and (@Col Tn Q P A) (@eq (@Tpoint Tn) B A)) *)
left.
(* Goal: iff (@Bet Tn M A' B') (@Bet Tn M A B) *)
repeat split.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
(* Goal: False *)
(* Goal: @Col Tn A B C *)
apply H2.
(* Goal: @Col Tn Q A B *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
ColR.

(* Goal: @Perp Tn A C T P *)
(* Goal: @Col Tn A C P *)
(* Goal: or (and (not (@Col Tn A C T)) (and (@Perp Tn A C T P) (@Col Tn A C P))) (and (@Col Tn A C T) (@eq (@Tpoint Tn) P T)) *)
eapply (perp_col _ B); auto.
(* Goal: @Col Tn Q A B *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
ColR.
(* Goal: or (and (not (@Col Tn A C T)) (and (@Perp Tn A C T P) (@Col Tn A C P))) (and (@Col Tn A C T) (@eq (@Tpoint Tn) P T)) *)
subst T.
(* Goal: or (and (not (@Col Tn Q P A)) (and (@Perp Tn Q P A A) (@Col Tn Q P A))) (and (@Col Tn Q P A) (@eq (@Tpoint Tn) A A)) *)
right.
(* Goal: and (@Bet Tn D C P') (@Cong Tn D P' A B) *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
split; auto.
(* Goal: @Col Tn Q A B *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
ColR.
Qed.

Lemma per_proj : forall A B T P, A <> B -> Per T P A -> Per T P B -> Col A B P -> proj T A B P.
(* Goal: forall (A B C : @Tpoint Tn) (_ : @Par Tn A B A C), @Col Tn A B C *)
intros.
(* Goal: proj T A B P *)
unfold proj.
(* Goal: and (@Bet Tn D C P') (@Cong Tn D P' A B) *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
split; auto.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => proj T A B P) *)
induction (col_dec A B T).
(* Goal: or (and (not (@Col Tn Q P A)) (and (@Perp Tn Q P A A) (@Col Tn Q P A))) (and (@Col Tn Q P A) (@eq (@Tpoint Tn) A A)) *)
right.
(* Goal: and (@Bet Tn D C P') (@Cong Tn D P' A B) *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
split; auto.

assert(Col T P A).
(* Goal: @Col Tn Q A B *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
ColR.
assert(Col T P B).
(* Goal: @Col Tn Q A B *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
ColR.

induction(eq_dec_points A P).
(* Goal: @Per Tn P C A *)
(* Goal: @Per Tn P1 C1 A1 *)
subst P.
assert(T=A \/ B=A).
apply l8_9; auto.
induction H6.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
subst B.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
tauto.

assert(T=P \/ A=P).
apply l8_9; auto.
induction H7.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Per Tn P C A *)
(* Goal: @Per Tn P1 C1 A1 *)
subst P.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
tauto.

(* Goal: or (and (not (@Col Tn Q P A)) (and (@Perp Tn Q P A B) (@Col Tn Q P B))) (and (@Col Tn Q P A) (@eq (@Tpoint Tn) B A)) *)
(* Goal: or (and (not (@Col Tn Q P A)) (and (@Perp Tn Q P A B) (@Col Tn Q P B))) (and (@Col Tn Q P A) (@eq (@Tpoint Tn) B A)) *)
left.

induction (eq_dec_points A P).

(* Goal: @Per Tn P C A *)
(* Goal: @Per Tn P1 C1 A1 *)
subst P.

(* Goal: and (@Bet Tn D C P') (@Cong Tn D P' A B) *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
repeat split; auto.

apply per_perp_in in H1.
apply perp_in_comm in H1.
apply perp_in_perp_bis in H1.
(* Goal: not (@Col Tn P Q A) *)
induction H1.
(* Goal: @Perp_at Tn B A B B C *)
(* Goal: not (@eq (@Tpoint Tn) A C) *)
Perp.

apply perp_not_eq_1 in H1.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
tauto.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
(* Goal: or (and (not (@Col Tn A C T)) (and (@Perp Tn A C T P) (@Col Tn A C P))) (and (@Col Tn A C T) (@eq (@Tpoint Tn) P T)) *)
subst T.
(* Goal: False *)
contradiction.
(* Goal: @Le Tn A B C D *)
assumption.

(* Goal: and (@Bet Tn D C P') (@Cong Tn D P' A B) *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
repeat split; auto.
apply per_perp_in in H0.
apply perp_in_comm in H0.
apply perp_in_perp_bis in H0.
induction H0.
eapply perp_col.
(* Goal: @Le Tn A B C D *)
assumption.
eauto with perp.

(* Goal: @Col Tn A B C *)
Col.
apply perp_not_eq_1 in H0.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
tauto.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
(* Goal: or (and (not (@Col Tn A C T)) (and (@Perp Tn A C T P) (@Col Tn A C P))) (and (@Col Tn A C T) (@eq (@Tpoint Tn) P T)) *)
subst T.
(* Goal: False *)
contradiction.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
Qed.


Definition eqo := fun A B P A1 B1 P1 => ~Col A B P /\ ~Col A1 B1 P1 /\
                      forall C C1 B2 M B' C' K,
                             Perp A B C A  -> Per P C A -> Perp A1 B1 C1 A1 -> Per P1 C1 A1 ->
                             Out A1 B1 B2 -> Cong A B A1 B2 ->
                             Midpoint M A A1 -> Midpoint M B2 B' -> Midpoint M C1 C' -> Midpoint K B B' ->
                             Bet C A C' \/ OS A K C C'.



Definition eq_o := fun A B P A1 B1 P1 => ~Col A B P /\ ~Col A1 B1 P1 /\
                      forall C C1 B2 M B' C' K,
                             Perp A B C A -> proj P A C C -> Perp A1 B1 C1 A1 -> proj P1 A1 C1 C1 ->
                             Out A1 B1 B2 -> Cong A B A1 B2 ->
                             Midpoint M A A1 -> Midpoint M B2 B' -> Midpoint M C1 C' -> Midpoint K B B' ->
                             Bet C A C' \/ OS A K C C'.

Lemma eqo_eq_o : forall A B P A1 B1 P1, eqo A B P A1 B1 P1 -> eq_o A B P A1 B1 P1.
(* Goal: forall (A B C : @Tpoint Tn) (_ : @Par Tn A B A C), @Col Tn A B C *)
intros.
(* Goal: eq_o A B P A1 B1 P1 *)
unfold eqo in H.
(* Goal: @Col Tn A B C *)
spliter.
(* Goal: eq_o A B P A1 B1 P1 *)
unfold eq_o.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
repeat split ; auto.
(* Goal: forall (A B C : @Tpoint Tn) (_ : @Par Tn A B A C), @Col Tn A B C *)
intros.
(* Goal: or (@Bet Tn C A C') (@OS Tn A K C C') *)
assert(HH:= H1 C C1 B2 M B' C' K).
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
apply HH; auto.
(* Goal: @Col Tn A' B' C' *)
unfold proj in *.
(* Goal: @Col Tn A B C *)
spliter.
(* Goal: @Per Tn P1 C1 A1 *)
induction H13; induction H12.
(* Goal: @Col Tn A B C *)
spliter.
(* Goal: @Per Tn A B C *)
(* Goal: not (@eq (@Tpoint Tn) A C) *)
apply perp_in_per.
(* Goal: @Perp_at Tn C1 P1 C1 C1 A1 *)
(* Goal: @Per Tn P1 C1 A1 *)
apply perp_in_comm.
(* Goal: @Perp_at Tn C1 C1 P1 A1 C1 *)
(* Goal: @Per Tn P1 C1 A1 *)
apply perp_perp_in.
(* Goal: @Perp Tn C1 P1 A1 C1 *)
(* Goal: @Per Tn P1 C1 A1 *)
apply perp_sym.
(* Goal: @Perp_at Tn B A B B C *)
(* Goal: not (@eq (@Tpoint Tn) A C) *)
Perp.
(* Goal: @Col Tn A B C *)
spliter.
(* Goal: @Per Tn A B C *)
(* Goal: not (@eq (@Tpoint Tn) A C) *)
apply perp_in_per.
(* Goal: @Perp_at Tn C1 P1 C1 C1 A1 *)
(* Goal: @Per Tn P1 C1 A1 *)
apply perp_in_comm.
(* Goal: @Perp_at Tn C1 C1 P1 A1 C1 *)
(* Goal: @Per Tn P1 C1 A1 *)
apply perp_perp_in.
(* Goal: @Perp Tn C1 P1 A1 C1 *)
(* Goal: @Per Tn P1 C1 A1 *)
apply perp_sym.
(* Goal: @Perp_at Tn B A B B C *)
(* Goal: not (@eq (@Tpoint Tn) A C) *)
Perp.
(* Goal: @Col Tn A B C *)
spliter.
(* Goal: @Per Tn P C A *)
(* Goal: @Per Tn P1 C1 A1 *)
subst P.
(* Goal: @Per Tn C1 C1 A1 *)
apply l8_2.
(* Goal: @Per Tn A1 C1 C1 *)
apply l8_5.
(* Goal: @Col Tn A B C *)
spliter.
(* Goal: @Per Tn P C A *)
(* Goal: @Per Tn P1 C1 A1 *)
subst P.
(* Goal: @Per Tn C1 C1 A1 *)
apply l8_2.
(* Goal: @Per Tn A1 C1 C1 *)
apply l8_5.
(* Goal: @Col Tn A' B' C' *)
unfold proj in *.
(* Goal: @Col Tn A B C *)
spliter.
(* Goal: @Per Tn P1 C1 A1 *)
induction H13; induction H12.
(* Goal: @Col Tn A B C *)
spliter.
(* Goal: @Per Tn A B C *)
(* Goal: not (@eq (@Tpoint Tn) A C) *)
apply perp_in_per.
(* Goal: @Perp_at Tn C1 P1 C1 C1 A1 *)
(* Goal: @Per Tn P1 C1 A1 *)
apply perp_in_comm.
(* Goal: @Perp_at Tn C1 C1 P1 A1 C1 *)
(* Goal: @Per Tn P1 C1 A1 *)
apply perp_perp_in.
(* Goal: @Perp Tn C1 P1 A1 C1 *)
(* Goal: @Per Tn P1 C1 A1 *)
apply perp_sym.
(* Goal: @Perp_at Tn B A B B C *)
(* Goal: not (@eq (@Tpoint Tn) A C) *)
Perp.
(* Goal: @Col Tn A B C *)
spliter.
(* Goal: @Per Tn P1 C1 A1 *)
subst P1.
(* Goal: @Per Tn C1 C1 A1 *)
apply l8_2.
(* Goal: @Per Tn A1 C1 C1 *)
apply l8_5.
(* Goal: @Col Tn A B C *)
spliter.
(* Goal: @Per Tn A B C *)
(* Goal: not (@eq (@Tpoint Tn) A C) *)
apply perp_in_per.
(* Goal: @Perp_at Tn C1 P1 C1 C1 A1 *)
(* Goal: @Per Tn P1 C1 A1 *)
apply perp_in_comm.
(* Goal: @Perp_at Tn C1 C1 P1 A1 C1 *)
(* Goal: @Per Tn P1 C1 A1 *)
apply perp_perp_in.
(* Goal: @Perp Tn C1 P1 A1 C1 *)
(* Goal: @Per Tn P1 C1 A1 *)
apply perp_sym.
(* Goal: @Perp_at Tn B A B B C *)
(* Goal: not (@eq (@Tpoint Tn) A C) *)
Perp.
(* Goal: @Col Tn A B C *)
spliter.
(* Goal: @Per Tn P1 C1 A1 *)
subst P1.
(* Goal: @Per Tn C1 C1 A1 *)
apply l8_2.
(* Goal: @Per Tn A1 C1 C1 *)
apply l8_5.
Qed.




Lemma eq_o_eqo : forall A B P A1 B1 P1, eq_o A B P A1 B1 P1 -> eqo A B P A1 B1 P1.
(* Goal: forall (A B C : @Tpoint Tn) (_ : @Par Tn A B A C), @Col Tn A B C *)
intros.
unfold eq_o in H.
(* Goal: @Col Tn A B C *)
spliter.
unfold eqo.
(* Goal: and (@Bet Tn D C P') (@Cong Tn D P' A B) *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
repeat split; auto.
(* Goal: forall (A B C : @Tpoint Tn) (_ : @Par Tn A B A C), @Col Tn A B C *)
intros.
eapply H1.
(* Goal: False *)
(* Goal: @Col Tn A B C *)
apply H2.
apply per_proj.
apply perp_not_eq_2 in H2.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Per Tn A1 C1 C1 *)
apply l8_5.
(* Goal: @Col Tn A B C *)
Col.
apply H4.
apply per_proj.
apply perp_not_eq_2 in H4.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Per Tn A1 C1 C1 *)
apply l8_5.
(* Goal: @Col Tn A B C *)
Col.
apply H6.
(* Goal: @Le Tn A B C D *)
assumption.
apply H8.
apply H9.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Le Tn A B C D *)
assumption.
Qed.



Lemma eq_o_one_side : forall A B X Y, eq_o A B X A B Y -> OS A B X Y.
(* Goal: forall (A B C : @Tpoint Tn) (_ : @Par Tn A B A C), @Col Tn A B C *)
intros.
unfold eq_o in H.
(* Goal: @Col Tn A B C *)
spliter.
assert(A <> B).
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
subst B.
apply H.
(* Goal: @Col Tn A B C *)
Col.

assert(HH:=ex_per_cong B A A X A B).
assert(exists P : Tpoint, Per P A B /\ Cong P A A B /\ OS B A P X).
apply HH;
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
apply H.
(* Goal: @Col Tn A B C *)
Col.
clear HH.
ex_and H3 T.

assert(A <> T).
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
(* Goal: or (and (not (@Col Tn A C T)) (and (@Perp Tn A C T P) (@Col Tn A C P))) (and (@Col Tn A C T) (@eq (@Tpoint Tn) P T)) *)
subst T.
apply cong_symmetry in H4.
apply cong_identity in H4.
(* Goal: False *)
contradiction.

assert(Perp T A A B).
apply per_perp_in in H3.
apply perp_in_perp_bis in H3.
(* Goal: @Par_strict Tn A B A' B' *)
induction H3.
apply perp_not_eq_1 in H3.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
tauto.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Le Tn A B C D *)
assumption.

assert(HH:=proj_exists A T X H6).
ex_and HH PX.
assert(HH:=proj_exists A T Y H6).
ex_and HH PY.
prolong B A B' B A.
prolong PY A C' PY A.
assert(Col PX A T).
eapply proj_col.
apply H8.
assert(Col PY A T).
eapply proj_col.
apply H9.

assert(PX <> A).
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
subst PX.
apply proj_per in H8.
(* Goal: @Col Tn A B C *)
spliter.
apply H.
apply col_permutation_2.
eapply per2__col.
(* Goal: @Per Tn C1 C1 A1 *)
apply l8_2.
apply H3.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Le Tn A B C D *)
assumption.

assert(PY <> A).
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
subst PY.
apply proj_per in H9.
(* Goal: @Col Tn A B C *)
spliter.
(* Goal: False *)
apply H0.
apply col_permutation_2.
eapply per2__col.
(* Goal: @Per Tn C1 C1 A1 *)
apply l8_2.
apply H3.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Le Tn A B C D *)
assumption.

assert(~Col T A B).
apply per_not_col in H3.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Le Tn A B C D *)
assumption.

assert(Col A PX PY).
(* Goal: @Col Tn Q A B *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
ColR.

assert(~Col PX A B).
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
apply H18.
(* Goal: @Col Tn Q A B *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
ColR.

assert(~Col PY A B).
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
apply H18.
(* Goal: @Col Tn Q A B *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
ColR.

assert(A <> C').
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
(* Goal: @Col Tn A B C' *)
subst C'.
apply cong_symmetry in H13.
apply cong_identity in H13.
(* Goal: False *)
contradiction.

assert(TS A B PY C').
unfold TS.
(* Goal: and (@Bet Tn D C P') (@Cong Tn D P' A B) *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
repeat split; auto.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
apply H21.
apply bet_col in H12.
(* Goal: @Col Tn Q A B *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
ColR.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X A B) (@Col Tn X A C)) *)
(* Goal: @Col Tn A B C *)
exists A.
(* Goal: iff (@Bet Tn M A' B') (@Bet Tn M A B) *)
split.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: @Le Tn A B C D *)
assumption.

assert(HH:= H1 PX PY B A B' C' A).

assert(Bet PX A C' \/ OS A A PX C').
apply HH;
clear HH; clear H1.

apply per_perp_in in H3.
apply perp_in_comm in H3.
apply perp_in_perp_bis in H3.
(* Goal: @Par_strict Tn A B A' B' *)
induction H3.
apply perp_comm.
(* Goal: @Perp Tn C1 P1 A1 C1 *)
(* Goal: @Per Tn P1 C1 A1 *)
apply perp_sym.
eapply perp_col.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
apply H1.
(* Goal: @Col Tn A B C *)
Col.
apply perp_not_eq_1 in H1.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
tauto.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Le Tn A B C D *)
assumption.

eapply proj_col_proj.
apply H8.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Col Tn A B C *)
Col.

apply per_perp_in in H3.
apply perp_in_comm in H3.
apply perp_in_perp_bis in H3.
(* Goal: @Par_strict Tn A B A' B' *)
induction H3.
apply perp_comm.
(* Goal: @Perp Tn C1 P1 A1 C1 *)
(* Goal: @Per Tn P1 C1 A1 *)
apply perp_sym.
eapply perp_col.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
apply H1.
(* Goal: @Col Tn A B C *)
Col.
apply perp_not_eq_1 in H1.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
tauto.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Le Tn A B C D *)
assumption.

eapply proj_col_proj.
apply H9.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Col Tn A B C *)
Col.

apply out_trivial.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @eq (@Tpoint Tn) C' C' *)
apply cong_reflexivity.
apply l7_3_2.
unfold Midpoint.
apply cong_symmetry in H11.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
split;auto.
unfold Midpoint.
apply cong_symmetry in H13.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
split;auto.
unfold Midpoint.
apply cong_symmetry in H11.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
split;auto.

clear H1 HH.

assert(TS A B PX C').
unfold TS.
(* Goal: and (@Bet Tn D C P') (@Cong Tn D P' A B) *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
repeat split; auto.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
apply H21.
apply bet_col in H12.
(* Goal: @Col Tn Q A B *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
ColR.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X A B) (@Col Tn X A C)) *)
(* Goal: @Col Tn A B C *)
exists A.
induction H24.
(* Goal: iff (@Bet Tn M A' B') (@Bet Tn M A B) *)
split.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: @Le Tn A B C D *)
assumption.
unfold OS in H1.
ex_and H1 U.
unfold TS in H1.
(* Goal: @Col Tn A B C *)
spliter.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
assert_diffs; tauto.

unfold proj in H8.
(* Goal: @Col Tn A B C *)
spliter.
induction H25.
(* Goal: @Col Tn A B C *)
spliter.

assert(Par A B X PX).
apply l12_9_2D with T A.
(* Goal: @Perp Tn C1 P1 A1 C1 *)
(* Goal: @Per Tn P1 C1 A1 *)
apply perp_sym.
apply H7.
apply perp_right_comm.
(* Goal: @Perp_at Tn B A B B C *)
(* Goal: not (@eq (@Tpoint Tn) A C) *)
Perp.

assert(Par_strict A B X PX).
induction H28.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Col Tn A B C *)
spliter.
(* Goal: @Col Tn A B C *)
(* Goal: @Col Tn A B C *)
apply False_ind.
apply H.
(* Goal: @Col Tn Q A B *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
ColR.

unfold proj in H9.
(* Goal: @Col Tn A B C *)
spliter.
induction H30.
(* Goal: @Col Tn A B C *)
spliter.

assert(Par A B Y PY).
apply l12_9_2D with T A.
(* Goal: @Perp Tn C1 P1 A1 C1 *)
(* Goal: @Per Tn P1 C1 A1 *)
apply perp_sym.
apply H7.
apply perp_right_comm.
(* Goal: @Perp_at Tn B A B B C *)
(* Goal: not (@eq (@Tpoint Tn) A C) *)
Perp.

assert(Par_strict A B Y PY).
induction H33.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Col Tn A B C *)
spliter.
(* Goal: @Col Tn A B C *)
(* Goal: @Col Tn A B C *)
apply False_ind.
(* Goal: False *)
apply H0.
(* Goal: @Col Tn Q A B *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
ColR.
apply l12_6 in H29.
apply l12_6 in H34.

assert(TS A B X C').
eapply l9_8_2.
apply H1.
apply one_side_symmetry.
(* Goal: @Le Tn A B C D *)
assumption.

assert(TS A B Y C').
eapply l9_8_2.
apply H23.
apply one_side_symmetry.
(* Goal: @Le Tn A B C D *)
assumption.
eapply l9_8_1.
apply H35.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Col Tn A B C *)
spliter.
subst Y.
apply l12_6 in H29.
eapply one_side_transitivity.
apply H29.
eapply l9_8_1.
apply H1.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Col Tn A B C *)
spliter.
subst X.
unfold proj in H9.
(* Goal: @Col Tn A B C *)
spliter.
induction H26.
(* Goal: @Col Tn A B C *)
spliter.

assert(Par A B Y PY).
apply l12_9_2D with T A.
(* Goal: @Perp Tn C1 P1 A1 C1 *)
(* Goal: @Per Tn P1 C1 A1 *)
apply perp_sym.
apply H7.
apply perp_right_comm.
(* Goal: @Perp_at Tn B A B B C *)
(* Goal: not (@eq (@Tpoint Tn) A C) *)
Perp.

assert(Par_strict A B Y PY).
induction H29.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Col Tn A B C *)
spliter.
(* Goal: @Col Tn A B C *)
(* Goal: @Col Tn A B C *)
apply False_ind.
(* Goal: False *)
apply H0.
(* Goal: @Col Tn Q A B *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
ColR.
apply l12_6 in H30.
eapply one_side_transitivity.
eapply l9_8_1.
apply H1.
apply H23.
apply one_side_symmetry.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Col Tn A B C *)
spliter.
subst Y.
eapply l9_8_1.
apply H1.
(* Goal: @Le Tn A B C D *)
assumption.
Qed.


Lemma eqo_one_side : forall A B X Y, eqo A B X A B Y -> OS A B X Y.
(* Goal: forall (A B C : @Tpoint Tn) (_ : @Par Tn A B A C), @Col Tn A B C *)
intros.
(* Goal: @OS Tn A B X Y *)
apply eqo_eq_o in H.
(* Goal: @OS Tn A B X Y *)
apply eq_o_one_side.
(* Goal: @Le Tn A B C D *)
assumption.
Qed.


Lemma eq_o_refl : forall A B P, ~Col A B P -> eq_o A B P A B P.
(* Goal: forall (A B C : @Tpoint Tn) (_ : @Par Tn A B A C), @Col Tn A B C *)
intros.
(* Goal: eq_o A B P A1 B1 P1 *)
unfold eq_o.
(* Goal: and (@Bet Tn D C P') (@Cong Tn D P' A B) *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
repeat split; auto.
(* Goal: forall (A B C : @Tpoint Tn) (_ : @Par Tn A B A C), @Col Tn A B C *)
intros.
unfold Midpoint in H8.
apply l7_3 in H6.
subst M.
(* Goal: @Col Tn A B C *)
spliter.
assert(proj P A C C1).
eapply proj_col_proj.
apply H3.
apply perp_not_eq_2 in H0.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
eapply perp2__col.
apply perp_comm.
(* Goal: @Perp Tn C1 P1 A1 C1 *)
(* Goal: @Per Tn P1 C1 A1 *)
apply perp_sym.
(* Goal: False *)
(* Goal: @Col Tn A B C *)
apply H2.
apply perp_comm.
(* Goal: @Perp_at Tn B A B B C *)
(* Goal: not (@eq (@Tpoint Tn) A C) *)
Perp.
assert(C=C1).
eapply proj_uniqueness.
apply H1.
(* Goal: @Le Tn A B C D *)
assumption.
subst C1.
(* Goal: or (and (not (@Col Tn Q P A)) (and (@Perp Tn Q P A B) (@Col Tn Q P B))) (and (@Col Tn Q P A) (@eq (@Tpoint Tn) B A)) *)
(* Goal: or (and (not (@Col Tn Q P A)) (and (@Perp Tn Q P A B) (@Col Tn Q P B))) (and (@Col Tn Q P A) (@eq (@Tpoint Tn) B A)) *)
left.
(* Goal: @Le Tn A B C D *)
assumption.
Qed.

Lemma eqo_refl : forall A B P, ~Col A B P -> eqo A B P A B P.
(* Goal: forall (A B C : @Tpoint Tn) (_ : @Par Tn A B A C), @Col Tn A B C *)
intros.
(* Goal: eqo A B P A B P *)
apply eq_o_eqo.
(* Goal: eq_o A B P A B P *)
apply eq_o_refl.
(* Goal: @Le Tn A B C D *)
assumption.
Qed.

Lemma per_id : forall A B B' C, A <> B -> B <> C -> B' <> C -> Per A B C -> Per A B' C -> Col C B B' -> B = B'.
(* Goal: forall (A B C : @Tpoint Tn) (_ : @Par Tn A B A C), @Col Tn A B C *)
intros.
assert(~ Col A B C).
eapply per_not_col.
(* Goal: @Le Tn A B C D *)
assumption.
assumption;
assert(Per B B' C).
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
eapply (l8_3 A); try auto.
(* Goal: @Col Tn A B C *)
Col.

assert(A <> B').
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
(* Goal: @Col Tn A B A' *)
(* Goal: forall _ : @Col Tn A B A', @eq (@Tpoint Tn) A' B' *)
subst B'.
apply H5.
(* Goal: @Col Tn A B C *)
Col.

assert(Per A B B').
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
eapply (per_col _ _ C); auto.
(* Goal: @Col Tn A B C *)
Col.
assert(Per A B' B).
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
eapply (per_col _ _ C); auto.
(* Goal: @Col Tn A B C *)
Col.
eapply l8_7.
apply H7.
(* Goal: @Le Tn A B C D *)
assumption.
Qed.


Lemma proj_one_side : forall A B A' B' P Q, A <> A' -> proj A P Q A' -> proj B P Q B' -> Col B A A' \/ OS A A' B B'.
(* Goal: forall (A B C : @Tpoint Tn) (_ : @Par Tn A B A C), @Col Tn A B C *)
intros.

induction (col_dec B A A').
(* Goal: or (and (not (@Col Tn Q P A)) (and (@Perp Tn Q P A B) (@Col Tn Q P B))) (and (@Col Tn Q P A) (@eq (@Tpoint Tn) B A)) *)
(* Goal: or (and (not (@Col Tn Q P A)) (and (@Perp Tn Q P A B) (@Col Tn Q P B))) (and (@Col Tn Q P A) (@eq (@Tpoint Tn) B A)) *)
left.
(* Goal: @Le Tn A B C D *)
assumption.
induction(eq_dec_points B B').
(* Goal: @Col Tn A B A' *)
(* Goal: forall _ : @Col Tn A B A', @eq (@Tpoint Tn) A' B' *)
subst B'.
(* Goal: or (and (not (@Col Tn Q P A)) (and (@Perp Tn Q P A A) (@Col Tn Q P A))) (and (@Col Tn Q P A) (@eq (@Tpoint Tn) A A)) *)
right.
(* Goal: @eq (@Tpoint Tn) C' C' *)
apply one_side_reflexivity.
(* Goal: @Le Tn A B C D *)
assumption.

assert(Par A A' B B').
(* Goal: @Col Tn A' B' C' *)
unfold proj in *.
(* Goal: @Col Tn A B C *)
spliter.
(* Goal: @Col Tn A B C *)
induction H5; induction H4;spliter.
eapply l12_9_2D.
(* Goal: @Perp Tn C1 P1 A1 C1 *)
(* Goal: @Per Tn P1 C1 A1 *)
apply perp_sym.
apply H8.
(* Goal: @Perp_at Tn B A B B C *)
(* Goal: not (@eq (@Tpoint Tn) A C) *)
Perp.
(* Goal: @Col Tn A B A' *)
(* Goal: forall _ : @Col Tn A B A', @eq (@Tpoint Tn) A' B' *)
subst B'.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
tauto.
(* Goal: @Col Tn A' B' C' *)
subst A'.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
tauto.
(* Goal: @Col Tn A B A' *)
(* Goal: forall _ : @Col Tn A B A', @eq (@Tpoint Tn) A' B' *)
subst B'.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
tauto.
assert(Par_strict A A' B B').
induction H4.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Col Tn A B C *)
spliter.
(* Goal: @Col Tn A B C *)
(* Goal: @Col Tn A B C *)
apply False_ind.
(* Goal: False *)
(* Goal: @Col Tn A B C *)
apply H2.
(* Goal: @Col Tn Q A B *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
ColR.
(* Goal: or (and (not (@Col Tn Q P A)) (and (@Perp Tn Q P A A) (@Col Tn Q P A))) (and (@Col Tn Q P A) (@eq (@Tpoint Tn) A A)) *)
right.
eapply l12_6.
(* Goal: @Le Tn A B C D *)
assumption.
Qed.


Lemma proj_eq_col : forall A B P Q C, proj A P Q C -> proj B P Q C -> Col A B C.
(* Goal: forall (A B C : @Tpoint Tn) (_ : @Par Tn A B A C), @Col Tn A B C *)
intros.
(* Goal: @Col Tn A' B' C' *)
unfold proj in *.
(* Goal: @Col Tn A B C *)
spliter.
(* Goal: @Col Tn A B C *)
induction H2; induction H1; spliter.
apply col_permutation_1.
eapply perp2__col.
(* Goal: @Perp Tn C1 P1 A1 C1 *)
(* Goal: @Per Tn P1 C1 A1 *)
apply perp_sym.
apply perp_comm.
apply H5.
(* Goal: @Perp Tn C1 P1 A1 C1 *)
(* Goal: @Per Tn P1 C1 A1 *)
apply perp_sym.
(* Goal: @Perp_at Tn B A B B C *)
(* Goal: not (@eq (@Tpoint Tn) A C) *)
Perp.
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
subst B.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: False *)
subst C.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: False *)
subst C.
(* Goal: @Col Tn A B C *)
Col.
Qed.

Lemma proj_par : forall A B A' B' P Q, A <> A' -> B <> B' -> proj A P Q A' -> proj B P Q B' -> Par A A' B B'.
(* Goal: forall (A B C : @Tpoint Tn) (_ : @Par Tn A B A C), @Col Tn A B C *)
intros.
eapply l12_9_2D.
(* Goal: @Col Tn A' B' C' *)
unfold proj in *.
(* Goal: @Col Tn A B C *)
spliter.
(* Goal: @Col Tn A B C *)
induction H4; induction H3; spliter.
(* Goal: @Perp Tn C1 P1 A1 C1 *)
(* Goal: @Per Tn P1 C1 A1 *)
apply perp_sym.
apply H7.
(* Goal: @Perp_at Tn B A B B C *)
(* Goal: not (@eq (@Tpoint Tn) A C) *)
Perp.
(* Goal: @Col Tn A' B' C' *)
subst A'.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
tauto.
(* Goal: @Col Tn A B A' *)
(* Goal: forall _ : @Col Tn A B A', @eq (@Tpoint Tn) A' B' *)
subst B'.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
tauto.
(* Goal: @Col Tn A' B' C' *)
unfold proj in *.
(* Goal: @Col Tn A B C *)
spliter.
(* Goal: @Col Tn A B C *)
induction H4; induction H3; spliter.
(* Goal: @Perp Tn C1 P1 A1 C1 *)
(* Goal: @Per Tn P1 C1 A1 *)
apply perp_sym.
apply H5.
(* Goal: @Col Tn A B A' *)
(* Goal: forall _ : @Col Tn A B A', @eq (@Tpoint Tn) A' B' *)
subst B'.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
tauto.
(* Goal: @Col Tn A' B' C' *)
subst A'.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
tauto.
(* Goal: @Col Tn A' B' C' *)
subst A'.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
tauto.
Qed.

Lemma proj_not_col : forall A A' P Q, A <> A' -> proj A P Q A' -> ~Col P Q A.
(* Goal: forall (A B C : @Tpoint Tn) (_ : @Par Tn A B A C), @Col Tn A B C *)
intros.
(* Goal: not (@Col Tn P Q A) *)
unfold proj in H0.
(* Goal: @Col Tn A B C *)
spliter.
(* Goal: not (@Col Tn P Q A) *)
induction H1.
(* Goal: @Col Tn A B C *)
spliter.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Col Tn A B C *)
spliter.
(* Goal: @Col Tn A' B' C' *)
subst A'.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
tauto.
Qed.

Lemma proj_comm : forall A B P Q, proj A P Q B -> proj A Q P B.
(* Goal: forall (A B C : @Tpoint Tn) (_ : @Par Tn A B A C), @Col Tn A B C *)
intros.
(* Goal: @Col Tn A' B' C' *)
unfold proj in *.
(* Goal: @Col Tn A B C *)
spliter.
(* Goal: and (@Bet Tn D C P') (@Cong Tn D P' A B) *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
induction H0; spliter; split; auto.
(* Goal: or (and (not (@Col Tn Q P A)) (and (@Perp Tn Q P A B) (@Col Tn Q P B))) (and (@Col Tn Q P A) (@eq (@Tpoint Tn) B A)) *)
(* Goal: or (and (not (@Col Tn Q P A)) (and (@Perp Tn Q P A B) (@Col Tn Q P B))) (and (@Col Tn Q P A) (@eq (@Tpoint Tn) B A)) *)
left.
(* Goal: iff (@Bet Tn M A' B') (@Bet Tn M A B) *)
repeat split.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
(* Goal: False *)
apply H0.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: @Perp_at Tn B A B B C *)
(* Goal: not (@eq (@Tpoint Tn) A C) *)
Perp.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
subst B.
(* Goal: or (and (not (@Col Tn Q P A)) (and (@Perp Tn Q P A A) (@Col Tn Q P A))) (and (@Col Tn Q P A) (@eq (@Tpoint Tn) A A)) *)
right.
(* Goal: @Col Tn A B C *)
split; Col.
Qed.

Lemma proj_not_eq : forall A B A' B' P Q, A' <> B' -> proj A P Q A' -> proj B P Q B' -> A <> B.
(* Goal: forall (A B C : @Tpoint Tn) (_ : @Par Tn A B A C), @Col Tn A B C *)
intros.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
apply H.
eapply proj_uniqueness.
(* Goal: False *)
apply H0.
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
subst B.
(* Goal: @Le Tn A B C D *)
assumption.
Qed.

Lemma proj_not_eq_not_col : forall A B A' B' P Q, A' <> B' -> A <> A' -> proj A P Q A' -> proj B P Q B' -> ~Col A A' B'.
(* Goal: forall (A B C : @Tpoint Tn) (_ : @Par Tn A B A C), @Col Tn A B C *)
intros.
unfold proj in H1.
(* Goal: @Col Tn A B C *)
spliter.
(* Goal: @Col Tn A B C *)
induction H3; spliter.
assert(Col P Q B').
apply col_permutation_1.
eapply proj_col.
(* Goal: False *)
(* Goal: @Col Tn A B C *)
apply H2.

induction(eq_dec_points P A').
(* Goal: @Per Tn P C A *)
(* Goal: @Per Tn P1 C1 A1 *)
subst P.

assert(Perp A' B' A A').
eapply perp_col.
(* Goal: @Le Tn A B C D *)
assumption.
apply perp_left_comm.
eapply perp_col.
2: apply perp_left_comm.
2: apply H4.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: @Col Tn A B C *)
Col.
assert(~Col A' A B').
eapply perp_not_col.
apply perp_comm.
(* Goal: @Perp_at Tn B A B B C *)
(* Goal: not (@eq (@Tpoint Tn) A C) *)
Perp.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
apply H8.
(* Goal: @Col Tn A B C *)
Col.

assert(Perp A' B' A A').
eapply perp_col.
(* Goal: @Le Tn A B C D *)
assumption.
apply perp_left_comm.
eapply perp_col.
2: apply H4.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Col Tn Q A B *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
ColR.
assert(~Col A' A B').
eapply perp_not_col.
apply perp_comm.
(* Goal: @Perp_at Tn B A B B C *)
(* Goal: not (@eq (@Tpoint Tn) A C) *)
Perp.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
apply H9.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: @Col Tn A' B' C' *)
subst A'.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
tauto.
Qed.

Lemma proj_par_strict : forall A B A' B' P Q, A <> A' -> B <> B' -> A' <> B' -> proj A P Q A' -> proj B P Q B' -> Par_strict A A' B B'.

(* Goal: forall (A B C : @Tpoint Tn) (_ : @Par Tn A B A C), @Col Tn A B C *)
intros.
assert(Par A A' B B').
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
eapply (proj_par A B A' B' P Q); auto.
induction H4.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Col Tn A B C *)
spliter.
unfold Par_strict.
repeat split; auto; try apply all_coplanar.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
ex_and H8 X.

assert(~Col P Q A).
eapply proj_not_col.
apply H.
(* Goal: @Le Tn A B C D *)
assumption.

assert(~Col P Q B).
eapply proj_not_col.
(* Goal: False *)
apply H0.
(* Goal: @Le Tn A B C D *)
assumption.

assert(A <> B).
eapply proj_not_eq.
apply H1.
(* Goal: False *)
(* Goal: @Col Tn A B C *)
apply H2.
(* Goal: @Le Tn A B C D *)
assumption.

assert(Col A' P Q).
eapply proj_col.
(* Goal: False *)
(* Goal: @Col Tn A B C *)
apply H2.

assert(Col B' P Q).
eapply proj_col.
apply H3.

apply H1.
eapply (l6_21 P Q).
apply H11.
(* Goal: False *)
apply H0.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: @Col Tn A B C *)
Col.
Qed.

Lemma col_proj_col : forall A B A' B' P Q, A <> A' -> Col A B A' -> proj A P Q A' -> proj B P Q B' -> Col A B B'.
(* Goal: forall (A B C : @Tpoint Tn) (_ : @Par Tn A B A C), @Col Tn A B C *)
intros.
(* Goal: @Le Tn A B D C *)
induction(eq_dec_points A B).
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
subst B.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: @Col Tn A' B' C' *)
unfold proj in *.
(* Goal: @Col Tn A B C *)
spliter.
(* Goal: @Col Tn A B C *)
induction H4; induction H5; spliter.
apply col_permutation_2.
eapply perp2__col.
(* Goal: @Perp Tn C1 P1 A1 C1 *)
(* Goal: @Per Tn P1 C1 A1 *)
apply perp_sym.
apply H6.
apply perp_left_comm.
eapply perp_col.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Perp Tn C1 P1 A1 C1 *)
(* Goal: @Per Tn P1 C1 A1 *)
apply perp_sym.
apply H8.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: @Col Tn A' B' C' *)
subst A'.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
tauto.
(* Goal: @Col Tn A B A' *)
(* Goal: forall _ : @Col Tn A B A', @eq (@Tpoint Tn) A' B' *)
subst B'.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: @Col Tn A B A' *)
(* Goal: forall _ : @Col Tn A B A', @eq (@Tpoint Tn) A' B' *)
subst B'.
(* Goal: @Col Tn A B C *)
Col.
Qed.

Lemma col_proj_proj : forall A B A' P Q, A <> A' -> Col A B A' -> proj A P Q A' -> proj B P Q A'.
(* Goal: forall (A B C : @Tpoint Tn) (_ : @Par Tn A B A C), @Col Tn A B C *)
intros.

(* Goal: @Col Tn A' B' C' *)
unfold proj in *.
(* Goal: @Col Tn A B C *)
spliter.
induction H2;
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
spliter; split;auto.
induction(col_dec P Q B).
(* Goal: or (and (not (@Col Tn Q P A)) (and (@Perp Tn Q P A A) (@Col Tn Q P A))) (and (@Col Tn Q P A) (@eq (@Tpoint Tn) A A)) *)
right.
(* Goal: iff (@Bet Tn M A' B') (@Bet Tn M A B) *)
split.
(* Goal: @Le Tn A B C D *)
assumption.

induction(eq_dec_points A' P).
(* Goal: @Per Tn P C A *)
(* Goal: @Per Tn P1 C1 A1 *)
subst P.
assert(Perp_at A' A' Q A A').
(* Goal: @Perp_at Tn C1 C1 P1 A1 C1 *)
(* Goal: @Per Tn P1 C1 A1 *)
eapply perp_perp_in.
(* Goal: @Le Tn A B C D *)
assumption.
eapply l8_14_2_1b.
apply H6.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: @Col Tn A B C *)
Col.
assert(Perp P A' A A').
eapply perp_col.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
apply H3.
(* Goal: @Le Tn A B C D *)
assumption.

assert(Perp_at A' A' P A A').
(* Goal: @Perp_at Tn C1 C1 P1 A1 C1 *)
(* Goal: @Per Tn P1 C1 A1 *)
eapply perp_perp_in.
(* Goal: @Perp_at Tn B A B B C *)
(* Goal: not (@eq (@Tpoint Tn) A C) *)
Perp.

induction(eq_dec_points B P).
(* Goal: @Per Tn P C A *)
(* Goal: @Per Tn P1 C1 A1 *)
subst P.

assert(Perp B Q A B).
(* Goal: @Perp Tn C1 P1 A1 C1 *)
(* Goal: @Per Tn P1 C1 A1 *)
apply perp_sym.
eapply perp_col.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
subst B.
(* Goal: False *)
(* Goal: @Col Tn A B C *)
apply H2.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: @Perp Tn C1 P1 A1 C1 *)
(* Goal: @Per Tn P1 C1 A1 *)
apply perp_sym.
apply H3.
(* Goal: @Col Tn A B C *)
Col.
eapply l8_14_2_1b.
apply H8.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: @Col Tn A B C *)
Col.

assert(Perp P B A B).
eapply perp_col.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Perp Tn C1 P1 A1 C1 *)
(* Goal: @Per Tn P1 C1 A1 *)
apply perp_sym.
eapply perp_col.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
subst B.
(* Goal: False *)
contradiction.
(* Goal: @Perp Tn C1 P1 A1 C1 *)
(* Goal: @Per Tn P1 C1 A1 *)
apply perp_sym.
apply H3.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: @Col Tn A B C *)
Col.
eapply l8_14_2_1b.
apply H8.
(* Goal: @Col Tn Q A B *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
ColR.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: or (and (not (@Col Tn Q P A)) (and (@Perp Tn Q P A B) (@Col Tn Q P B))) (and (@Col Tn Q P A) (@eq (@Tpoint Tn) B A)) *)
(* Goal: or (and (not (@Col Tn Q P A)) (and (@Perp Tn Q P A B) (@Col Tn Q P B))) (and (@Col Tn Q P A) (@eq (@Tpoint Tn) B A)) *)
left.
(* Goal: and (@Bet Tn D C P') (@Cong Tn D P' A B) *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
repeat split; auto.
(* Goal: @Perp Tn C1 P1 A1 C1 *)
(* Goal: @Per Tn P1 C1 A1 *)
apply perp_sym.
apply perp_left_comm.
eapply perp_col.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
(* Goal: @Col Tn A' B' C' *)
subst A'.
(* Goal: False *)
contradiction.
(* Goal: @Perp Tn C1 P1 A1 C1 *)
(* Goal: @Per Tn P1 C1 A1 *)
apply perp_sym.
apply perp_right_comm.
apply H3.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: @Col Tn A' B' C' *)
subst A'.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
tauto.
Qed.



Lemma proj_id : forall A B A' B' P Q, A <> A' -> Col A B A' -> proj A P Q A' -> proj B P Q B' -> A'= B'.
(* Goal: forall (A B C : @Tpoint Tn) (_ : @Par Tn A B A C), @Col Tn A B C *)
intros.

assert(proj B P Q A').
eapply col_proj_proj.
apply H.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Le Tn A B C D *)
assumption.
eapply proj_uniqueness.
apply H3.
(* Goal: @Le Tn A B C D *)
assumption.
Qed.

Lemma proj_diff : forall A P Q A' , proj A P Q A' -> P <> Q.
(* Goal: forall (A B C : @Tpoint Tn) (_ : @Par Tn A B A C), @Col Tn A B C *)
intros.
(* Goal: not (@eq (@Tpoint Tn) P Q) *)
unfold proj in H.
(* Goal: @Col Tn A B C *)
spliter.
(* Goal: @Le Tn A B C D *)
assumption.
Qed.


Lemma proj3_col : forall A B C A' B' C' P Q , proj A P Q A' -> proj B P Q B' -> proj C P Q C' -> Col A' B' C'.
(* Goal: forall (A B C : @Tpoint Tn) (_ : @Par Tn A B A C), @Col Tn A B C *)
intros.
(* Goal: @Col Tn A' B' C' *)
unfold proj in *.
(* Goal: @Col Tn A B C *)
spliter.

(* Goal: @Col Tn A B C *)
induction H4; induction H3; induction H2; spliter.
(* Goal: @Col Tn A B C *)
eapply (col3 P Q); Col.
(* Goal: @Col Tn A B C' *)
subst C'.
(* Goal: @Col Tn A B C *)
eapply (col3 P Q); Col.
(* Goal: @Col Tn A B A' *)
(* Goal: forall _ : @Col Tn A B A', @eq (@Tpoint Tn) A' B' *)
subst B'.
(* Goal: @Col Tn A B C *)
eapply (col3 P Q); Col.
(* Goal: @Col Tn A B C' *)
subst C'.
(* Goal: @Col Tn A B A' *)
(* Goal: forall _ : @Col Tn A B A', @eq (@Tpoint Tn) A' B' *)
subst B'.
(* Goal: @Col Tn A B C *)
eapply (col3 P Q); Col.
(* Goal: @Col Tn A' B' C' *)
subst A'.
(* Goal: @Col Tn A B C *)
eapply (col3 P Q); Col.
(* Goal: @Col Tn A B C' *)
subst C'.
(* Goal: @Col Tn A' B' C' *)
subst A'.
(* Goal: @Col Tn A B C *)
eapply (col3 P Q); Col.
(* Goal: @Col Tn A' B' C' *)
subst A'.
(* Goal: @Col Tn A B A' *)
(* Goal: forall _ : @Col Tn A B A', @eq (@Tpoint Tn) A' B' *)
subst B'.
(* Goal: @Col Tn A B C *)
eapply (col3 P Q); Col.
(* Goal: @Col Tn A' B' C' *)
subst A'.
(* Goal: @Col Tn A B A' *)
(* Goal: forall _ : @Col Tn A B A', @eq (@Tpoint Tn) A' B' *)
subst B'.
(* Goal: @Col Tn A B C' *)
subst C'.
(* Goal: @Col Tn A B C *)
eapply (col3 P Q); Col.
Qed.

Lemma proj3_id : forall A B C C' P Q, A <> B -> Col A B C -> proj A P Q A -> proj B P Q B -> proj C P Q C' -> C = C'.
(* Goal: forall (A B C : @Tpoint Tn) (_ : @Par Tn A B A C), @Col Tn A B C *)
intros.
(* Goal: @eq (@Tpoint Tn) C C' *)
assert(Col A B C').
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
eapply (proj3_col A B C A B C' P Q); auto.

(* Goal: @eq (@Tpoint Tn) C C' *)
assert(HH1:= H1).
(* Goal: @eq (@Tpoint Tn) C C' *)
assert(HH2:=H2).
(* Goal: @eq (@Tpoint Tn) C C' *)
assert(HH3:=H3).

(* Goal: @eq (@Tpoint Tn) C C' *)
unfold proj in HH1.
(* Goal: @eq (@Tpoint Tn) C C' *)
unfold proj in HH2.
(* Goal: @eq (@Tpoint Tn) C C' *)
unfold proj in HH3.
(* Goal: @Col Tn A B C *)
spliter.
(* Goal: @Col Tn A B C *)
induction H10; induction H8; induction H6; spliter.
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
apply perp_not_eq_2 in H15.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
tauto.
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
apply perp_not_eq_2 in H14.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
tauto.
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
apply perp_not_eq_2 in H14.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
tauto.
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
apply perp_not_eq_2 in H13.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
tauto.
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
apply perp_not_eq_2 in H13.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
tauto.
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
apply perp_not_eq_2 in H12.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
tauto.
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
assert(Col P A B).
(* Goal: @Col Tn Q A B *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
ColR.
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
assert(Col Q A B).
(* Goal: @Col Tn Q A B *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
ColR.


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


eapply (l8_14_2_1b_bis _ _ _ _ C') in H7.
(* Goal: False *)
contradiction.
(* Goal: False *)
subst C.
(* Goal: @eq (@Tpoint Tn) C' C' *)
reflexivity.
Qed.

Lemma proj_inv_exists : forall P Q A', P <> Q -> Col P Q A'  -> exists A, A <> A' /\ proj A P Q A'.
(* Goal: forall (A B C : @Tpoint Tn) (_ : @Par Tn A B A C), @Col Tn A B C *)
intros.
assert(HH0:= not_col_exists P Q H).
ex_and HH0 X.

induction(eq_dec_points A' P).
(* Goal: @Per Tn P C A *)
(* Goal: @Per Tn P1 C1 A1 *)
subst P.

assert(Q <> A').
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
apply H.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
apply col_permutation_1 in H0.
assert(~Col Q A' X).
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
apply H1.
(* Goal: @Col Tn A B C *)
Col.
assert(HH:= ex_per_cong Q A' A' X A' Q H2 H H0 H3).
ex_and HH A.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X A B) (@Col Tn X A C)) *)
(* Goal: @Col Tn A B C *)
exists A.
(* Goal: iff (@Bet Tn M A' B') (@Bet Tn M A B) *)
split.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
(* Goal: @Col Tn A' B' C' *)
subst A'.
apply cong_symmetry in H5.
apply cong_identity in H5.
(* Goal: False *)
contradiction.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
eapply per_proj; auto.
(* Goal: @Per Tn A1 C1 C1 *)
apply l8_5.
(* Goal: @Col Tn A B C *)
Col.
assert(HH:= ex_per_cong P Q A' X P Q H H H0 H1).
ex_and HH A.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X A B) (@Col Tn X A C)) *)
(* Goal: @Col Tn A B C *)
exists A.
(* Goal: iff (@Bet Tn M A' B') (@Bet Tn M A B) *)
split.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
(* Goal: @Col Tn A' B' C' *)
subst A'.
apply cong_symmetry in H4.
apply cong_identity in H4.
(* Goal: False *)
contradiction.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
apply per_proj; auto.
eapply per_col.
2: apply H3.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Col Tn A B C *)
Col.
Qed.

Lemma proj_perp_id : forall A B C A' B' P Q, A <> C -> Col A B C -> 
                                                         proj A P Q A' -> proj B P Q B' -> proj C P Q A' ->
                                                         A' = B'.
(* Goal: forall (A B C : @Tpoint Tn) (_ : @Par Tn A B A C), @Col Tn A B C *)
intros.

induction(eq_dec_points A A').
(* Goal: @Col Tn A' B' C' *)
subst A'.

eapply proj_id.
(* Goal: False *)
(* Goal: @Col Tn A B C *)
4:apply H2.
3: apply H3.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Col Tn A B C *)
Col.

assert(Col A C A').
eapply proj_eq_col.
apply H1.
(* Goal: @Le Tn A B C D *)
assumption.
assert(Col A B A').
(* Goal: @Col Tn Q A B *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
ColR.

eapply proj_id.
apply H4.
apply H6.
apply H1.
(* Goal: @Le Tn A B C D *)
assumption.
Qed.

Lemma proj_diff_not_col : forall A B A' B' P Q, A <> A' -> proj A P Q A' -> proj B P Q B' ->  (A' <> B' <-> ~Col A B A').
(* Goal: forall (A B C : @Tpoint Tn) (_ : @Par Tn A B A C), @Col Tn A B C *)
intros.
(* Goal: iff (@Bet Tn M A' B') (@Bet Tn M A B) *)
split.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.

(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
assert(proj B P Q A').
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
eapply (col_proj_proj A); auto.
(* Goal: False *)
(* Goal: @Col Tn A B C *)
apply H2.
eapply proj_uniqueness.
apply H4.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
(* Goal: @Col Tn A B A' *)
(* Goal: forall _ : @Col Tn A B A', @eq (@Tpoint Tn) A' B' *)
subst B'.
(* Goal: False *)
(* Goal: @Col Tn A B C *)
apply H2.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
eapply (proj_eq_col _ _ P Q); auto.
Qed.

Lemma proj_diff_not_col_inv : forall A B A' B' P Q, A <> A' -> proj A P Q A' -> proj B P Q B' ->  (A' = B' <-> Col A B A').
(* Goal: forall (A B C : @Tpoint Tn) (_ : @Par Tn A B A C), @Col Tn A B C *)
intros.
(* Goal: iff (@Bet Tn M A' B') (@Bet Tn M A B) *)
split.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
(* Goal: @Col Tn A B A' *)
(* Goal: forall _ : @Col Tn A B A', @eq (@Tpoint Tn) A' B' *)
subst B'.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
eapply (proj_eq_col A B P Q A'); auto.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
eapply (proj_id A B A' B' P Q); auto.
Qed.

Lemma proj_preserves_bet1 : forall A B C B' C' P Q, Bet A B C -> 
                                                         proj A P Q A -> proj B P Q B' -> proj C P Q C' ->
                                                         Bet A B' C'.
(* Goal: forall (A B C : @Tpoint Tn) (_ : @Par Tn A B A C), @Col Tn A B C *)
intros.
(* Goal: @Le Tn A B D C *)
induction(eq_dec_points A B).
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
subst B.
assert(A = B').
eapply proj_uniqueness.
(* Goal: False *)
apply H0.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Col Tn A B A' *)
(* Goal: forall _ : @Col Tn A B A', @eq (@Tpoint Tn) A' B' *)
subst B'.
apply between_trivial2.
induction(eq_dec_points B C).
(* Goal: False *)
subst C.
assert(B' = C').
eapply proj_uniqueness.
apply H1.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Col Tn A B C' *)
subst C'.
(* Goal: @Bet Tn D C C *)
(* Goal: @Cong Tn A B D C *)
(* Goal: @Le Tn A B D C *)
apply between_trivial.
assert(A <> C).
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
(* Goal: False *)
subst C.
apply between_identity in H.
(* Goal: False *)
contradiction.

assert(P <> Q).
eapply proj_diff.
(* Goal: False *)
apply H0.
assert(Col A P Q).
eapply proj_col.
(* Goal: False *)
apply H0.
assert(Col B' P Q).
eapply proj_col.
apply H1.
assert(Col C' P Q).
eapply proj_col.
(* Goal: False *)
(* Goal: @Col Tn A B C *)
apply H2.

assert(Col A B C).
eapply bet_col.
(* Goal: @Le Tn A B C D *)
assumption.

induction(eq_dec_points B B').
(* Goal: @Col Tn A B A' *)
(* Goal: forall _ : @Col Tn A B A', @eq (@Tpoint Tn) A' B' *)
subst B'.

assert(C = C').

(* Goal: @Col Tn A B C *)
apply (proj3_id A B C C' P Q); Col.
(* Goal: @Col Tn A B C' *)
subst C'.
(* Goal: @Le Tn A B C D *)
assumption.

induction (eq_dec_points A C').
(* Goal: @Col Tn A B C' *)
subst C'.

assert(Col P A B').
(* Goal: @Col Tn Q A B *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
ColR.
assert(proj B P Q A).
eapply col_proj_proj.
(* Goal: False *)
(* Goal: @Col Tn A B C *)
3: apply H2.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Col Tn A B C *)
Col.
assert(A = B').
eapply proj_uniqueness.
apply H13.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Col Tn A B A' *)
(* Goal: forall _ : @Col Tn A B A', @eq (@Tpoint Tn) A' B' *)
subst B'.
apply l7_3_2.

induction(eq_dec_points B' C').
(* Goal: @Col Tn A B C' *)
subst C'.
(* Goal: @Bet Tn D C C *)
(* Goal: @Cong Tn A B D C *)
(* Goal: @Le Tn A B D C *)
apply between_trivial.

assert(HH:= proj_not_eq_not_col B C B' C' P Q H13 H11 H1 H2).

assert(A <> B').
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
(* Goal: @Col Tn A B A' *)
(* Goal: forall _ : @Col Tn A B A', @eq (@Tpoint Tn) A' B' *)
subst B'.

assert(Col B C C').
eapply col_proj_col.
(* Goal: False *)
(* Goal: @Col Tn A B C *)
4:apply H2.
3: apply H1.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: and (not (@eq (@Tpoint Tn) B A)) (and (@Col Tn B' B A) (@Col Tn A' B A)) *)
(* Goal: False *)
apply HH.
(* Goal: @Col Tn Q A B *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
ColR.

assert(HH1:= proj_one_side B C B' C' P Q H11 H1 H2).

assert(Col A B' C').
eapply proj3_col.
(* Goal: False *)
apply H0.
apply H1.
(* Goal: False *)
(* Goal: @Col Tn A B C *)
apply H2.
induction HH1.

(* Goal: @Col Tn A B C *)
(* Goal: @Col Tn A B C *)
apply False_ind.
(* Goal: and (not (@eq (@Tpoint Tn) B A)) (and (@Col Tn B' B A) (@Col Tn A' B A)) *)
(* Goal: False *)
apply HH.
assert(Col A B B').
(* Goal: @Col Tn Q A B *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
ColR.
(* Goal: @Col Tn Q A B *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
ColR.

assert(TS B B' A C).
unfold TS.
(* Goal: iff (@Bet Tn M A' B') (@Bet Tn M A B) *)
repeat split.
assert(~Col B B' A).
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
eapply proj_not_eq_not_col; auto.
apply H1.
(* Goal: False *)
apply H0.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
apply H17.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
(* Goal: and (not (@eq (@Tpoint Tn) B A)) (and (@Col Tn B' B A) (@Col Tn A' B A)) *)
(* Goal: False *)
apply HH.
apply col_permutation_2.
eapply (col_transitivity_1 _ A).
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: @Col Tn Q A B *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
ColR.
exists B.
(* Goal: @Col Tn A B C *)
split; Col.

assert(TS B B' A C').
apply l9_2.
eapply l9_8_2.
apply l9_2.
apply H17.
(* Goal: @Le Tn A B C D *)
assumption.
unfold TS in H18.
(* Goal: @Col Tn A B C *)
spliter.
ex_and H20 BB.

assert(BB= B').
eapply l6_21.
apply not_col_permutation_1.
apply H19.
4: apply col_permutation_2.
4: apply bet_col.
4: apply H21.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: @Col Tn A B C *)
Col.
subst BB.
(* Goal: @Le Tn A B C D *)
assumption.
Qed.

Lemma proj_preserves_bet : forall A B C A' B' C' P Q, Bet A B C -> 
                                                         proj A P Q A' -> proj B P Q B' -> proj C P Q C' ->
                                                         Bet A' B' C'.
(* Goal: forall (A B C : @Tpoint Tn) (_ : @Par Tn A B A C), @Col Tn A B C *)
intros.


(* Goal: @Le Tn A B D C *)
induction(eq_dec_points A B).
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
subst B.
assert(A' = B').
eapply proj_uniqueness.
(* Goal: False *)
apply H0.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Col Tn A B A' *)
(* Goal: forall _ : @Col Tn A B A', @eq (@Tpoint Tn) A' B' *)
subst B'.
apply between_trivial2.
induction(eq_dec_points B C).
(* Goal: False *)
subst C.
assert(B' = C').
eapply proj_uniqueness.
apply H1.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Col Tn A B C' *)
subst C'.
(* Goal: @Bet Tn D C C *)
(* Goal: @Cong Tn A B D C *)
(* Goal: @Le Tn A B D C *)
apply between_trivial.
assert(A <> C).
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
(* Goal: False *)
subst C.
apply between_identity in H.
(* Goal: False *)
contradiction.

induction (eq_dec_points A' C').
(* Goal: @Col Tn A B C' *)
subst C'.

assert(A' = B').
eapply proj_perp_id.
4: apply H1.
(* Goal: False *)
3: apply H0.
(* Goal: False *)
(* Goal: @Col Tn A B C *)
3: apply H2.
(* Goal: @Le Tn A B C D *)
assumption.
apply bet_col.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Col Tn A B A' *)
(* Goal: forall _ : @Col Tn A B A', @eq (@Tpoint Tn) A' B' *)
subst B'.
apply l7_3_2.

assert(P <> Q).
eapply proj_diff.
(* Goal: False *)
apply H0.
assert(Col A' P Q).
eapply proj_col.
(* Goal: False *)
apply H0.
assert(Col B' P Q).
eapply proj_col.
apply H1.
assert(Col C' P Q).
eapply proj_col.
(* Goal: False *)
(* Goal: @Col Tn A B C *)
apply H2.

assert(Col A B C).
eapply bet_col.
(* Goal: @Le Tn A B C D *)
assumption.

induction (eq_dec_points A A').
(* Goal: @Col Tn A' B' C' *)
subst A'.
(* Goal: @Le Tn A B C D *)
eapply (proj_preserves_bet1 A B C _ _ P Q); assumption.

assert(~Col A P Q).
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.

apply proj_not_col in H0.
(* Goal: False *)
apply H0.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: @Le Tn A B C D *)
assumption.

induction (eq_dec_points B B').
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
subst B.

assert(C <> C').
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
(* Goal: @Col Tn A B C' *)
subst C'.
apply H13.
assert(Col B' C P).
(* Goal: @Col Tn Q A B *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
ColR.
assert(Col B' C Q).
(* Goal: @Col Tn Q A B *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
ColR.
(* Goal: @Col Tn A B C *)
eapply (col3 B' C); Col.
apply col_permutation_1 in H9.

assert(~Col C P Q).
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
apply proj_not_col in H2.
(* Goal: False *)
(* Goal: @Col Tn A B C *)
apply H2.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: @Le Tn A B C D *)
assumption.

assert(HH:= proj_inv_exists P Q B' H7 H9).
ex_and HH B.

assert(HH:=proj_diff_not_col_inv B A B' A' P Q H16 H17 H0).
destruct HH.

assert(HH:=proj_diff_not_col_inv B C B' C' P Q H16 H17 H2).
destruct HH.

assert(HH:= proj_one_side B A B' A' P Q H16 H17 H0).
induction HH.
assert(B' = A').
apply H19.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: @Col Tn A B A' *)
(* Goal: forall _ : @Col Tn A B A', @eq (@Tpoint Tn) A' B' *)
subst B'.
apply between_trivial2.

assert(HH:= proj_one_side B C B' C' P Q H16 H17 H2).
induction HH.

assert(B' = C').
apply H21.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: @Col Tn A B A' *)
(* Goal: forall _ : @Col Tn A B A', @eq (@Tpoint Tn) A' B' *)
subst B'.
(* Goal: @Bet Tn D C C *)
(* Goal: @Cong Tn A B D C *)
(* Goal: @Le Tn A B D C *)
apply between_trivial.

(*********************************************)


assert(HH:=proj_diff_not_col_inv B A B' A' P Q H16 H17 H0).
destruct HH.

assert(HH:=proj_diff_not_col_inv B C B' C' P Q H16 H17 H2).
destruct HH.

assert(TS B B' A C).
unfold TS.
(* Goal: iff (@Bet Tn M A' B') (@Bet Tn M A B) *)
repeat split.

(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
assert(B' = A').
apply H25.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: @Col Tn A B A' *)
(* Goal: forall _ : @Col Tn A B A', @eq (@Tpoint Tn) A' B' *)
subst B'.

assert(Col A' B C).
(* Goal: @Col Tn Q A B *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
ColR.
assert(A' = C').
apply H27.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: False *)
contradiction.

(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
assert(B' = C').
apply H27.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: @Col Tn A B A' *)
(* Goal: forall _ : @Col Tn A B A', @eq (@Tpoint Tn) A' B' *)
subst B'.

assert(Col C' A C).
(* Goal: @Col Tn Q A B *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
ColR.
assert(C' = A').
apply H25.
(* Goal: @Col Tn Q A B *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
ColR.
(* Goal: @Col Tn A B C' *)
subst C'.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
tauto.

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


assert(TS B B' A' C).
eapply l9_8_2.
apply H28.
(* Goal: @Le Tn A B C D *)
assumption.
assert(TS B B' C' A').
eapply l9_8_2.
apply l9_2.
apply H29.
(* Goal: @Le Tn A B C D *)
assumption.
unfold TS in H30.
(* Goal: @Col Tn A B C *)
spliter.
ex_and H32 BB.

assert(BB= B').
eapply l6_21.
apply not_col_permutation_1.
apply H31.
4: apply col_permutation_2.
4: apply bet_col.
4: apply H33.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
eapply (proj3_col A C B A' C' B' P Q); auto.
subst BB.
Between.

induction(eq_dec_points C C').
(* Goal: @Col Tn A B C' *)
subst C'.

apply between_symmetry.
(* Goal: @Le Tn A B C D *)
eapply (proj_preserves_bet1 C B A _ _ P Q); try assumption.
Between.

assert(HH:=proj_diff_not_col_inv B A B' A' P Q H14 H1 H0).
destruct HH.

assert(HH:=proj_diff_not_col_inv B C B' C' P Q H14 H1 H2).
destruct HH.

assert(HH:= proj_one_side B A B' A' P Q H14 H1 H0).
induction HH.
assert(B' = A').
apply H17.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: @Col Tn A B A' *)
(* Goal: forall _ : @Col Tn A B A', @eq (@Tpoint Tn) A' B' *)
subst B'.
apply between_trivial2.

assert(HH:= proj_one_side B C B' C' P Q H14 H1 H2).
induction HH.

assert(B' = C').
apply H19.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: @Col Tn A B A' *)
(* Goal: forall _ : @Col Tn A B A', @eq (@Tpoint Tn) A' B' *)
subst B'.
(* Goal: @Bet Tn D C C *)
(* Goal: @Cong Tn A B D C *)
(* Goal: @Le Tn A B D C *)
apply between_trivial.

assert(HH:=proj_diff_not_col_inv B A B' A' P Q H14 H1 H0).
destruct HH.

assert(HH:=proj_diff_not_col_inv B C B' C' P Q H14 H1 H2).
destruct HH.

assert(TS B B' A C).
unfold TS.
(* Goal: iff (@Bet Tn M A' B') (@Bet Tn M A B) *)
repeat split.

(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
assert(B' = A').
apply H23.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: @Col Tn A B A' *)
(* Goal: forall _ : @Col Tn A B A', @eq (@Tpoint Tn) A' B' *)
subst B'.

assert(Col A' B C).
(* Goal: @Col Tn Q A B *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
ColR.
assert(A' = C').
apply H25.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: False *)
contradiction.

(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
assert(B' = C').
apply H25.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: @Col Tn A B A' *)
(* Goal: forall _ : @Col Tn A B A', @eq (@Tpoint Tn) A' B' *)
subst B'.

assert(Col C' A C).
(* Goal: @Col Tn Q A B *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
ColR.
assert(C' = A').
apply H23.
(* Goal: @Col Tn Q A B *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
ColR.
(* Goal: @Col Tn A B C' *)
subst C'.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
tauto.

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


assert(TS B B' A' C).
eapply l9_8_2.
apply H26.
(* Goal: @Le Tn A B C D *)
assumption.
assert(TS B B' C' A').
eapply l9_8_2.
apply l9_2.
apply H27.
(* Goal: @Le Tn A B C D *)
assumption.
unfold TS in H28.
(* Goal: @Col Tn A B C *)
spliter.
ex_and H30 BB.

assert(BB= B').
eapply l6_21.
apply not_col_permutation_1.
apply H29.
4: apply col_permutation_2.
4: apply bet_col.
4: apply H31.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
eapply (proj3_col A C B A' C' B' P Q); auto.
subst BB.
Between.
Qed.

Lemma one_side_eq_o : forall A B C D, A <> B -> OS A B C D -> eq_o A B C A B D.
(* Goal: forall (A B C : @Tpoint Tn) (_ : @Par Tn A B A C), @Col Tn A B C *)
intros.
assert(HH:= H0).
unfold OS in HH.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => proj T A B P) *)
ex_and HH P.
unfold TS in H2.
assert(~ Col D A B).
(* Goal: @Col Tn A B C *)
spliter.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Col Tn A B C *)
spliter.
unfold TS in H1.
assert(~ Col C A B).
(* Goal: @Col Tn A B C *)
spliter.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Col Tn A B C *)
spliter.
clear H7 H8 H4 H5.
(* Goal: eq_o A B P A1 B1 P1 *)
unfold eq_o.
(* Goal: iff (@Bet Tn M A' B') (@Bet Tn M A B) *)
repeat split.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
apply H6.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
apply H3.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: forall (A B C : @Tpoint Tn) (_ : @Par Tn A B A C), @Col Tn A B C *)
intros.
apply l7_3 in H11.
subst M.
assert(HH:=H13).
unfold Midpoint in HH.
(* Goal: @Col Tn A B C *)
spliter.

assert(Col A C0 C1).
eapply perp2__col.
(* Goal: @Perp Tn C1 P1 A1 C1 *)
(* Goal: @Per Tn P1 C1 A1 *)
apply perp_sym.
apply perp_comm.
apply H4.
(* Goal: @Perp Tn C1 P1 A1 C1 *)
(* Goal: @Per Tn P1 C1 A1 *)
apply perp_sym.
(* Goal: @Perp_at Tn B A B B C *)
(* Goal: not (@eq (@Tpoint Tn) A C) *)
Perp.

assert(C1 <> A).
apply perp_not_eq_2 in H7.
(* Goal: @Le Tn A B C D *)
assumption.

assert(C0 <> A).
apply perp_not_eq_2 in H4.
(* Goal: @Le Tn A B C D *)
assumption.

(* Goal: or (and (not (@Col Tn Q P A)) (and (@Perp Tn Q P A B) (@Col Tn Q P B))) (and (@Col Tn Q P A) (@eq (@Tpoint Tn) B A)) *)
(* Goal: or (and (not (@Col Tn Q P A)) (and (@Perp Tn Q P A B) (@Col Tn Q P B))) (and (@Col Tn Q P A) (@eq (@Tpoint Tn) B A)) *)
left.
induction H16.
eapply between_exchange3.
apply between_symmetry.
apply H16.
(* Goal: @Le Tn A B C D *)
assumption.
induction H16.
eapply outer_transitivity_between2.
apply H16.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Le Tn A B C D *)
assumption.


assert(~Col C1 A B).
eapply perp_not_col in H7.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
apply H7.
(* Goal: @Col Tn A B C *)
Col.

assert(~Col C0 A B).
eapply perp_not_col in H4.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
apply H4.
(* Goal: @Col Tn A B C *)
Col.

assert(TS A B C1 C0).
unfold TS.
(* Goal: and (@Bet Tn D C P') (@Cong Tn D P' A B) *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
repeat split; auto.

(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X A B) (@Col Tn X A C)) *)
(* Goal: @Col Tn A B C *)
exists A.
(* Goal: @Col Tn A B C *)
split; Col.

assert(proj B A C1 A).
(* Goal: proj T A B P *)
unfold proj.
(* Goal: iff (@Bet Tn M A' B') (@Bet Tn M A B) *)
split.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: or (and (not (@Col Tn Q P A)) (and (@Perp Tn Q P A B) (@Col Tn Q P B))) (and (@Col Tn Q P A) (@eq (@Tpoint Tn) B A)) *)
(* Goal: or (and (not (@Col Tn Q P A)) (and (@Perp Tn Q P A B) (@Col Tn Q P B))) (and (@Col Tn Q P A) (@eq (@Tpoint Tn) B A)) *)
left.
(* Goal: iff (@Bet Tn M A' B') (@Bet Tn M A B) *)
repeat split.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
apply H19.
(* Goal: @Col Tn A B C *)
Col.
apply perp_comm.
(* Goal: @Perp_at Tn B A B B C *)
(* Goal: not (@eq (@Tpoint Tn) A C) *)
Perp.
(* Goal: @Col Tn A B C *)
Col.

assert(proj C A C1 C0).
eapply proj_col_proj.
apply H5.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
apply bet_col in H16.
(* Goal: @Col Tn A B C *)
Col.

assert( HH:=proj_one_side B C A C0 A C1).
assert(Col C B A \/ OS B A C C0).
apply HH;
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
induction H24.
(* Goal: @Col Tn A B C *)
(* Goal: @Col Tn A B C *)
apply False_ind.
apply H6.
(* Goal: @Col Tn A B C *)
Col.

assert( HH1:=proj_one_side B D A C1 A C1).
assert(Col D B A \/ OS B A D C1).
apply HH1;
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
induction H25.
(* Goal: @Col Tn A B C *)
(* Goal: @Col Tn A B C *)
apply False_ind.
apply H3.
(* Goal: @Col Tn A B C *)
Col.
clear HH HH1.
assert(OS A B C0 C1).
eapply one_side_transitivity.
apply one_side_symmetry.
apply invert_one_side.
apply H24.
eapply one_side_transitivity.
(* Goal: False *)
apply H0.
apply invert_one_side.
(* Goal: @Le Tn A B C D *)
assumption.
apply l9_9 in H21.
apply one_side_symmetry in H26.
(* Goal: False *)
contradiction.
Qed.


Lemma out_preserves_eq_o : forall A B B' P, ~Col A B  P -> Out A B B' -> eq_o A B P A B' P.
(* Goal: forall (A B C : @Tpoint Tn) (_ : @Par Tn A B A C), @Col Tn A B C *)
intros.
assert(A <> B /\ A <> B').

unfold Out in H0.
(* Goal: @Col Tn A B C *)
spliter.
(* Goal: and (@Bet Tn D C P') (@Cong Tn D P' A B) *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
split; auto.
(* Goal: @Col Tn A B C *)
spliter.
(* Goal: eq_o A B P A1 B1 P1 *)
unfold eq_o.
(* Goal: iff (@Bet Tn M A' B') (@Bet Tn M A B) *)
repeat split.
(* Goal: @Le Tn A B C D *)
assumption.
apply out_col in H0.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
apply H.
(* Goal: @Col Tn Q A B *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
ColR.
(* Goal: forall (A B C : @Tpoint Tn) (_ : @Par Tn A B A C), @Col Tn A B C *)
intros.
apply l7_3 in H9.
subst M.

assert(A <> C).
apply perp_not_eq_2 in H3.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
assert(A <> C1).
apply perp_not_eq_2 in H5.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.

assert(Perp A B C1 A).
eapply perp_col.
(* Goal: @Le Tn A B C D *)
assumption.
apply H5.
apply out_col in H0.
(* Goal: @Col Tn A B C *)
Col.

assert(Col A C C1).
eapply perp2__col.
(* Goal: @Perp Tn C1 P1 A1 C1 *)
(* Goal: @Per Tn P1 C1 A1 *)
apply perp_sym.
apply perp_comm.
apply H3.
apply perp_comm.
(* Goal: @Perp_at Tn B A B B C *)
(* Goal: not (@eq (@Tpoint Tn) A C) *)
Perp.

assert(proj B A C1 A).
(* Goal: proj T A B P *)
unfold proj.
(* Goal: and (@Bet Tn D C P') (@Cong Tn D P' A B) *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
split; auto.
(* Goal: or (and (not (@Col Tn Q P A)) (and (@Perp Tn Q P A B) (@Col Tn Q P B))) (and (@Col Tn Q P A) (@eq (@Tpoint Tn) B A)) *)
(* Goal: or (and (not (@Col Tn Q P A)) (and (@Perp Tn Q P A B) (@Col Tn Q P B))) (and (@Col Tn Q P A) (@eq (@Tpoint Tn) B A)) *)
left.
(* Goal: iff (@Bet Tn M A' B') (@Bet Tn M A B) *)
repeat split.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
apply perp_not_col in H14.
apply H14.
(* Goal: @Col Tn A B C *)
Col.
apply perp_comm.
(* Goal: @Perp_at Tn B A B B C *)
(* Goal: not (@eq (@Tpoint Tn) A C) *)
Perp.
(* Goal: @Col Tn A B C *)
Col.

assert(proj P A C C1).
eapply proj_col_proj.
apply H6.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Col Tn A B C *)
Col.
assert(C= C1).
eapply proj_uniqueness.
2:apply H17.
(* Goal: @Le Tn A B C D *)
assumption.
subst C1.
clear H17 H6 H14.

(* Goal: or (and (not (@Col Tn Q P A)) (and (@Perp Tn Q P A B) (@Col Tn Q P B))) (and (@Col Tn Q P A) (@eq (@Tpoint Tn) B A)) *)
(* Goal: or (and (not (@Col Tn Q P A)) (and (@Perp Tn Q P A B) (@Col Tn Q P B))) (and (@Col Tn Q P A) (@eq (@Tpoint Tn) B A)) *)
left.
apply midpoint_bet.
(* Goal: @Le Tn A B C D *)
assumption.
Qed.

Lemma cong_identity_inv : forall A B C, A <> B -> ~Cong A B C C.
(* Goal: forall (A B C : @Tpoint Tn) (_ : @Par Tn A B A C), @Col Tn A B C *)
intros.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
apply H.
eapply cong_identity.
(* Goal: False *)
apply H0.
Qed.

Lemma midpoint_col : forall A B A' B' M, A <> B -> Midpoint M A A' -> Midpoint M B B' -> Col A B B' -> A' <> B' /\ Col A A' B' /\ Col B A' B'.
(* Goal: forall (A B C : @Tpoint Tn) (_ : @Par Tn A B A C), @Col Tn A B C *)
intros.
assert(A' <> B').
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
apply H.
assert(Cong A' B' A B).
eapply l7_13.
(* Goal: False *)
apply H0.
(* Goal: @Le Tn A B C D *)
assumption.
apply cong_symmetry in H4.
(* Goal: @Col Tn A B A' *)
(* Goal: forall _ : @Col Tn A B A', @eq (@Tpoint Tn) A' B' *)
subst B'.
apply cong_identity in H4.
(* Goal: @Le Tn A B C D *)
assumption.

assert(HH0:= H0).
(* Goal: @eq (@Tpoint Tn) C C' *)
assert(HH1:= H1).
unfold Midpoint in HH0.
unfold Midpoint in HH1.
(* Goal: @Col Tn A B C *)
spliter.

assert(Col M A A').
apply bet_col in H6.
(* Goal: @Col Tn A B C *)
Col.
assert(Col M B B').
apply bet_col in H4.
(* Goal: @Col Tn A B C *)
Col.

induction(eq_dec_points B B').
(* Goal: @Col Tn A B A' *)
(* Goal: forall _ : @Col Tn A B A', @eq (@Tpoint Tn) A' B' *)
subst B'.
apply l7_3 in H1.
subst M.
Col5.

assert(Col A A' B').

assert(Col B M A).
eapply col_transitivity_1.
apply H10.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: @Col Tn A B C *)
Col.

assert(Col A M B').

eapply col_transitivity_1.
apply H.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: @Col Tn A B C *)
Col.

induction(eq_dec_points A M).
subst M.
apply cong_symmetry in H7.
apply cong_identity in H7.
(* Goal: @Col Tn A' B' C' *)
subst A'.
(* Goal: @Col Tn A B C *)
Col.

eapply col_transitivity_1.
apply H13.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: @Col Tn A B C *)
Col.
repeat split;
(* Goal: @Col Tn A B C *)
Col.

induction(eq_dec_points A B').
(* Goal: @Col Tn A B A' *)
(* Goal: forall _ : @Col Tn A B A', @eq (@Tpoint Tn) A' B' *)
subst B'.
assert(A'=B).
eapply l7_9.
2: apply H1.
(* Goal: @Midpoint Tn M A' A *)
(* Goal: @Col Tn B' A' A *)
(* Goal: False *)
apply l7_2.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Col Tn A' B' C' *)
subst A'.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: @Col Tn Q A B *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
ColR.
Qed.

Lemma midpoint_par : forall A B A' B' M, A <> B -> Midpoint M A A' -> Midpoint M B B' -> Par A B A' B'.
(* Goal: forall (A B C : @Tpoint Tn) (_ : @Par Tn A B A C), @Col Tn A B C *)
intros.

assert(A' <> B').
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
apply H.
assert(Cong A' B' A B).
eapply l7_13.
(* Goal: False *)
apply H0.
(* Goal: @Le Tn A B C D *)
assumption.
apply cong_symmetry in H3.
(* Goal: @Col Tn A B A' *)
(* Goal: forall _ : @Col Tn A B A', @eq (@Tpoint Tn) A' B' *)
subst B'.
apply cong_identity in H3.
(* Goal: @Le Tn A B C D *)
assumption.

induction(col_dec A B B').
assert(A' <> B' /\ Col A A' B' /\ Col B A' B').
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
eapply (midpoint_col _ _ _ _ M); auto.

unfold Par.
(* Goal: or (and (not (@Col Tn Q P A)) (and (@Perp Tn Q P A A) (@Col Tn Q P A))) (and (@Col Tn Q P A) (@eq (@Tpoint Tn) A A)) *)
right.
(* Goal: and (@Bet Tn D C P') (@Cong Tn D P' A B) *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
split; auto.

assert(HH0:= H0).
(* Goal: @eq (@Tpoint Tn) C C' *)
assert(HH1:= H1).
unfold Midpoint in HH0.
unfold Midpoint in HH1.
(* Goal: @Col Tn A B C *)
spliter.

assert(Col M A A').
apply bet_col in H6.
(* Goal: @Col Tn A B C *)
Col.
assert(Col M B B').
apply bet_col in H4.
(* Goal: @Col Tn A B C *)
Col.

unfold Par.
(* Goal: or (and (not (@Col Tn Q P A)) (and (@Perp Tn Q P A B) (@Col Tn Q P B))) (and (@Col Tn Q P A) (@eq (@Tpoint Tn) B A)) *)
(* Goal: or (and (not (@Col Tn Q P A)) (and (@Perp Tn Q P A B) (@Col Tn Q P B))) (and (@Col Tn Q P A) (@eq (@Tpoint Tn) B A)) *)
left.
unfold Par_strict.
repeat split; auto; try apply all_coplanar.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
ex_and H10 X.

prolong X M X' M X.
assert(Col A' B' X').
eapply mid_preserves_col.
(* Goal: False *)
2: apply H0.
2: apply H1.
apply col_permutation_1.
apply H10.
unfold Midpoint.
(* Goal: iff (@Bet Tn M A' B') (@Bet Tn M A B) *)
split.
(* Goal: @Le Tn A B C D *)
assumption.
apply cong_left_commutativity.
(* Goal: @Cong Tn A B D P' *)
Cong.

assert(Col B' X X').
eapply (col_transitivity_1 _ A').
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: @Col Tn A B C *)
Col.
induction(eq_dec_points X X').
subst X'.
apply between_identity in H12.
subst X.

apply H3.
induction(eq_dec_points B M).
subst M.
apply cong_symmetry in H5.
apply cong_identity in H5.
(* Goal: @Col Tn A B A' *)
(* Goal: forall _ : @Col Tn A B A', @eq (@Tpoint Tn) A' B' *)
subst B'.
(* Goal: @Col Tn A B C *)
Col.
apply col_permutation_2.
(* Goal: @Col Tn A B C *)
apply (col_transitivity_1 _ M); Col.

assert(Col X M B').
apply bet_col in H12.
(* Goal: @Col Tn A B C *)
apply (col_transitivity_1 _ X'); Col.

assert(Col X' M B').
apply bet_col in H12.
(* Goal: @Col Tn A B C *)
apply (col_transitivity_1 _ X); Col.

assert(Col M B X).
eapply (col_transitivity_1 ).
2: apply col_permutation_5.
2: apply H9.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
(* Goal: @Col Tn A B A' *)
(* Goal: forall _ : @Col Tn A B A', @eq (@Tpoint Tn) A' B' *)
subst B'.
apply cong_identity in H5.
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
subst B.


apply H3.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: @Col Tn A B C *)
Col.

assert(Col X M A).
eapply (col_transitivity_1 ).
2: apply col_permutation_3.
2:apply H19.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
subst X.

assert(Cong M X' M B').
eapply cong_transitivity.
apply H13.
(* Goal: @Cong Tn A B D P' *)
Cong.
assert (HH:=l7_20 M X' B' H18 H20).
induction HH.
subst X'.
apply H3.
apply col_permutation_2.
apply (col_transitivity_1 _ M).
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
subst M.
apply cong_identity in H13.
(* Goal: False *)
contradiction.
(* Goal: @Col Tn A B C *)
Col.

assert(Col M B A').
(* Goal: @Col Tn Q A B *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
ColR.
induction(eq_dec_points M A').
(* Goal: @Col Tn A' B' C' *)
subst A'.
apply cong_identity in H7.
subst A.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: @Col Tn Q A B *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
ColR.
assert(X'= B).
eapply l7_9.
apply H21.
(* Goal: @Le Tn A B C D *)
assumption.
subst X'.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
tauto.
(* Goal: @Col Tn A B C *)
Col.
apply H3.
eapply col3.
2: apply H20.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
subst X.
apply cong_identity in H13.
subst X'.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
tauto.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: @Col Tn A B C *)
Col.
Qed.

Lemma midpoint_par_strict : forall A B A' B' M, A <> B -> ~Col A B B' -> Midpoint M A A' -> Midpoint M B B' -> Par_strict A B A' B'.
(* Goal: forall (A B C : @Tpoint Tn) (_ : @Par Tn A B A C), @Col Tn A B C *)
intros.
(* Goal: @Par_strict Tn A B A' B' *)
assert(Par A B A' B').
(* Goal: @Le Tn A B C D *)
eapply (midpoint_par A B A' B' M); assumption.
(* Goal: @Par_strict Tn A B A' B' *)
induction H3.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Col Tn A B C *)
spliter.
(* Goal: @Col Tn A B C *)
(* Goal: @Col Tn A B C *)
apply False_ind.

(* Goal: False *)
assert(HH:=midpoint_col B' A' B A M).
(* Goal: False *)
assert(B <> A /\ Col B' B A /\ Col A' B A).
(* Goal: and (not (@eq (@Tpoint Tn) B A)) (and (@Col Tn B' B A) (@Col Tn A' B A)) *)
(* Goal: False *)
apply HH.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Midpoint Tn M A' A *)
(* Goal: @Col Tn B' A' A *)
(* Goal: False *)
apply l7_2.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Midpoint Tn M A' A *)
(* Goal: @Col Tn B' A' A *)
(* Goal: False *)
apply l7_2.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: @Col Tn A B C *)
spliter.
(* Goal: False *)
apply H0.
(* Goal: @Col Tn A B C *)
Col.
Qed.

Lemma le_left_comm : forall A B C D, Le A B C D -> Le B A C D.
(* Goal: forall (A B C : @Tpoint Tn) (_ : @Par Tn A B A C), @Col Tn A B C *)
intros.
(* Goal: @Le Tn B A C D *)
unfold Le in *.
(* Goal: @ex (@Tpoint Tn) (fun E : @Tpoint Tn => and (@Bet Tn C E D) (@Cong Tn B A C E)) *)
ex_and H P.
(* Goal: @ex (@Tpoint Tn) (fun E : @Tpoint Tn => and (@Bet Tn C E D) (@Cong Tn B A C E)) *)
exists P.
(* Goal: iff (@Bet Tn M A' B') (@Bet Tn M A B) *)
split.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Cong Tn A B D P' *)
Cong.
Qed.

Lemma le_right_comm : forall A B C D, Le A B C D -> Le A B D C.
(* Goal: forall (A B C : @Tpoint Tn) (_ : @Par Tn A B A C), @Col Tn A B C *)
intros.
(* Goal: @Le Tn A B D C *)
induction(eq_dec_points D C).
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
subst D.
(* Goal: @Le Tn A B C C *)
(* Goal: @Le Tn A B D C *)
apply le_zero in H.
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
subst B.
(* Goal: @Le Tn A A C C *)
(* Goal: @Le Tn A B D C *)
eapply le_trivial.

(* Goal: @Le Tn A B D C *)
induction(eq_dec_points A B).
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
subst B.
(* Goal: @Le Tn A A D C *)
(* Goal: @Le Tn A B D C *)
apply le_trivial.

(* Goal: @Le Tn A B D C *)
assert(HH:=segment_construction_3 D C A B H0 H1).
(* Goal: @Le Tn A B D C *)
ex_and HH P'.
(* Goal: @Le Tn A B D C *)
unfold Out in H2.
(* Goal: @Col Tn A B C *)
spliter.
(* Goal: @Le Tn A B D C *)
induction H5.

(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
assert(Le D C A B).
(* Goal: @Le Tn D C A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
eapply l5_5_2.
(* Goal: @ex (@Tpoint Tn) (fun E : @Tpoint Tn => and (@Bet Tn D E C) (@Cong Tn A B D E)) *)
exists P'.
(* Goal: and (@Bet Tn D C P') (@Cong Tn D P' A B) *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
split; auto.
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
apply le_left_comm in H6.
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
assert(Cong A B C D).
(* Goal: @Cong Tn A B C D *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
apply le_anti_symmetry.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Le Tn A B D C *)
unfold Le.
(* Goal: @ex (@Tpoint Tn) (fun E : @Tpoint Tn => and (@Bet Tn D E C) (@Cong Tn A B D E)) *)
(* Goal: @Le Tn A B D C *)
exists C.
(* Goal: iff (@Bet Tn M A' B') (@Bet Tn M A B) *)
split.
(* Goal: @Bet Tn D C C *)
(* Goal: @Cong Tn A B D C *)
(* Goal: @Le Tn A B D C *)
apply between_trivial.
(* Goal: @Cong Tn A B D P' *)
Cong.
(* Goal: @Le Tn A B D C *)
unfold Le.
(* Goal: @ex (@Tpoint Tn) (fun E : @Tpoint Tn => and (@Bet Tn D E C) (@Cong Tn A B D E)) *)
exists P'.
(* Goal: iff (@Bet Tn M A' B') (@Bet Tn M A B) *)
split.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Cong Tn A B D P' *)
Cong.
Qed.

Lemma le_comm : forall A B C D, Le A B C D -> Le B A D C.
(* Goal: forall (A B C : @Tpoint Tn) (_ : @Par Tn A B A C), @Col Tn A B C *)
intros.
(* Goal: @Le Tn B A D C *)
apply le_left_comm.
(* Goal: @Le Tn A B D C *)
apply le_right_comm.
(* Goal: @Le Tn A B C D *)
assumption.
Qed.

Lemma le_cong_le : forall A B C A' B' C', Bet A B C -> Bet A' B' C' -> Le A B A' B' -> Cong B C B' C' -> Le A C A' C'.
(* Goal: forall (A B C : @Tpoint Tn) (_ : @Par Tn A B A C), @Col Tn A B C *)
intros.
(* Goal: @Le Tn D C A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
eapply l5_5_2.
unfold Le in H1.
ex_and H1 P.
prolong A C T P B'.
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => proj T A B P) *)
(* Goal: @ex (@Tpoint Tn) (fun P : @Tpoint Tn => proj T A B P) *)
exists T.
(* Goal: iff (@Bet Tn M A' B') (@Bet Tn M A B) *)
split.
(* Goal: @Le Tn A B C D *)
assumption.

assert(Bet A B T).
eapply between_exchange4.
apply H.
(* Goal: @Le Tn A B C D *)
assumption.

eapply l2_11.
apply H6.
2: apply H3.
eapply between_exchange4.
apply H1.
(* Goal: @Le Tn A B C D *)
assumption.
apply cong_left_commutativity.
eapply l2_11.
4: apply cong_left_commutativity.
(* Goal: False *)
(* Goal: @Col Tn A B C *)
4:apply H2.
apply between_symmetry.
eapply between_exchange3.
apply H.
(* Goal: @Le Tn A B C D *)
assumption.
eapply between_exchange3.
apply H1.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Cong Tn A B D P' *)
Cong.
Qed.


Lemma cong_le_le : forall A B C A' B' C', Bet A B C -> Bet A' B' C' -> Le B C B' C' -> Cong A B A' B' -> Le A C A' C'.
(* Goal: forall (A B C : @Tpoint Tn) (_ : @Par Tn A B A C), @Col Tn A B C *)
intros.
apply le_comm.
eapply le_cong_le.
apply between_symmetry.
apply H.
apply between_symmetry.
(* Goal: False *)
apply H0.
apply le_comm.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Cong Tn A B D P' *)
Cong.
Qed.


Lemma bet_le_le : forall A B C A' B' C', Bet A B C -> Bet A' B' C' -> Le A B A' B' -> Le B C B' C' -> Le A C A' C'.
(* Goal: forall (A B C : @Tpoint Tn) (_ : @Par Tn A B A C), @Col Tn A B C *)
intros.
(* Goal: @eq (@Tpoint Tn) C C' *)
assert(HH1:=H1).
(* Goal: @eq (@Tpoint Tn) C C' *)
assert(HH2:=H2).
unfold Le in HH1.
unfold Le in HH2.
ex_and HH1 X.
ex_and HH2 Y.
assert(Le A C A' Y).
eapply le_cong_le.
3: apply H1.
apply H.
(* Goal: @Le Tn A B C D *)
(* assumption. *)

eapply between_inner_transitivity.
(* Goal: False *)
apply H0.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Le Tn A B C D *)
assumption.

induction (eq_dec_points B' Y).
subst Y.

assert(Le A' B' A' C').
(* Goal: @Le Tn A B D C *)
unfold Le.
exists B'.
(* Goal: iff (@Bet Tn M A' B') (@Bet Tn M A B) *)
split.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @eq (@Tpoint Tn) C' C' *)
apply cong_reflexivity.
eapply le_transitivity.
apply H7.
(* Goal: @Le Tn A B C D *)
assumption.

assert(Bet A' Y C').
eapply outer_transitivity_between2.
2: apply H5.

eapply between_inner_transitivity.
(* Goal: False *)
apply H0.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Le Tn A B C D *)
assumption.
eapply le_transitivity.
apply H7.
(* Goal: @Le Tn A B D C *)
unfold Le.
exists Y.
(* Goal: iff (@Bet Tn M A' B') (@Bet Tn M A B) *)
split.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @eq (@Tpoint Tn) C' C' *)
apply cong_reflexivity.
Qed.


Lemma bet_double_bet : forall A B C B' C', Midpoint B' A B -> Midpoint C' A C -> Bet A B' C' -> Bet A B C.
(* Goal: forall (A B C : @Tpoint Tn) (_ : @Par Tn A B A C), @Col Tn A B C *)
intros.
unfold Midpoint in *.
(* Goal: @Col Tn A B C *)
spliter.
assert(Le A B' A C').
(* Goal: @Le Tn A B D C *)
unfold Le.
exists B'.
(* Goal: iff (@Bet Tn M A' B') (@Bet Tn M A B) *)
split.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @eq (@Tpoint Tn) C' C' *)
apply cong_reflexivity.
assert (Le B' B C' C).
eapply l5_6.
apply H4.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Le Tn A B C D *)
assumption.
assert(Le A B A C).
eapply bet_le_le.
apply H.
(* Goal: False *)
apply H0.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Le Tn A B C D *)
assumption.

induction (eq_dec_points A B').
(* Goal: @Col Tn A B A' *)
(* Goal: forall _ : @Col Tn A B A', @eq (@Tpoint Tn) A' B' *)
subst B'.
apply cong_symmetry in H3.
apply cong_identity in H3.
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
subst B.
apply between_trivial2.

assert( A <> C').
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
(* Goal: @Col Tn A B C' *)
subst C'.
apply le_zero in H4.
(* Goal: False *)
contradiction.

assert(A <> B).
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
subst B.
apply between_identity in H.
(* Goal: False *)
contradiction.
assert(A <> C).
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
(* Goal: False *)
subst C.
apply between_identity in H0.
(* Goal: False *)
contradiction.

assert(Out A B C).

assert(Bet A B C' \/ Bet A C' B).
eapply l5_1.
apply H7.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Le Tn A B C D *)
assumption.
induction H11.

eapply l6_7.
apply bet_out.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
apply H11.
apply bet_out.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Le Tn A B C D *)
assumption.

assert(Bet A B C \/ Bet A C B).
eapply l5_1.
2: apply H11.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Le Tn A B C D *)
assumption.
induction H12.
apply bet_out.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Le Tn A B C D *)
assumption.
apply l6_6.
apply bet_out.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Le Tn A B C D *)
assumption.
eapply l6_13_1.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Le Tn A B C D *)
assumption.
Qed.


Lemma bet_half_bet : forall A B C B' C', Bet A B C  -> Midpoint B' A B -> Midpoint C' A C -> Bet A B' C'.
(* Goal: forall (A B C : @Tpoint Tn) (_ : @Par Tn A B A C), @Col Tn A B C *)
intros.
assert(HH0:= H0).
(* Goal: @eq (@Tpoint Tn) C C' *)
assert(HH1:= H1).
unfold Midpoint in H0.
unfold Midpoint in H1.
(* Goal: @Col Tn A B C *)
spliter.

(* Goal: @Le Tn A B D C *)
induction(eq_dec_points A B).
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
subst B.
apply between_identity in H0.
(* Goal: @Col Tn A B A' *)
(* Goal: forall _ : @Col Tn A B A', @eq (@Tpoint Tn) A' B' *)
subst B'.
apply between_trivial2.
assert(A <> C).
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
(* Goal: False *)
subst C.
apply between_identity in H1.
(* Goal: @Col Tn A B C' *)
subst C'.
apply between_identity in H.
(* Goal: False *)
contradiction.
assert(A <> B').
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
(* Goal: @Col Tn A B A' *)
(* Goal: forall _ : @Col Tn A B A', @eq (@Tpoint Tn) A' B' *)
subst B'.
apply cong_symmetry in H3.
apply cong_identity in H3.
(* Goal: False *)
contradiction.
assert(A <> C').
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
(* Goal: @Col Tn A B C' *)
subst C'.
apply cong_symmetry in H2.
apply cong_identity in H2.
(* Goal: False *)
contradiction.

assert(Col A B' C').
apply bet_col in H0.
apply bet_col in H1.
apply bet_col in H.
(* Goal: @Col Tn Q A B *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
ColR.
induction H8.
(* Goal: @Le Tn A B C D *)
assumption.
induction H8.
apply between_symmetry in H8.

assert(Bet A C B).
eapply bet_double_bet.
apply HH1.
apply HH0.
(* Goal: @Le Tn A B C D *)
assumption.

assert(B = C).
eapply between_equality.
apply between_symmetry.
apply H9.
Between.
(* Goal: False *)
subst C.
assert(B' = C').
eapply l7_17.
apply HH0.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Col Tn A B C' *)
subst C'.
(* Goal: @Bet Tn D C C *)
(* Goal: @Cong Tn A B D C *)
(* Goal: @Le Tn A B D C *)
apply between_trivial.

(***********************************)

assert(Bet A B' C).
eapply between_exchange4.
(* Goal: False *)
apply H0.
(* Goal: @Le Tn A B C D *)
assumption.

assert(Out A B' C').
unfold Out.
(* Goal: and (@Bet Tn D C P') (@Cong Tn D P' A B) *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
repeat split; auto.
eapply l5_3.
apply H9.
(* Goal: @Le Tn A B C D *)
assumption.
eapply l6_4_1 in H10.
(* Goal: @Col Tn A B C *)
spliter.
apply between_symmetry in H8.
(* Goal: False *)
contradiction.
Qed.

Lemma midpoint_preserves_bet : forall A B C B' C', Midpoint B' A B -> Midpoint C' A C -> (Bet A B C <-> Bet A B' C').
(* Goal: forall (A B C : @Tpoint Tn) (_ : @Par Tn A B A C), @Col Tn A B C *)
intros.
(* Goal: iff (@Bet Tn M A' B') (@Bet Tn M A B) *)
split.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
eapply bet_half_bet.
apply H1.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
eapply bet_double_bet.
apply H.
(* Goal: False *)
apply H0.
(* Goal: @Le Tn A B C D *)
assumption.
Qed.

Lemma symmetry_preseves_bet1 : forall A B M A' B', Midpoint M A A' -> Midpoint M B B' -> Bet M A B -> Bet M A' B'.
(* Goal: forall (A B C : @Tpoint Tn) (_ : @Par Tn A B A C), @Col Tn A B C *)
intros.

eapply l7_15.
2: apply H.
(* Goal: False *)
2: apply H0.
2: apply H1.
apply l7_3_2.
Qed.

Lemma symmetry_preseves_bet2 : forall A B M A' B', Midpoint M A A' -> Midpoint M B B' -> Bet M A' B' -> Bet M A B.
(* Goal: forall (A B C : @Tpoint Tn) (_ : @Par Tn A B A C), @Col Tn A B C *)
intros.
eapply l7_15.
apply l7_3_2.
(* Goal: @Midpoint Tn M A' A *)
(* Goal: @Col Tn B' A' A *)
(* Goal: False *)
apply l7_2.
apply H.
(* Goal: @Midpoint Tn M A' A *)
(* Goal: @Col Tn B' A' A *)
(* Goal: False *)
apply l7_2.
(* Goal: False *)
apply H0.
(* Goal: @Le Tn A B C D *)
assumption.
Qed.

Lemma symmetry_preserves_bet : forall A B M A' B', Midpoint M A A' -> Midpoint M B B' -> (Bet M A' B' <-> Bet M A B).
(* Goal: forall (A B C : @Tpoint Tn) (_ : @Par Tn A B A C), @Col Tn A B C *)
intros.
(* Goal: iff (@Bet Tn M A' B') (@Bet Tn M A B) *)
split.
apply symmetry_preseves_bet2;
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
eapply (symmetry_preseves_bet1 A B);
(* Goal: @Le Tn A B C D *)
assumption.
Qed.

Lemma par_cong_mid : forall A B A' B', Par A B A' B' -> Cong A B A' B' -> exists M,  Midpoint M A A' /\ Midpoint M B B' \/ Midpoint M A B' /\ Midpoint M B A'.
(* Goal: forall (A B C : @Tpoint Tn) (_ : @Par Tn A B A C), @Col Tn A B C *)
intros.
(* Goal: @Col Tn A B C *)
induction H.

(*******Cas general**********)


assert(HH:= one_or_two_sides A A' B B').
assert(HH0:= H).
unfold Par_strict in HH0.
(* Goal: @Col Tn A B C *)
spliter.
assert(TS A A' B B' \/ OS A A' B B').
(* Goal: and (not (@eq (@Tpoint Tn) B A)) (and (@Col Tn B' B A) (@Col Tn A' B A)) *)
(* Goal: False *)
apply HH.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
(* intro.
(* Goal: @Col Tn A' B' C' *)
subst A'.
apply H4.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X A B) (@Col Tn X A C)) *)
(* Goal: @Col Tn A B C *)
exists A.
split;
(* Goal: @Col Tn A B C *)
Col. *)
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
apply H4.
exists A'.
(* Goal: @Col Tn A B C *)
split;Col.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
apply H4.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X A B) (@Col Tn X A C)) *)
(* Goal: @Col Tn A B C *)
exists A.
(* Goal: @Col Tn A B C *)
split; Col.

(* Goal: @Le Tn A B D C *)
induction H5.
clear HH.
assert(HH:= H5).
unfold TS in HH.
assert(~ Col B A A').
(* Goal: @Col Tn A B C *)
spliter.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Col Tn A B C *)
spliter.
ex_and H9 M.
exists M.
(* Goal: or (and (not (@Col Tn Q P A)) (and (@Perp Tn Q P A B) (@Col Tn Q P B))) (and (@Col Tn Q P A) (@eq (@Tpoint Tn) B A)) *)
(* Goal: or (and (not (@Col Tn Q P A)) (and (@Perp Tn Q P A B) (@Col Tn Q P B))) (and (@Col Tn Q P A) (@eq (@Tpoint Tn) B A)) *)
left.

assert(B <> B').
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
(* Goal: @Col Tn A B A' *)
(* Goal: forall _ : @Col Tn A B A', @eq (@Tpoint Tn) A' B' *)
subst B'.
apply between_identity in H10.
subst M.
apply H4.
exists B.
(* Goal: @Col Tn A B C *)
split; Col.

induction (eq_dec_points B M).
subst M.
(* Goal: False *)
contradiction.

induction (eq_dec_points B' M).
subst M.
(* Goal: @Col Tn A B C *)
(* Goal: @Col Tn A B C *)
apply False_ind.
apply H8.
(* Goal: @Col Tn A B C *)
Col.

assert(A <> A').
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
(* Goal: @Col Tn A' B' C' *)
subst A'.
(* Goal: @Col Tn A B C *)
(* Goal: @Col Tn A B C *)
apply False_ind.
apply H8.
(* Goal: @Col Tn A B C *)
Col.

assert(A <> M).
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
subst M.
apply H4.
exists B'.
(* Goal: iff (@Bet Tn M A' B') (@Bet Tn M A B) *)
split.
apply bet_col in H10.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: @Col Tn A B C *)
Col.

assert(A' <> M).
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
subst M.
apply H4.
exists B.
apply bet_col in H10.
(* Goal: iff (@Bet Tn M A' B') (@Bet Tn M A B) *)
split.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: @Col Tn A B C *)
Col.

(****************)

assert(HH:=(midpoint_existence A A')).
ex_and HH X.

prolong B X B'' B X.
assert(Midpoint X B B'').
unfold Midpoint.
(* Goal: iff (@Bet Tn M A' B') (@Bet Tn M A B) *)
split.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Cong Tn A B D P' *)
Cong.

(*

assert(~ Col B A A').
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
apply H8.

apply bet_col in H10.
assert(Col B' A M).
eapply (col_transitivity_1 _ B).
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: @Col Tn Q A B *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
ColR.
*)

assert(Par_strict B A B'' A').
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
apply (midpoint_par_strict B A B'' A' X); auto.

assert(Col B'' B' A' /\ Col A' B' A').
apply(parallel_uniqueness B A B' A' B'' A' A').

apply par_comm.
unfold Par.
(* Goal: or (and (not (@Col Tn Q P A)) (and (@Perp Tn Q P A B) (@Col Tn Q P B))) (and (@Col Tn Q P A) (@eq (@Tpoint Tn) B A)) *)
(* Goal: or (and (not (@Col Tn Q P A)) (and (@Perp Tn Q P A B) (@Col Tn Q P B))) (and (@Col Tn Q P A) (@eq (@Tpoint Tn) B A)) *)
left.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Col Tn A B C *)
Col.
unfold Par.
(* Goal: or (and (not (@Col Tn Q P A)) (and (@Perp Tn Q P A B) (@Col Tn Q P B))) (and (@Col Tn Q P A) (@eq (@Tpoint Tn) B A)) *)
(* Goal: or (and (not (@Col Tn Q P A)) (and (@Perp Tn Q P A B) (@Col Tn Q P B))) (and (@Col Tn Q P A) (@eq (@Tpoint Tn) B A)) *)
left.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: @Col Tn A B C *)
spliter.

assert(Cong A B A' B'').
eapply l7_13.
(* Goal: @Midpoint Tn M A' A *)
(* Goal: @Col Tn B' A' A *)
(* Goal: False *)
apply l7_2.
apply H17.
(* Goal: @Midpoint Tn M A' A *)
(* Goal: @Col Tn B' A' A *)
(* Goal: False *)
apply l7_2.
(* Goal: @Le Tn A B C D *)
assumption.
assert(Cong A' B' A' B'').
eapply cong_transitivity.
apply cong_symmetry.
(* Goal: False *)
apply H0.
(* Goal: @Le Tn A B C D *)
assumption.

assert(B' = B'' \/ Midpoint A' B' B'').
eapply l7_20.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: @Cong Tn A B D P' *)
Cong.
induction H26.

(***************)

subst B''.

assert(X = M).
(* Goal: @Col Tn A B C *)
eapply (l6_21 A A' B B'); Col.
subst X.
(* Goal: and (@Bet Tn D C P') (@Cong Tn D P' A B) *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
split; auto.

assert(TS A A' B B'').
unfold TS.
(* Goal: and (@Bet Tn D C P') (@Cong Tn D P' A B) *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
repeat split; auto.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
apply H8.
apply col_permutation_1.
eapply (col_transitivity_1 _ B'').
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
subst B''.
apply l7_2 in H26.
apply is_midpoint_id in H26.
(* Goal: False *)
contradiction.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: @Col Tn A B C *)
Col.
exists X.
(* Goal: iff (@Bet Tn M A' B') (@Bet Tn M A B) *)
split.

unfold Midpoint in H17.
(* Goal: @Col Tn A B C *)
spliter.
apply bet_col in H17.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: @Le Tn A B C D *)
assumption.

assert(OS A A' B' B'').
eapply l9_8_1.
apply l9_2.
apply H5.
apply l9_2.
(* Goal: @Le Tn A B C D *)
assumption.

assert(TS A A' B' B'').
unfold TS.
(* Goal: iff (@Bet Tn M A' B') (@Bet Tn M A B) *)
repeat split.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
apply H8.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
apply H8.

apply col_permutation_1.
eapply (col_transitivity_1 _ B'').
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
subst B''.
apply l7_2 in H26.
apply is_midpoint_id in H26.
(* Goal: False *)
contradiction.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: @Col Tn A B C *)
Col.

exists A'.
(* Goal: iff (@Bet Tn M A' B') (@Bet Tn M A B) *)
split.
(* Goal: @Col Tn A B C *)
Col.
unfold Midpoint in H26.
(* Goal: @Col Tn A B C *)
spliter.
(* Goal: @Le Tn A B C D *)
assumption.
apply l9_9 in H29.
(* Goal: False *)
contradiction.

clear HH H3.


(****************)

assert(HH:=(midpoint_existence A' B)).
ex_and HH X.
exists X.
(* Goal: or (and (not (@Col Tn Q P A)) (and (@Perp Tn Q P A A) (@Col Tn Q P A))) (and (@Col Tn Q P A) (@eq (@Tpoint Tn) A A)) *)
right.

prolong A X B'' A X.
assert(Midpoint X A B'').
unfold Midpoint.
(* Goal: iff (@Bet Tn M A' B') (@Bet Tn M A B) *)
split.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Cong Tn A B D P' *)
Cong.

assert(~Col A B A').
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
apply H4.
exists A'.
(* Goal: @Col Tn A B C *)
split; Col.

(*


assert(HH:= H5).
unfold OS in HH.
ex_and HH T.


assert(~Col A A' B).
unfold TS in H9.
(* Goal: @Col Tn A B C *)
spliter.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
apply H11.
(* Goal: @Col Tn A B C *)
Col.

assert(~Col A A' B').
unfold TS in H10.
(* Goal: @Col Tn A B C *)
spliter.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
apply H12.
(* Goal: @Col Tn A B C *)
Col.


assert(~Col B A B').
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
apply H4.
exists B'.
split;
(* Goal: @Col Tn A B C *)
Col.
*)

assert(Par_strict  A B B'' A').
apply (midpoint_par_strict A B  B'' A' X).
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Midpoint Tn M A' A *)
(* Goal: @Col Tn B' A' A *)
(* Goal: False *)
apply l7_2.
(* Goal: @Le Tn A B C D *)
assumption.

assert(Col B'' B' A' /\ Col A' B' A').
apply (parallel_uniqueness B A B' A' B'' A' A').

(*
assert (Col A' A' B' /\ Col B'' A' B').
(* Goal: @Col Tn A B C *)
Col.
*)
apply par_comm.
unfold Par.
(* Goal: or (and (not (@Col Tn Q P A)) (and (@Perp Tn Q P A B) (@Col Tn Q P B))) (and (@Col Tn Q P A) (@eq (@Tpoint Tn) B A)) *)
(* Goal: or (and (not (@Col Tn Q P A)) (and (@Perp Tn Q P A B) (@Col Tn Q P B))) (and (@Col Tn Q P A) (@eq (@Tpoint Tn) B A)) *)
left.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Col Tn A B C *)
Col.
apply par_left_comm.
unfold Par.
(* Goal: or (and (not (@Col Tn Q P A)) (and (@Perp Tn Q P A B) (@Col Tn Q P B))) (and (@Col Tn Q P A) (@eq (@Tpoint Tn) B A)) *)
(* Goal: or (and (not (@Col Tn Q P A)) (and (@Perp Tn Q P A B) (@Col Tn Q P B))) (and (@Col Tn Q P A) (@eq (@Tpoint Tn) B A)) *)
left.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: @Col Tn A B C *)
spliter.

assert(Cong A B  B'' A').
eapply l7_13.
(* Goal: @Midpoint Tn M A' A *)
(* Goal: @Col Tn B' A' A *)
(* Goal: False *)
apply l7_2.
apply H8.
(* Goal: @Le Tn A B C D *)
assumption.
assert(Cong A' B' A' B'').
eapply cong_transitivity.
apply cong_symmetry.
(* Goal: False *)
apply H0.
(* Goal: @Cong Tn A B D P' *)
Cong.
assert(B' = B'' \/ Midpoint A' B' B'').
eapply l7_20.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: @Cong Tn A B D P' *)
Cong.

induction H15.
subst B''.
(* Goal: iff (@Bet Tn M A' B') (@Bet Tn M A B) *)
split.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Midpoint Tn M A' A *)
(* Goal: @Col Tn B' A' A *)
(* Goal: False *)
apply l7_2.
(* Goal: @Le Tn A B C D *)
assumption.

assert(OS A A' X B'').

eapply (out_one_side_1 _ _ X B'').
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
apply H9.
apply col_permutation_1.
eapply (col_transitivity_1 _ X).
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
subst X.
apply is_midpoint_id in H3.
(* Goal: @Col Tn A' B' C' *)
subst A'.
apply H4.
exists B.
(* Goal: @Col Tn A B C *)
split; Col.
(* Goal: @Col Tn A B C *)
Col.
unfold Midpoint in H3.
(* Goal: @Col Tn A B C *)
spliter.
apply bet_col in H3.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: @Col Tn A B C *)
Col.
unfold Out.
(* Goal: iff (@Bet Tn M A' B') (@Bet Tn M A B) *)
repeat split.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
subst X.
apply cong_identity in H7.
subst B''.
unfold Par_strict in H10.
(* Goal: @Col Tn A B C *)
spliter.
apply H17.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X A B) (@Col Tn X A C)) *)
(* Goal: @Col Tn A B C *)
exists A.
(* Goal: @Col Tn A B C *)
split; Col.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
subst B''.
unfold Par_strict in H10.
(* Goal: @Col Tn A B C *)
spliter.
apply H18.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X A B) (@Col Tn X A C)) *)
(* Goal: @Col Tn A B C *)
exists A.
(* Goal: @Col Tn A B C *)
split; Col.
unfold Midpoint in H8.
(* Goal: @Col Tn A B C *)
spliter.
(* Goal: or (and (not (@Col Tn Q P A)) (and (@Perp Tn Q P A B) (@Col Tn Q P B))) (and (@Col Tn Q P A) (@eq (@Tpoint Tn) B A)) *)
(* Goal: or (and (not (@Col Tn Q P A)) (and (@Perp Tn Q P A B) (@Col Tn Q P B))) (and (@Col Tn Q P A) (@eq (@Tpoint Tn) B A)) *)
left.
(* Goal: @Le Tn A B C D *)
assumption.

assert(TS A A' B' B'').
unfold TS.
(* Goal: iff (@Bet Tn M A' B') (@Bet Tn M A B) *)
repeat split.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
apply H4.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X A B) (@Col Tn X A C)) *)
(* Goal: @Col Tn A B C *)
exists A.
(* Goal: @Col Tn A B C *)
split; Col.

unfold OS in H16.
ex_and H16 T.
unfold TS in H17.
(* Goal: @Col Tn A B C *)
spliter.
(* Goal: @Le Tn A B C D *)
assumption.
exists A'.
(* Goal: iff (@Bet Tn M A' B') (@Bet Tn M A B) *)
split.
(* Goal: @Col Tn A B C *)
Col.
unfold Midpoint in H15.
(* Goal: @Col Tn A B C *)
spliter.
(* Goal: @Le Tn A B C D *)
assumption.

assert(TS A A' X B').
eapply l9_8_2.
apply l9_2.
apply H17.
apply one_side_symmetry.
(* Goal: @Le Tn A B C D *)
assumption.

assert(OS A A' X B).

eapply (out_one_side_1).
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
apply H9.
apply col_permutation_1.
eapply (col_transitivity_1 _ X).
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
subst X.
apply is_midpoint_id in H3.
(* Goal: @Col Tn A' B' C' *)
subst A'.
apply H4.
exists B.
(* Goal: @Col Tn A B C *)
split; Col.
(* Goal: @Col Tn A B C *)
Col.
unfold Midpoint in H3.
(* Goal: @Col Tn A B C *)
spliter.
apply bet_col in H3.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: @Le Tn A B C D *)
apply col_trivial_2;assumption.
unfold Out.
(* Goal: iff (@Bet Tn M A' B') (@Bet Tn M A B) *)
repeat split.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
subst X.
unfold TS in H18.
(* Goal: @Col Tn A B C *)
spliter.
apply H18.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
(* Goal: @Col Tn A' B' C' *)
subst A'.
unfold Par_strict in H10.
(* Goal: @Col Tn A B C *)
spliter.
apply H21.
exists B.
(* Goal: @Col Tn A B C *)
split; Col.
unfold Midpoint in H3.
(* Goal: @Col Tn A B C *)
spliter.
(* Goal: or (and (not (@Col Tn Q P A)) (and (@Perp Tn Q P A B) (@Col Tn Q P B))) (and (@Col Tn Q P A) (@eq (@Tpoint Tn) B A)) *)
(* Goal: or (and (not (@Col Tn Q P A)) (and (@Perp Tn Q P A B) (@Col Tn Q P B))) (and (@Col Tn Q P A) (@eq (@Tpoint Tn) B A)) *)
left.
(* Goal: @Le Tn A B C D *)
assumption.

assert(OS A A' X B').
eapply one_side_transitivity.
apply H19.
(* Goal: @Le Tn A B C D *)
assumption.
apply l9_9 in H18.
(* Goal: False *)
contradiction.

(* Goal: @Col Tn A B C *)
spliter.

induction (eq_dec_points A A').
(* Goal: @Col Tn A' B' C' *)
subst A'.
assert(B = B' \/ Midpoint A B B').
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
eapply l7_20; auto.
induction H4.
(* Goal: @Col Tn A B A' *)
(* Goal: forall _ : @Col Tn A B A', @eq (@Tpoint Tn) A' B' *)
subst B'.
assert( HH:= midpoint_existence A B).
ex_and HH M.
exists M.
(* Goal: or (and (not (@Col Tn Q P A)) (and (@Perp Tn Q P A A) (@Col Tn Q P A))) (and (@Col Tn Q P A) (@eq (@Tpoint Tn) A A)) *)
right.
(* Goal: iff (@Bet Tn M A' B') (@Bet Tn M A B) *)
split.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Midpoint Tn M A' A *)
(* Goal: @Col Tn B' A' A *)
(* Goal: False *)
apply l7_2.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X A B) (@Col Tn X A C)) *)
(* Goal: @Col Tn A B C *)
exists A.
(* Goal: or (and (not (@Col Tn Q P A)) (and (@Perp Tn Q P A B) (@Col Tn Q P B))) (and (@Col Tn Q P A) (@eq (@Tpoint Tn) B A)) *)
(* Goal: or (and (not (@Col Tn Q P A)) (and (@Perp Tn Q P A B) (@Col Tn Q P B))) (and (@Col Tn Q P A) (@eq (@Tpoint Tn) B A)) *)
left.
(* Goal: iff (@Bet Tn M A' B') (@Bet Tn M A B) *)
split.
apply l7_3_2.
(* Goal: @Le Tn A B C D *)
assumption.

induction (eq_dec_points B B').
(* Goal: @Col Tn A B A' *)
(* Goal: forall _ : @Col Tn A B A', @eq (@Tpoint Tn) A' B' *)
subst B'.
assert(A = A' \/ Midpoint B A A').
eapply l7_20.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: @Cong Tn A B D P' *)
Cong.
(* Goal: @Le Tn A B D C *)
induction H5.
(* Goal: @Col Tn A' B' C' *)
subst A'.
assert( HH:= midpoint_existence A B).
ex_and HH M.
exists M.
(* Goal: or (and (not (@Col Tn Q P A)) (and (@Perp Tn Q P A A) (@Col Tn Q P A))) (and (@Col Tn Q P A) (@eq (@Tpoint Tn) A A)) *)
right.
(* Goal: iff (@Bet Tn M A' B') (@Bet Tn M A B) *)
split.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Midpoint Tn M A' A *)
(* Goal: @Col Tn B' A' A *)
(* Goal: False *)
apply l7_2.
(* Goal: @Le Tn A B C D *)
assumption.
exists B.
(* Goal: or (and (not (@Col Tn Q P A)) (and (@Perp Tn Q P A B) (@Col Tn Q P B))) (and (@Col Tn Q P A) (@eq (@Tpoint Tn) B A)) *)
(* Goal: or (and (not (@Col Tn Q P A)) (and (@Perp Tn Q P A B) (@Col Tn Q P B))) (and (@Col Tn Q P A) (@eq (@Tpoint Tn) B A)) *)
left.
(* Goal: iff (@Bet Tn M A' B') (@Bet Tn M A B) *)
split.
(* Goal: @Le Tn A B C D *)
assumption.
apply l7_3_2.

induction (eq_dec_points A B').
(* Goal: @Col Tn A B A' *)
(* Goal: forall _ : @Col Tn A B A', @eq (@Tpoint Tn) A' B' *)
subst B'.
assert(B = A' \/ Midpoint A B A').
eapply l7_20.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: @Cong Tn A B D P' *)
Cong.
induction H6.
(* Goal: @Col Tn A' B' C' *)
subst A'.
assert( HH:= midpoint_existence A B).
ex_and HH M.
exists M.
(* Goal: or (and (not (@Col Tn Q P A)) (and (@Perp Tn Q P A B) (@Col Tn Q P B))) (and (@Col Tn Q P A) (@eq (@Tpoint Tn) B A)) *)
(* Goal: or (and (not (@Col Tn Q P A)) (and (@Perp Tn Q P A B) (@Col Tn Q P B))) (and (@Col Tn Q P A) (@eq (@Tpoint Tn) B A)) *)
left.
(* Goal: iff (@Bet Tn M A' B') (@Bet Tn M A B) *)
split.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Midpoint Tn M A' A *)
(* Goal: @Col Tn B' A' A *)
(* Goal: False *)
apply l7_2.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X A B) (@Col Tn X A C)) *)
(* Goal: @Col Tn A B C *)
exists A.
(* Goal: or (and (not (@Col Tn Q P A)) (and (@Perp Tn Q P A A) (@Col Tn Q P A))) (and (@Col Tn Q P A) (@eq (@Tpoint Tn) A A)) *)
right.
(* Goal: iff (@Bet Tn M A' B') (@Bet Tn M A B) *)
split.
apply l7_3_2.
(* Goal: @Le Tn A B C D *)
assumption.

induction (eq_dec_points A' B).
(* Goal: @Col Tn A' B' C' *)
subst A'.
assert(A = B' \/ Midpoint B A B').
eapply l7_20.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: @Cong Tn A B D P' *)
Cong.
induction H7.
(* Goal: @Col Tn A B A' *)
(* Goal: forall _ : @Col Tn A B A', @eq (@Tpoint Tn) A' B' *)
subst B'.
assert( HH:= midpoint_existence A B).
ex_and HH M.
exists M.
(* Goal: or (and (not (@Col Tn Q P A)) (and (@Perp Tn Q P A B) (@Col Tn Q P B))) (and (@Col Tn Q P A) (@eq (@Tpoint Tn) B A)) *)
(* Goal: or (and (not (@Col Tn Q P A)) (and (@Perp Tn Q P A B) (@Col Tn Q P B))) (and (@Col Tn Q P A) (@eq (@Tpoint Tn) B A)) *)
left.
(* Goal: iff (@Bet Tn M A' B') (@Bet Tn M A B) *)
split.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Midpoint Tn M A' A *)
(* Goal: @Col Tn B' A' A *)
(* Goal: False *)
apply l7_2.
(* Goal: @Le Tn A B C D *)
assumption.
exists B.
(* Goal: or (and (not (@Col Tn Q P A)) (and (@Perp Tn Q P A A) (@Col Tn Q P A))) (and (@Col Tn Q P A) (@eq (@Tpoint Tn) A A)) *)
right.
(* Goal: iff (@Bet Tn M A' B') (@Bet Tn M A B) *)
split.
(* Goal: @Le Tn A B C D *)
assumption.
apply l7_3_2.

assert(Col A B A').
(* Goal: @Col Tn Q A B *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
ColR.
assert(Col A B B').
(* Goal: @Col Tn Q A B *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
ColR.

induction H9.
(* Goal: @Par_strict Tn A B A' B' *)
induction H3.

assert( HH:= midpoint_existence A' B).
ex_and HH M.
exists M.
(* Goal: or (and (not (@Col Tn Q P A)) (and (@Perp Tn Q P A A) (@Col Tn Q P A))) (and (@Col Tn Q P A) (@eq (@Tpoint Tn) A A)) *)
right.
(* Goal: iff (@Bet Tn M A' B') (@Bet Tn M A B) *)
split.

assert(Bet B M B').

eapply between_exchange4.
2: apply H3.
unfold Midpoint in H10.
(* Goal: @Col Tn A B C *)
spliter.
Between.

assert(Bet A M B').
eapply between_exchange2.
apply H9.
(* Goal: @Le Tn A B C D *)
assumption.
assert(Cong A M B' M).
eapply (l2_11 A  B _  _ A').
eapply between_inner_transitivity.
apply H9.
(* Goal: @Le Tn A B C D *)
assumption.
eapply between_inner_transitivity.
apply between_symmetry.
apply H3.
unfold Midpoint in H10.
(* Goal: @Col Tn A B C *)
spliter.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Cong Tn A B D P' *)
Cong.
unfold Midpoint in H10.
(* Goal: @Col Tn A B C *)
spliter.
apply cong_left_commutativity.
(* Goal: @Cong Tn A B D P' *)
Cong.
unfold Midpoint.
(* Goal: iff (@Bet Tn M A' B') (@Bet Tn M A B) *)
split.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Cong Tn A B D P' *)
Cong.
(* Goal: @Midpoint Tn M A' A *)
(* Goal: @Col Tn B' A' A *)
(* Goal: False *)
apply l7_2.
(* Goal: @Le Tn A B C D *)
assumption.

(* Goal: @Par_strict Tn A B A' B' *)
induction H3.

assert( HH:= midpoint_existence B B').
ex_and HH M.
exists M.
(* Goal: or (and (not (@Col Tn Q P A)) (and (@Perp Tn Q P A B) (@Col Tn Q P B))) (and (@Col Tn Q P A) (@eq (@Tpoint Tn) B A)) *)
(* Goal: or (and (not (@Col Tn Q P A)) (and (@Perp Tn Q P A B) (@Col Tn Q P B))) (and (@Col Tn Q P A) (@eq (@Tpoint Tn) B A)) *)
left.
(* Goal: iff (@Bet Tn M A' B') (@Bet Tn M A B) *)
split.

assert(Bet A' M B).
eapply between_exchange2.
apply H3.
unfold Midpoint in H10.
(* Goal: @Col Tn A B C *)
spliter.
Between.
assert(Bet M B A).
eapply between_exchange3.
unfold Midpoint in H10.
(* Goal: @Col Tn A B C *)
spliter.
apply between_symmetry.
apply H10.
Between.
assert(Bet A' M A).
eapply outer_transitivity_between.
apply H11.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
subst M.
apply is_midpoint_id in H10.
(* Goal: False *)
contradiction.
assert(Cong A M A' M).
eapply l2_11.
apply between_symmetry.
apply H12.
eapply between_inner_transitivity.
apply H3.

unfold Midpoint in H10.
(* Goal: @Col Tn A B C *)
spliter.
Between.
(* Goal: @Le Tn A B C D *)
assumption.
unfold Midpoint in H10.
(* Goal: @Col Tn A B C *)
spliter.
(* Goal: @Cong Tn A B D P' *)
Cong.
unfold Midpoint.
(* Goal: iff (@Bet Tn M A' B') (@Bet Tn M A B) *)
split.
Between.
(* Goal: @Cong Tn A B D P' *)
Cong.
(* Goal: @Le Tn A B C D *)
assumption.

assert(Bet B A' A).
eapply (bet_cong_bet B').
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
Between.
Between.
(* Goal: @Cong Tn A B D P' *)
Cong.

assert( HH:= midpoint_existence A' B).
ex_and HH M.
exists M.
(* Goal: or (and (not (@Col Tn Q P A)) (and (@Perp Tn Q P A A) (@Col Tn Q P A))) (and (@Col Tn Q P A) (@eq (@Tpoint Tn) A A)) *)
right.
(* Goal: iff (@Bet Tn M A' B') (@Bet Tn M A B) *)
split.
assert(Bet B M A).
eapply between_exchange4.
unfold Midpoint in H11.
(* Goal: @Col Tn A B C *)
spliter.
apply between_symmetry.
apply H11.
(* Goal: @Le Tn A B C D *)
assumption.

assert(Bet B' B M).
eapply between_inner_transitivity.
apply between_symmetry.
apply H9.
(* Goal: @Le Tn A B C D *)
assumption.

assert(Bet M A' A).
eapply between_exchange3.
2:apply H10.
unfold Midpoint in H11.
(* Goal: @Col Tn A B C *)
spliter.
Between.
assert(Bet B' M A').
eapply outer_transitivity_between2.
apply H13.
unfold Midpoint in H11.
(* Goal: @Col Tn A B C *)
spliter.
Between.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
subst M.
apply l7_2 in H11.
apply is_midpoint_id in H11.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
assert(Bet B' M A).
eapply outer_transitivity_between.
apply H15.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
(* Goal: @Col Tn A' B' C' *)
subst A'.
apply is_midpoint_id in H11.
subst M.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
tauto.

assert(Cong A M B' M).
eapply l4_3.
apply between_symmetry.
apply H12.
apply H15.
(* Goal: @Cong Tn A B D P' *)
Cong.
unfold Midpoint in H11.
(* Goal: @Col Tn A B C *)
spliter.
(* Goal: @Cong Tn A B D P' *)
Cong.
unfold Midpoint.
(* Goal: iff (@Bet Tn M A' B') (@Bet Tn M A B) *)
split.
Between.
(* Goal: @Cong Tn A B D P' *)
Cong.
Midpoint.

induction H9.
induction H2.


assert(B' = B /\ A = A').
eapply bet_cong_eq.
(* Goal: @Le Tn A B C D *)
assumption.
Between.
(* Goal: @Cong Tn A B D P' *)
Cong.
(* Goal: @Col Tn A B C *)
spliter.
(* Goal: False *)
contradiction.
induction H2.

assert(Bet B' B A').
eapply bet_cong_bet.
apply H6.
Between.
Between.
(* Goal: @Cong Tn A B D P' *)
Cong.

assert( HH:= midpoint_existence B B').
ex_and HH M.
exists M.
(* Goal: or (and (not (@Col Tn Q P A)) (and (@Perp Tn Q P A B) (@Col Tn Q P B))) (and (@Col Tn Q P A) (@eq (@Tpoint Tn) B A)) *)
(* Goal: or (and (not (@Col Tn Q P A)) (and (@Perp Tn Q P A B) (@Col Tn Q P B))) (and (@Col Tn Q P A) (@eq (@Tpoint Tn) B A)) *)
left.
(* Goal: iff (@Bet Tn M A' B') (@Bet Tn M A B) *)
split.

assert(Bet A' M B').
eapply between_exchange2.
apply between_symmetry.
apply H10.
unfold Midpoint in H11.
(* Goal: @Col Tn A B C *)
spliter.
(* Goal: @Le Tn A B C D *)
assumption.

assert(Bet M B' A).
eapply between_exchange3.
unfold Midpoint in H11.
(* Goal: @Col Tn A B C *)
spliter.
apply H11.
(* Goal: @Le Tn A B C D *)
assumption.
assert(Bet A' M A).
eapply outer_transitivity_between.
apply H12.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
subst M.
apply l7_2 in H11.
apply is_midpoint_id in H11.
apply sym_equal in H11.
(* Goal: False *)
contradiction.

assert(Bet A M B).
eapply outer_transitivity_between2.
apply between_symmetry.
apply H13.
unfold Midpoint in H11.
(* Goal: @Col Tn A B C *)
spliter.
Between.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
subst M.
apply l7_2 in H11.
apply is_midpoint_id in H11.
apply sym_equal in H11.
(* Goal: False *)
contradiction.

assert(Cong A' M A M).
eapply l4_3.
apply H12.
apply H15.
(* Goal: @Cong Tn A B D P' *)
Cong.
unfold Midpoint in H11.
(* Goal: @Col Tn A B C *)
spliter.
(* Goal: @Cong Tn A B D P' *)
Cong.
unfold Midpoint.
(* Goal: iff (@Bet Tn M A' B') (@Bet Tn M A B) *)
split.
Between.
(* Goal: @Cong Tn A B D P' *)
Cong.
(* Goal: @Le Tn A B C D *)
assumption.

assert( HH:= midpoint_existence A B').
ex_and HH M.
exists M.
(* Goal: or (and (not (@Col Tn Q P A)) (and (@Perp Tn Q P A A) (@Col Tn Q P A))) (and (@Col Tn Q P A) (@eq (@Tpoint Tn) A A)) *)
right.
(* Goal: iff (@Bet Tn M A' B') (@Bet Tn M A B) *)
split.
(* Goal: @Le Tn A B C D *)
assumption.

assert(Bet A' A M).
eapply between_inner_transitivity.
apply between_symmetry.
(* Goal: False *)
(* Goal: @Col Tn A B C *)
apply H2.
unfold Midpoint in H10.
(* Goal: @Col Tn A B C *)
spliter.
(* Goal: @Le Tn A B C D *)
assumption.

assert(Bet A M B).
eapply between_exchange4.
unfold Midpoint in H10.
(* Goal: @Col Tn A B C *)
spliter.
apply H10.
Between.

assert(Bet A' M B).
eapply outer_transitivity_between2.
apply H11.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
subst M.
apply is_midpoint_id in H10.
(* Goal: False *)
contradiction.

assert(Cong B M A' M).
eapply l4_3.
apply between_symmetry.
apply H12.
eapply between_exchange2.
apply between_symmetry.
(* Goal: False *)
(* Goal: @Col Tn A B C *)
apply H2.
unfold Midpoint in H10.
(* Goal: @Col Tn A B C *)
spliter.

(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Cong Tn A B D P' *)
Cong.
unfold Midpoint in H10.
(* Goal: @Col Tn A B C *)
spliter.
(* Goal: @Cong Tn A B D P' *)
Cong.
unfold Midpoint.
(* Goal: iff (@Bet Tn M A' B') (@Bet Tn M A B) *)
split.
Between.
(* Goal: @Cong Tn A B D P' *)
Cong.

induction H8.

assert(Bet B' B A').
eapply outer_transitivity_between2.
apply H9.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Le Tn A B C D *)
assumption.

assert(B = A' /\ B' = A).
eapply bet_cong_eq.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Cong Tn A B D P' *)
Cong.
(* Goal: @Col Tn A B C *)
spliter.
(* Goal: @Col Tn A' B' C' *)
subst A'.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
tauto.

induction H8.

assert( HH:= midpoint_existence A A').
ex_and HH M.
exists M.
(* Goal: or (and (not (@Col Tn Q P A)) (and (@Perp Tn Q P A B) (@Col Tn Q P B))) (and (@Col Tn Q P A) (@eq (@Tpoint Tn) B A)) *)
(* Goal: or (and (not (@Col Tn Q P A)) (and (@Perp Tn Q P A B) (@Col Tn Q P B))) (and (@Col Tn Q P A) (@eq (@Tpoint Tn) B A)) *)
left.
(* Goal: iff (@Bet Tn M A' B') (@Bet Tn M A B) *)
split.
(* Goal: @Le Tn A B C D *)
assumption.

assert(Bet B A' M).
eapply between_inner_transitivity.
apply H8.
unfold Midpoint in H10.
(* Goal: @Col Tn A B C *)
spliter.
Between.

assert(Bet B M A).
eapply outer_transitivity_between2.
apply H11.
unfold Midpoint in H10.
(* Goal: @Col Tn A B C *)
spliter.
Between.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
subst M.
apply l7_2 in H10.
apply is_midpoint_id in H10.
(* Goal: @Col Tn A' B' C' *)
subst A'.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
tauto.

assert(Bet B M B').
eapply between_exchange4.
apply H12.
Between.

assert(Cong B M B' M).
eapply l4_3.
apply H12.

assert(Bet B' A A').
eapply between_inner_transitivity.
apply H9.
Between.
eapply between_exchange2.
apply H14.
unfold Midpoint in H10.
(* Goal: @Col Tn A B C *)
spliter.
Between.
(* Goal: @Cong Tn A B D P' *)
Cong.
unfold Midpoint in H10.
(* Goal: @Col Tn A B C *)
spliter.
(* Goal: @Cong Tn A B D P' *)
Cong.
unfold Midpoint.
(* Goal: iff (@Bet Tn M A' B') (@Bet Tn M A B) *)
split.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Cong Tn A B D P' *)
Cong.

assert(Bet A B' A' \/ Bet A A' B').
eapply (l5_2 B).
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
Between.
Between.
induction H10.

assert( HH:= midpoint_existence A B').
ex_and HH M.
exists M.
(* Goal: or (and (not (@Col Tn Q P A)) (and (@Perp Tn Q P A A) (@Col Tn Q P A))) (and (@Col Tn Q P A) (@eq (@Tpoint Tn) A A)) *)
right.
(* Goal: iff (@Bet Tn M A' B') (@Bet Tn M A B) *)
split.
(* Goal: @Le Tn A B C D *)
assumption.

assert(Bet B M B').
eapply between_exchange2.
apply between_symmetry.
apply H9.
unfold Midpoint in H11.
(* Goal: @Col Tn A B C *)
spliter.
Between.
assert(Bet A' B' M).
eapply between_inner_transitivity.
apply between_symmetry.
apply H10.
unfold Midpoint in H11.
(* Goal: @Col Tn A B C *)
spliter.
Between.

assert(Bet A' M B).
eapply outer_transitivity_between2.
apply H13.
Between.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
subst M.
apply l7_2 in H11.
apply is_midpoint_id in H11.
(* Goal: @Col Tn A B A' *)
(* Goal: forall _ : @Col Tn A B A', @eq (@Tpoint Tn) A' B' *)
subst B'.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
tauto.

assert(Cong M A' M B).
eapply l2_11.
apply between_symmetry.
apply H13.
eapply between_exchange3.
unfold Midpoint in H11.
(* Goal: @Col Tn A B C *)
spliter.
apply between_symmetry.
apply H11.
(* Goal: @Le Tn A B C D *)
assumption.
unfold Midpoint in H11.
(* Goal: @Col Tn A B C *)
spliter.
Between.
(* Goal: @Cong Tn A B D P' *)
Cong.
(* Goal: @Cong Tn A B D P' *)
Cong.
unfold Midpoint.
(* Goal: iff (@Bet Tn M A' B') (@Bet Tn M A B) *)
split.
Between.
(* Goal: @Cong Tn A B D P' *)
Cong.

assert( HH:= midpoint_existence A A').
ex_and HH M.
exists M.
(* Goal: or (and (not (@Col Tn Q P A)) (and (@Perp Tn Q P A B) (@Col Tn Q P B))) (and (@Col Tn Q P A) (@eq (@Tpoint Tn) B A)) *)
(* Goal: or (and (not (@Col Tn Q P A)) (and (@Perp Tn Q P A B) (@Col Tn Q P B))) (and (@Col Tn Q P A) (@eq (@Tpoint Tn) B A)) *)
left.
(* Goal: iff (@Bet Tn M A' B') (@Bet Tn M A B) *)
split.
(* Goal: @Le Tn A B C D *)
assumption.

assert(Bet B A M).
eapply between_inner_transitivity.
apply between_symmetry.
apply H8.
unfold Midpoint in H11.
(* Goal: @Col Tn A B C *)
spliter.
Between.
assert(Bet B' M A).
eapply between_exchange2.
apply between_symmetry.
apply H10.
unfold Midpoint in H11.
(* Goal: @Col Tn A B C *)
spliter.
Between.
assert(Bet B' M B).
eapply outer_transitivity_between.
apply H13.
Between.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
subst M.
apply is_midpoint_id in H11.
(* Goal: False *)
contradiction.
assert(Cong B' M B M).
eapply l2_11.
eapply between_inner_transitivity.
apply between_symmetry.
apply H10.
unfold Midpoint in H11.
(* Goal: @Col Tn A B C *)
spliter.
Between.
apply H12.
(* Goal: @Cong Tn A B D P' *)
Cong.
unfold Midpoint in H11.
(* Goal: @Col Tn A B C *)
spliter.
Between.
(* Goal: @Cong Tn A B D P' *)
Cong.
unfold Midpoint.
(* Goal: iff (@Bet Tn M A' B') (@Bet Tn M A B) *)
split.
Between.
(* Goal: @Cong Tn A B D P' *)
Cong.
Qed.

Lemma per_preserves_bet_aux1 : forall P Q A B C B' C', P <> Q -> Bet A B C ->
                                      Col P Q A ->
                                      Per B B' P -> Col P Q B' ->
                                      Per C C' P -> Col P Q C' ->
                                      P <> A -> P <> B' -> P <> C' ->
                                      Bet A B' C'.
(* Goal: forall (A B C : @Tpoint Tn) (_ : @Par Tn A B A C), @Col Tn A B C *)
intros.

induction(eq_dec_points B B').
(* Goal: @Col Tn A B A' *)
(* Goal: forall _ : @Col Tn A B A', @eq (@Tpoint Tn) A' B' *)
subst B'.

(* Goal: @eq (@Tpoint Tn) C C' *)
assert(Col A B C').
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
apply (col3 P Q); try auto.

(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
assert(Col P A B).
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
eapply (col_transitivity_1 _ Q); try auto.

(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
assert(Col Q A B).
eapply (col_transitivity_1 _ P).
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: @Col Tn A B C *)
Col.

(* Goal: @Le Tn A B D C *)
induction(eq_dec_points A B).
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
subst B.
apply between_trivial2.

(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
assert(Col P Q C).
eapply col3.
apply H12.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: @Col Tn A B C *)
Col.
apply bet_col.
(* Goal: @Le Tn A B C D *)
assumption.

assert(Col P C' C).
eapply col_transitivity_1.
apply H.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Le Tn A B C D *)
assumption.

assert(P=C' \/ C=C').
eapply l8_9.
(* Goal: @Per Tn C1 C1 A1 *)
apply l8_2.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Le Tn A B C D *)
assumption.

induction H15.
(* Goal: @Col Tn A B C' *)
subst C'.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
tauto.
(* Goal: @Col Tn A B C' *)
subst C'.
(* Goal: @Le Tn A B C D *)
assumption.

(* A=A' et B<>B' *)

induction(eq_dec_points A C).
(* Goal: False *)
subst C.
apply between_identity in H0.
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
subst B.
assert(B'=C').
eapply per_id.
(* Goal: False *)
(* Goal: @Col Tn A B C *)
4:apply H2.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
eapply (col_transitivity_1 _ Q); auto.
(* Goal: @Col Tn A B C' *)
subst C'.
(* Goal: @Bet Tn D C C *)
(* Goal: @Cong Tn A B D C *)
(* Goal: @Le Tn A B D C *)
apply between_trivial.

assert(C <> C').
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
(* Goal: @Col Tn A B C' *)
subst C'.

assert(Col P A C).
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
eapply (col_transitivity_1 _ Q); try auto.

assert(Col A C B').
eapply col3.
apply H.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Le Tn A B C D *)
assumption.

assert(Col P B' B).
eapply col3.
3:apply H12.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Col Tn A B C *)
Col.
apply col_permutation_5.
apply bet_col.
(* Goal: @Le Tn A B C D *)
assumption.
assert(B=B' \/ P=B').
eapply l8_9.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Col Tn A B C *)
Col.
induction H14.
(* Goal: @Col Tn A B A' *)
(* Goal: forall _ : @Col Tn A B A', @eq (@Tpoint Tn) A' B' *)
subst B'.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
tauto.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.

induction (eq_dec_points A B').
(* Goal: @Col Tn A B A' *)
(* Goal: forall _ : @Col Tn A B A', @eq (@Tpoint Tn) A' B' *)
subst B'.
apply between_trivial2.

assert(A <> B).
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
subst B.
apply per_not_col in H2.
(* Goal: False *)
(* Goal: @Col Tn A B C *)
apply H2.
(* Goal: @Col Tn Q A B *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
ColR.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.

induction(col_dec C B B').
assert(C=B).

eapply (l6_21 B B').
assert(Per B B' A).
eapply (per_col _ _ P).
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Col Tn Q A B *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
ColR.
apply per_not_col in H15.
apply H15.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
apply H13.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: @Col Tn A B C *)
Col.
apply bet_col.
(* Goal: False *)
apply H0.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: False *)
subst C.

assert(B'=C').
eapply per_id.
(* Goal: False *)
(* Goal: @Col Tn A B C *)
4:apply H2.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Col Tn Q A B *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
ColR.
(* Goal: @Col Tn A B C' *)
subst C'.
(* Goal: @Bet Tn D C C *)
(* Goal: @Cong Tn A B D C *)
(* Goal: @Le Tn A B D C *)
apply between_trivial.


assert(Perp B' B' B' P \/ Perp B B' B' P).
eapply perp_in_perp_bis.

apply per_perp_in.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Le Tn A B C D *)
assumption.
induction H15.
apply perp_not_eq_1 in H15.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
tauto.

assert(Perp C' C' C' P \/ Perp C C' C' P).
eapply perp_in_perp_bis.

apply per_perp_in.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Le Tn A B C D *)
assumption.
induction H16.
apply perp_not_eq_1 in H16.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
tauto.

assert(Par B B' C C').
eapply l12_9_2D.
apply H15.
(* Goal: @Perp Tn C1 P1 A1 C1 *)
(* Goal: @Per Tn P1 C1 A1 *)
apply perp_sym.
apply perp_left_comm.
eapply perp_col.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
apply perp_left_comm.
(* Goal: @Perp Tn C1 P1 A1 C1 *)
(* Goal: @Per Tn P1 C1 A1 *)
apply perp_sym.
apply H16.
eapply (col_transitivity_1 _ Q);
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
unfold Par in H17.

assert(Par_strict B B' C C').
induction H17.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Col Tn A B C *)
spliter.
(* Goal: @Col Tn A B C *)
(* Goal: @Col Tn A B C *)
apply False_ind.
apply H14.
(* Goal: @Col Tn Q A B *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
ColR.
clear H17.


assert(OS B B' C C').
eapply l12_6.
(* Goal: @Le Tn A B C D *)
assumption.

assert(Per B B' A).
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
eapply (per_col _ _ P); try auto.
(* Goal: @Col Tn Q A B *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
ColR.

induction(eq_dec_points A C').
(* Goal: @Col Tn A B C' *)
subst C'.

assert(TS B B' A C).
unfold TS.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
repeat split; try auto.
apply per_not_col in H19.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
apply H19.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
exists B.
(* Goal: iff (@Bet Tn M A' B') (@Bet Tn M A B) *)
split.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: @Le Tn A B C D *)
assumption.
apply l9_2 in H20.
apply l9_9 in H20.
(* Goal: False *)
contradiction.


assert(TS B B' A C).
unfold TS.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
repeat split; try auto.
apply per_not_col in H19.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
apply H19.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
exists B.
(* Goal: iff (@Bet Tn M A' B') (@Bet Tn M A B) *)
split.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: @Le Tn A B C D *)
assumption.

assert(TS B B' C' A).

eapply l9_8_2.
apply l9_2.
apply H21.
(* Goal: @Le Tn A B C D *)
assumption.


unfold TS in H22.
(* Goal: @Col Tn A B C *)
spliter.
ex_and H24 T.


assert(T = B').
eapply l6_21.
apply not_col_permutation_1.
apply H23.
4: apply bet_col in H25.
4: apply col_permutation_2.
4: apply H25.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: @Col Tn Q A B *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
ColR.
(* Goal: or (and (not (@Col Tn A C T)) (and (@Perp Tn A C T P) (@Col Tn A C P))) (and (@Col Tn A C T) (@eq (@Tpoint Tn) P T)) *)
subst T.
Between.
Qed.

Lemma perp_not_eq_3 : forall A B C, Perp A B B C -> A <> C.
(* Goal: forall (A B C : @Tpoint Tn) (_ : @Par Tn A B A C), @Col Tn A B C *)
intros.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
apply perp_comm in H.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
apply perp_perp_in in H.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
assert(Per A B C).
(* Goal: @Per Tn A B C *)
(* Goal: not (@eq (@Tpoint Tn) A C) *)
apply perp_in_per.
(* Goal: @Perp_at Tn B A B B C *)
(* Goal: not (@eq (@Tpoint Tn) A C) *)
Perp.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
unfold Perp_at in H.
(* Goal: @Col Tn A B C *)
spliter.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
(* Goal: False *)
subst C.
(* Goal: False *)
apply l8_8 in H0.
(* Goal: False *)
contradiction.
Qed.


Lemma per_preserves_bet_aux2 : forall P Q A B C A' C', P <> Q -> Bet A B C ->
                                      Per A A' P -> Col P Q A' ->
                                      Col P Q B ->
                                      Per C C' P -> Col P Q C' ->
                                      P <> A'-> P <> B -> P <> C' ->
                                      Bet A' B C'.
(* Goal: forall (A B C : @Tpoint Tn) (_ : @Par Tn A B A C), @Col Tn A B C *)
intros.

induction (eq_dec_points A A').
(* Goal: @Col Tn A' B' C' *)
subst A'.

(* Goal: @eq (@Tpoint Tn) C C' *)
assert(Col A B C').
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
apply (col3 P Q); try auto.

(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
assert(Col P A B).
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
eapply (col_transitivity_1 _ Q); try auto.

(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
assert(Col Q A B).
eapply (col_transitivity_1 _ P).
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: @Col Tn A B C *)
Col.

(* Goal: @Le Tn A B D C *)
induction(eq_dec_points A B).
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
subst B.
apply between_trivial2.

(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
assert(Col P Q C).
eapply col3.
apply H12.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: @Col Tn A B C *)
Col.
apply bet_col.
(* Goal: @Le Tn A B C D *)
assumption.

assert(Col P C' C).
eapply col_transitivity_1.
apply H.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Le Tn A B C D *)
assumption.

assert(P=C' \/ C=C').
eapply l8_9.
(* Goal: @Per Tn C1 C1 A1 *)
apply l8_2.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Le Tn A B C D *)
assumption.

induction H15.
(* Goal: @Col Tn A B C' *)
subst C'.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
tauto.
(* Goal: @Col Tn A B C' *)
subst C'.
(* Goal: @Le Tn A B C D *)
assumption.


induction(eq_dec_points A C).
(* Goal: False *)
subst C.
apply between_identity in H0.
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
subst B.
(* Goal: @Col Tn A B C *)
(* Goal: @Col Tn A B C *)
apply False_ind.
apply H9.

apply l8_9 in H1.
(* Goal: not (@Col Tn P Q A) *)
induction H1.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Col Tn A' B' C' *)
subst A'.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
tauto.
(* Goal: @Col Tn Q A B *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
ColR.


assert(~Col P Q A).
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
assert (Col A A' P).
(* Goal: @Col Tn Q A B *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
ColR.
apply l8_9 in H1.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
induction H1;tauto.
(* Goal: @Le Tn A B C D *)
assumption.

assert(A <> B).
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
subst B.
(* Goal: False *)
contradiction.

induction (eq_dec_points C C').
(* Goal: @Col Tn A B C' *)
subst C'.
assert(Col A' B C).
(* Goal: @Le Tn A B C D *)
eapply (col3 P Q ); assumption.
assert(Col C A' P).
(* Goal: @Col Tn Q A B *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
ColR.

assert(B=C).
eapply l6_21.
apply H11.
apply H12.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: False *)
subst C.
(* Goal: @Bet Tn D C C *)
(* Goal: @Cong Tn A B D C *)
(* Goal: @Le Tn A B D C *)
apply between_trivial.

induction(eq_dec_points A' C').
(* Goal: @Col Tn A B C' *)
subst C'.

assert(Per  A A' B).
eapply per_col.
2:apply H1.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Col Tn Q A B *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
ColR.
assert(Per C A' B).
eapply per_col.
2:apply H4.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Col Tn Q A B *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
ColR.

eapply l8_6 in H14.
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
subst B.
(* Goal: @Bet Tn D C C *)
(* Goal: @Cong Tn A B D C *)
(* Goal: @Le Tn A B D C *)
apply between_trivial.
apply H15.
Between.

assert(HH:=ex_per_cong P Q B A P Q).
assert(exists T, Per T B P /\ Cong T B P Q /\ OS P Q T A).
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
apply HH; auto.
ex_and H15 T.
clear HH.

assert(Perp B B B P \/ Perp T B B P).
eapply perp_in_perp_bis.

apply per_perp_in.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
(* Goal: or (and (not (@Col Tn A C T)) (and (@Perp Tn A C T P) (@Col Tn A C P))) (and (@Col Tn A C T) (@eq (@Tpoint Tn) P T)) *)
subst T.
apply cong_symmetry in H16.
apply cong_identity in H16.
(* Goal: False *)
contradiction.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
induction H18.
apply perp_not_eq_1 in H18.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
tauto.

assert(Perp C' C' C' P \/ Perp C C' C' P).
eapply perp_in_perp_bis.

apply per_perp_in.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Le Tn A B C D *)
assumption.
induction H19.
apply perp_not_eq_1 in H19.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
tauto.

assert(Par T B C C').
eapply l12_9_2D.
apply H18.
(* Goal: @Perp Tn C1 P1 A1 C1 *)
(* Goal: @Per Tn P1 C1 A1 *)
apply perp_sym.
apply perp_left_comm.
eapply perp_col.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
apply perp_left_comm.
(* Goal: @Perp Tn C1 P1 A1 C1 *)
(* Goal: @Per Tn P1 C1 A1 *)
apply perp_sym.
apply H19.
eapply (col_transitivity_1 _ Q);
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.

assert(Perp A' A' A' P \/ Perp A A' A' P).
eapply perp_in_perp_bis.

apply per_perp_in.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Le Tn A B C D *)
assumption.
induction H21.
apply perp_not_eq_1 in H21.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
tauto.

assert(Par T B A A').
eapply l12_9_2D.
apply H18.
(* Goal: @Perp Tn C1 P1 A1 C1 *)
(* Goal: @Per Tn P1 C1 A1 *)
apply perp_sym.
apply perp_left_comm.
eapply perp_col.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
apply perp_left_comm.
(* Goal: @Perp Tn C1 P1 A1 C1 *)
(* Goal: @Per Tn P1 C1 A1 *)
apply perp_sym.
apply H21.
eapply (col_transitivity_1 _ Q);
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.

assert(Par_strict T B C C').
induction H20.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Col Tn A B C *)
spliter.
(* Goal: @Col Tn A B C *)
(* Goal: @Col Tn A B C *)
apply False_ind.

apply H14.
eapply per_id.
4:apply H1.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Per Tn C1 C1 A1 *)
apply l8_2.
eapply per_col.
(* Goal: @Per Tn C1 C1 A1 *)
2: apply l8_2.
2:apply H4.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.

apply col_permutation_2.
eapply col_transitivity_1.
2:apply bet_col.
2:apply between_symmetry.
apply bet_col in H0.
(* Goal: False *)
2: apply H0.

assert(~Col P Q C).
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
assert (Col C C' P).
(* Goal: @Col Tn Q A B *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
ColR.
apply l8_9 in H4.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
induction H1;tauto.
(* Goal: @Le Tn A B C D *)
assumption.

(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
(* Goal: False *)
subst C.
(* Goal: False *)
contradiction.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: @Col Tn Q A B *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
ColR.


assert(Par_strict T B A A').
induction H22.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Col Tn A B C *)
spliter.
(* Goal: @Col Tn A B C *)
(* Goal: @Col Tn A B C *)
apply False_ind.

apply H14.
eapply sym_equal.
eapply per_id.
4:apply H4.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Per Tn C1 C1 A1 *)
apply l8_2.
eapply per_col.
(* Goal: @Per Tn C1 C1 A1 *)
2: apply l8_2.
2:apply H1.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.

apply col_permutation_2.
eapply col_transitivity_1.
2:apply bet_col.
apply bet_col in H0.
(* Goal: False *)
2: apply H0.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: @Col Tn Q A B *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
ColR.

assert(OS T B C C').
apply l12_6.
(* Goal: @Le Tn A B C D *)
assumption.
assert(OS T B A A').
apply l12_6.
(* Goal: @Le Tn A B C D *)
assumption.

assert(TS T B A C).
unfold TS.
(* Goal: iff (@Bet Tn M A' B') (@Bet Tn M A B) *)
repeat split.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
unfold Par_strict in H24.
(* Goal: @Col Tn A B C *)
spliter.
apply H30.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X A B) (@Col Tn X A C)) *)
(* Goal: @Col Tn A B C *)
exists A.
(* Goal: iff (@Bet Tn M A' B') (@Bet Tn M A B) *)
split.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
unfold Par_strict in H23.
(* Goal: @Col Tn A B C *)
spliter.
apply H30.
(* Goal: @ex (@Tpoint Tn) (fun E : @Tpoint Tn => and (@Bet Tn D E C) (@Cong Tn A B D E)) *)
(* Goal: @Le Tn A B D C *)
exists C.
(* Goal: iff (@Bet Tn M A' B') (@Bet Tn M A B) *)
split.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Col Tn A B C *)
Col.
exists B.
(* Goal: iff (@Bet Tn M A' B') (@Bet Tn M A B) *)
split.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: @Le Tn A B C D *)
assumption.

assert(TS T B C' A).
eapply l9_8_2.
apply l9_2.
apply H27.
(* Goal: @Le Tn A B C D *)
assumption.

assert(TS T B A' C').
eapply l9_8_2.
apply l9_2.
apply H28.
(* Goal: @Le Tn A B C D *)
assumption.
unfold TS in H29.
(* Goal: @Col Tn A B C *)
spliter.
ex_and H31 BB.

assert(B=BB).
(* Goal: @Col Tn A B C *)
eapply (l6_21 T B A' C'); Col.
(* Goal: @Col Tn Q A B *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
ColR.
subst BB.
(* Goal: @Le Tn A B C D *)
assumption.
Qed.


Lemma par_col : forall A B C, Par A B A C -> Col A B C.
(* Goal: forall (A B C : @Tpoint Tn) (_ : @Par Tn A B A C), @Col Tn A B C *)
intros.
(* Goal: @Col Tn A B C *)
induction H.
(* Goal: @Col Tn A B C *)
(* Goal: @Col Tn A B C *)
unfold Par_strict in H.
(* Goal: @Col Tn A B C *)
spliter.
(* Goal: @Col Tn A B C *)
(* Goal: @Col Tn A B C *)
apply False_ind.
(* Goal: False *)
(* Goal: @Col Tn A B C *)
apply H2.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X A B) (@Col Tn X A C)) *)
(* Goal: @Col Tn A B C *)
exists A.
(* Goal: @Col Tn A B C *)
split; Col.
(* Goal: @Col Tn A B C *)
spliter.
(* Goal: @Col Tn A B C *)
Col.
Qed.

Lemma per_diff : forall A B A' B' P, A <> B -> ~ Col A B A' ->
                             Per A A' P -> Per B B' P ->
                             A' <> P -> B' <> P -> A' <> B'.
(* Goal: forall (A B C : @Tpoint Tn) (_ : @Par Tn A B A C), @Col Tn A B C *)
intros.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
(* Goal: @Col Tn A B A' *)
(* Goal: forall _ : @Col Tn A B A', @eq (@Tpoint Tn) A' B' *)
subst B'.
(* Goal: False *)
apply H0.
eapply per2__col.
apply H1.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Le Tn A B C D *)
assumption.
Qed.



Lemma per_preserves_bet : forall P Q A B C A' B' C', P <> Q -> Bet A B C ->
                                      Per A A' P -> Col P Q A' ->
                                      Per B B' P -> Col P Q B' ->
                                      Per C C' P -> Col P Q C' ->
                                      P <> A'-> P <> B' -> P <> C' ->
                                      Bet A' B' C'.
(* Goal: forall (A B C : @Tpoint Tn) (_ : @Par Tn A B A C), @Col Tn A B C *)
intros.

induction(eq_dec_points A A').
(* Goal: @Col Tn A' B' C' *)
subst A'.
(* Goal: @Le Tn A B C D *)
eapply (per_preserves_bet_aux1 P Q A B C B' C'); assumption.

induction(eq_dec_points B B').
(* Goal: @Col Tn A B A' *)
(* Goal: forall _ : @Col Tn A B A', @eq (@Tpoint Tn) A' B' *)
subst B'.
(* Goal: @Le Tn A B C D *)
eapply (per_preserves_bet_aux2 P Q A B C A' C'); assumption.

induction(eq_dec_points C C').
(* Goal: @Col Tn A B C' *)
subst C'.
assert(HH:=(per_preserves_bet_aux1 P Q C B A B' A')).
apply between_symmetry.
(* Goal: @Le Tn A B C D *)
apply HH; try assumption.
Between.

(* Goal: @Le Tn A B D C *)
induction (eq_dec_points A B).
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
subst B.
assert(A'=B').
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
eapply (per_id A _ _ P); try auto.
(* Goal: @Col Tn Q A B *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
ColR.
(* Goal: @Col Tn A B A' *)
(* Goal: forall _ : @Col Tn A B A', @eq (@Tpoint Tn) A' B' *)
subst B'.
apply between_trivial2.

induction (eq_dec_points C B).
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
subst B.
assert(C'=B').
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
eapply (per_id C _ _ P); try auto.
(* Goal: @Col Tn Q A B *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
ColR.
(* Goal: @Col Tn A B A' *)
(* Goal: forall _ : @Col Tn A B A', @eq (@Tpoint Tn) A' B' *)
subst B'.
(* Goal: @Bet Tn D C C *)
(* Goal: @Cong Tn A B D C *)
(* Goal: @Le Tn A B D C *)
apply between_trivial.

assert(A <> C).
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
(* Goal: False *)
subst C.
apply between_identity in H0.
(* Goal: False *)
contradiction.

assert(Perp B' B' B' P \/ Perp B B' B' P).
eapply perp_in_perp_bis.
apply per_perp_in.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Le Tn A B C D *)
assumption.
induction H16.
apply perp_not_eq_1 in H16.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
tauto.

assert(Perp C' C' C' P \/ Perp C C' C' P).
eapply perp_in_perp_bis.
apply per_perp_in.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Le Tn A B C D *)
assumption.
induction H17.
apply perp_not_eq_1 in H17.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
tauto.

assert(Perp A' A' A' P \/ Perp A A' A' P).
eapply perp_in_perp_bis.
apply per_perp_in.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Le Tn A B C D *)
assumption.
induction H18.
apply perp_not_eq_1 in H18.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
tauto.

assert(Par B B' C C').
eapply l12_9_2D.
apply H16.
(* Goal: @Perp Tn C1 P1 A1 C1 *)
(* Goal: @Per Tn P1 C1 A1 *)
apply perp_sym.
apply perp_left_comm.
eapply perp_col.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
apply perp_left_comm.
(* Goal: @Perp Tn C1 P1 A1 C1 *)
(* Goal: @Per Tn P1 C1 A1 *)
apply perp_sym.
apply H17.
eapply (col_transitivity_1 _ Q);
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.

assert(Par B B' A A').
eapply l12_9_2D.
apply H16.
(* Goal: @Perp Tn C1 P1 A1 C1 *)
(* Goal: @Per Tn P1 C1 A1 *)
apply perp_sym.
apply perp_left_comm.
eapply perp_col.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
apply perp_left_comm.
(* Goal: @Perp Tn C1 P1 A1 C1 *)
(* Goal: @Per Tn P1 C1 A1 *)
apply perp_sym.
apply H18.
eapply (col_transitivity_1 _ Q);
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.

(**************************************************************************************************)

(*induction(eq_dec_points A C).
(* Goal: False *)
subst C.
apply between_identity in H0.
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
subst B.
assert(A' = B').
eapply per_id.
4: apply H1.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Col Tn Q A B *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
ColR.
(* Goal: @Col Tn A B A' *)
(* Goal: forall _ : @Col Tn A B A', @eq (@Tpoint Tn) A' B' *)
subst B'.
apply between_trivial2.*)

assert(Col A B C).
apply bet_col.
(* Goal: @Le Tn A B C D *)
assumption.

induction(eq_dec_points A' C').
(* Goal: @Col Tn A B C' *)
subst C'.

assert(Col A C A').
eapply per2__col.
apply H1.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Le Tn A B C D *)
assumption.

assert(Col A B A').
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
eapply (col_transitivity_1 _ C); try auto.
(* Goal: @Col Tn A B C *)
Col.

assert(Per B A' P).
(* Goal: @Per Tn C1 C1 A1 *)
apply l8_2.
eapply (per_col _ _ A).
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Per Tn C1 C1 A1 *)
apply l8_2.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Col Tn A B C *)
Col.


assert(A' = B').
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
eapply (per_id B _ _ P); try auto.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
(* Goal: @Col Tn A' B' C' *)
subst A'.
apply par_right_comm in H20.
apply par_col in H20.

assert(Per P B B').
eapply (per_col _ _ A).
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Per Tn C1 C1 A1 *)
apply l8_2.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Col Tn A B C *)
Col.
apply H11.
eapply l8_7.
apply H25.
(* Goal: @Per Tn C1 C1 A1 *)
apply l8_2.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Col Tn Q A B *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
ColR.
(* Goal: @Col Tn A B A' *)
(* Goal: forall _ : @Col Tn A B A', @eq (@Tpoint Tn) A' B' *)
subst B'.
(* Goal: @Bet Tn D C C *)
(* Goal: @Cong Tn A B D C *)
(* Goal: @Le Tn A B D C *)
apply between_trivial.

(************************************* General case *********************************)

assert(Par A A' C C').
eapply par_trans.
apply par_symmetry.
apply H20.
(* Goal: @Le Tn A B C D *)
assumption.

assert(A' <> B').
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
(* Goal: @Col Tn A B A' *)
(* Goal: forall _ : @Col Tn A B A', @eq (@Tpoint Tn) A' B' *)
subst B'.
apply H22.
assert(Col A B A').
eapply per2__col.
apply H1.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Le Tn A B C D *)
assumption.
assert(Col C A A').
(* Goal: @Col Tn Q A B *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
ColR.
assert(Per P A' C).
eapply (per_col _ _ A).
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Per Tn C1 C1 A1 *)
apply l8_2.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Col Tn A B C *)
Col.
apply l8_2 in H26.
eapply (per_id).
4: apply H26.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
(* Goal: False *)
subst C.
apply perp_comm in H17.
apply perp_not_col in H17.
apply H17.
(* Goal: @Col Tn Q A B *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
ColR.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Col Tn Q A B *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
ColR.

assert(C' <> B').
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
(* Goal: @Col Tn A B A' *)
(* Goal: forall _ : @Col Tn A B A', @eq (@Tpoint Tn) A' B' *)
subst B'.
apply H22.
assert(Col B C C').
eapply per2__col.
apply H3.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Le Tn A B C D *)
assumption.
assert(Col A C C').
(* Goal: @Col Tn Q A B *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
ColR.
assert(Per P C' A).
eapply (per_col _ _ C).
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Per Tn C1 C1 A1 *)
apply l8_2.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Col Tn A B C *)
Col.
apply l8_2 in H27.
eapply (per_id).
5: apply H27.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Col Tn Q A B *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
ColR.

assert(Par_strict B B' C C').
induction H19.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Col Tn A B C *)
spliter.

(* Goal: @Col Tn A B C *)
(* Goal: @Col Tn A B C *)
apply False_ind.

apply H25.

eapply per_id.
5: apply H3.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
subst B.
apply perp_comm in H16.
apply perp_not_col in H16.
apply H16.
(* Goal: @Col Tn Q A B *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
ColR.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Per Tn C1 C1 A1 *)
apply l8_2.
eapply (per_col _ _ C).
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Per Tn C1 C1 A1 *)
apply l8_2.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: @Col Tn Q A B *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
ColR.

assert(Par_strict B B' A A').
induction H20.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Col Tn A B C *)
spliter.

(* Goal: @Col Tn A B C *)
(* Goal: @Col Tn A B C *)
apply False_ind.

apply H24.

eapply per_id.
5: apply H3.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
subst B.
apply perp_comm in H16.
apply perp_not_col in H16.
apply H16.
(* Goal: @Col Tn Q A B *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
ColR.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Per Tn C1 C1 A1 *)
apply l8_2.
eapply (per_col _ _ A).
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Per Tn C1 C1 A1 *)
apply l8_2.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: @Col Tn Q A B *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
ColR.

assert(OS B B' A A').
apply l12_6.
(* Goal: @Le Tn A B C D *)
assumption.
assert(OS B B' C C').
apply l12_6.
(* Goal: @Le Tn A B C D *)
assumption.
assert(TS B B' A C).
unfold TS.
(* Goal: and (@Bet Tn D C P') (@Cong Tn D P' A B) *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
repeat split; auto.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
apply H24.
eapply per_id.
4:apply H1.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.

(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Per Tn C1 C1 A1 *)
apply l8_2.
eapply per_col.
(* Goal: @Per Tn C1 C1 A1 *)
2: apply l8_2.
2:apply H3.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: @Col Tn Q A B *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
ColR.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
apply H25.
eapply per_id.
4: apply H5.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Per Tn C1 C1 A1 *)
apply l8_2.
eapply per_col.
(* Goal: @Per Tn C1 C1 A1 *)
2:apply l8_2.
2: apply H3.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: @Col Tn Q A B *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
ColR.
exists B.
(* Goal: iff (@Bet Tn M A' B') (@Bet Tn M A B) *)
split.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: @Le Tn A B C D *)
assumption.

assert(TS B B' A' C).
eapply l9_8_2.
apply H30.
(* Goal: @Le Tn A B C D *)
assumption.
assert(TS B B' A' C').
apply l9_2.
eapply l9_8_2.
apply l9_2.
apply H31.
(* Goal: @Le Tn A B C D *)
assumption.
unfold TS in H32.
(* Goal: @Col Tn A B C *)
spliter.
ex_and H34 BB.

assert(BB = B').
eapply l6_21.
apply not_col_permutation_1.
apply H33.
4:apply col_permutation_2.
4:apply bet_col.
4:apply H35.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: @Col Tn Q A B *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
ColR.
subst BB.
(* Goal: @Le Tn A B C D *)
assumption.
Qed.

Lemma ex_col : forall A B C, A <> B /\ A <> C /\ B <> C -> Col A B C -> exists D, Col A B D /\ A <> D /\ B <> D /\ C <> D.
(* Goal: forall (A B C : @Tpoint Tn) (_ : @Par Tn A B A C), @Col Tn A B C *)
intros.
(* Goal: @Col Tn A B C *)
spliter.
induction H0.
prolong A C D A C.
exists D.
(* Goal: iff (@Bet Tn M A' B') (@Bet Tn M A B) *)
repeat split.
apply bet_col.
eapply between_exchange4.
(* Goal: False *)
apply H0.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
subst D.
apply between_identity in H3.
(* Goal: False *)
contradiction.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
subst D.
assert(B = C).
eapply between_equality.
apply between_symmetry.
apply H3.
Between.
(* Goal: False *)
contradiction.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
subst D.
apply cong_symmetry in H4.
apply cong_identity in H4.
(* Goal: False *)
contradiction.

induction H0.
prolong B A D B A.
exists D.
(* Goal: iff (@Bet Tn M A' B') (@Bet Tn M A B) *)
repeat split.
apply bet_col in H3.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
subst D.
apply cong_symmetry in H4.
apply cong_identity in H4.
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
subst B.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
tauto.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
subst D.
apply between_identity in H3.
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
subst B.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
tauto.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
subst D.
assert(A = C).
eapply between_equality.
apply between_symmetry.
(* Goal: False *)
apply H0.
Between.
(* Goal: False *)
contradiction.

prolong C B D C B.
exists D.
(* Goal: iff (@Bet Tn M A' B') (@Bet Tn M A B) *)
repeat split.
apply bet_col.
eapply between_exchange3.
(* Goal: False *)
apply H0.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
subst D.
assert(A = B).
eapply between_equality.
apply between_symmetry.
apply H3.
Between.
(* Goal: False *)
contradiction.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
subst D.
apply cong_symmetry in H4.
apply cong_identity in H4.
(* Goal: False *)
subst C.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
tauto.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
subst D.
apply between_identity in H3.
(* Goal: False *)
subst C.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
tauto.
Qed.


Lemma out_preserves_eqo1 : forall A B P B', ~Col A B P -> Out A B B' -> eqo A B P A B' P.
(* Goal: forall (A B C : @Tpoint Tn) (_ : @Par Tn A B A C), @Col Tn A B C *)
intros.
unfold eqo.
(* Goal: iff (@Bet Tn M A' B') (@Bet Tn M A B) *)
repeat split.
(* Goal: @Le Tn A B C D *)
assumption.
assert(HH:=H0).
unfold Out in H0.
(* Goal: @Col Tn A B C *)
spliter.
apply out_col in HH.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
apply H.
(* Goal: @Col Tn Q A B *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
ColR.

(* Goal: forall (A B C : @Tpoint Tn) (_ : @Par Tn A B A C), @Col Tn A B C *)
intros.

assert(B=B2).
eapply l6_11_uniqueness.
(* Goal: False *)
3:apply H0.
unfold Out in H0.
(* Goal: @Col Tn A B C *)
spliter.
(* Goal: @Le Tn A B C D *)
assumption.
2: apply H6.
unfold Out in H5.
(* Goal: @Col Tn A B C *)
spliter.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
apply l6_6.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @eq (@Tpoint Tn) C' C' *)
apply cong_reflexivity.
subst B2.
apply l7_3 in H7.
subst M.

assert(Perp A B C1 A).
eapply perp_col.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
subst B.
apply H.
(* Goal: @Col Tn A B C *)
Col.
apply H3.
apply out_col in H5.
(* Goal: @Le Tn A B C D *)
assumption.

assert(A <> C).
apply perp_not_eq_2 in H1.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.

assert(A <> C1).
apply perp_not_eq_2 in H3.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.

assert(Col A C C1).
eapply perp2__col.
(* Goal: @Perp Tn C1 P1 A1 C1 *)
(* Goal: @Per Tn P1 C1 A1 *)
apply perp_sym.
apply perp_right_comm.
apply H1.
(* Goal: @Perp Tn C1 P1 A1 C1 *)
(* Goal: @Per Tn P1 C1 A1 *)
apply perp_sym.
(* Goal: @Perp_at Tn B A B B C *)
(* Goal: not (@eq (@Tpoint Tn) A C) *)
Perp.

induction (eq_dec_points P C).
(* Goal: @Per Tn P C A *)
(* Goal: @Per Tn P1 C1 A1 *)
subst P.

apply l8_9 in H4.
induction H4.
subst C1.
unfold Midpoint in H9.
(* Goal: @Col Tn A B C *)
spliter.
(* Goal: or (and (not (@Col Tn Q P A)) (and (@Perp Tn Q P A B) (@Col Tn Q P B))) (and (@Col Tn Q P A) (@eq (@Tpoint Tn) B A)) *)
(* Goal: or (and (not (@Col Tn Q P A)) (and (@Perp Tn Q P A B) (@Col Tn Q P B))) (and (@Col Tn Q P A) (@eq (@Tpoint Tn) B A)) *)
left.
(* Goal: @Le Tn A B C D *)
assumption.
subst C1.
apply perp_not_eq_2 in H3.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
tauto.
(* Goal: @Col Tn A B C *)
Col.

assert(P <> C1).
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
(* Goal: @Per Tn P C A *)
(* Goal: @Per Tn P1 C1 A1 *)
subst P.
apply H14.
apply l8_9 in H2.
induction H2.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: False *)
subst C.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
tauto.
(* Goal: @Col Tn A B C *)
Col.

assert(C1=C).
eapply per_id.
4:apply H4.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Col Tn A B C *)
Col.
subst C1.
unfold Midpoint in H9.
(* Goal: @Col Tn A B C *)
spliter.
(* Goal: or (and (not (@Col Tn Q P A)) (and (@Perp Tn Q P A B) (@Col Tn Q P B))) (and (@Col Tn Q P A) (@eq (@Tpoint Tn) B A)) *)
(* Goal: or (and (not (@Col Tn Q P A)) (and (@Perp Tn Q P A B) (@Col Tn Q P B))) (and (@Col Tn Q P A) (@eq (@Tpoint Tn) B A)) *)
left.
(* Goal: @Le Tn A B C D *)
assumption.
Qed.


Lemma out_preserves_eqo : forall A B P B' P', ~Col A B P -> Out A B B' -> Out A P P' -> eqo A B P A B' P'.
(* Goal: forall (A B C : @Tpoint Tn) (_ : @Par Tn A B A C), @Col Tn A B C *)
intros.

induction (eq_dec_points P P').
(* Goal: @eq (@Tpoint Tn) P P' *)
subst P'.
apply out_preserves_eqo1.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Le Tn A B C D *)
assumption.

unfold eqo.
(* Goal: iff (@Bet Tn M A' B') (@Bet Tn M A B) *)
repeat split.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
apply H.
assert(Col A B B').
apply out_col.
(* Goal: @Le Tn A B C D *)
assumption.
assert(Col A P P').
apply out_col.
(* Goal: @Le Tn A B C D *)
assumption.

assert(Col A P B').
apply (col_transitivity_1 _ P').
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
(* Goal: @eq (@Tpoint Tn) P P' *)
subst P'.
unfold Out in H1.
(* Goal: @Col Tn A B C *)
spliter.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: @Col Tn A B C *)
Col.
eapply (col_transitivity_1 _ B').
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
(* Goal: @Col Tn A B A' *)
(* Goal: forall _ : @Col Tn A B A', @eq (@Tpoint Tn) A' B' *)
subst B'.
unfold Out in H0.
(* Goal: @Col Tn A B C *)
spliter.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: @Col Tn A B C *)
Col.

(* Goal: forall (A B C : @Tpoint Tn) (_ : @Par Tn A B A C), @Col Tn A B C *)
intros.

assert(B = B2).
eapply l6_11_uniqueness.
4: apply H8.
(* Goal: False *)
3: apply H0.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
(* Goal: @Col Tn A B A' *)
(* Goal: forall _ : @Col Tn A B A', @eq (@Tpoint Tn) A' B' *)
subst B'.
unfold Out in H7.
(* Goal: @Col Tn A B C *)
spliter.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
subst B2.
unfold Out in H7.
(* Goal: @Col Tn A B C *)
spliter.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
apply l6_6.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @eq (@Tpoint Tn) C' C' *)
apply cong_reflexivity.
subst B2.

apply l7_3 in H9.
subst M.

assert(A <> C).
apply perp_not_eq_2 in H3.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
assert(A <> C1).
apply perp_not_eq_2 in H5.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.

assert(Perp A B C1 A).
eapply perp_col.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
subst B.
apply H.
(* Goal: @Col Tn A B C *)
Col.
apply H5.
apply out_col.
apply l6_6.
(* Goal: @Le Tn A B C D *)
assumption.

assert(Col A C C1).

eapply perp2__col.
(* Goal: @Perp Tn C1 P1 A1 C1 *)
(* Goal: @Per Tn P1 C1 A1 *)
apply perp_sym.
apply perp_comm.
apply H3.
apply perp_comm.
(* Goal: @Perp_at Tn B A B B C *)
(* Goal: not (@eq (@Tpoint Tn) A C) *)
Perp.

induction(eq_dec_points P C).
(* Goal: @Per Tn P C A *)
(* Goal: @Per Tn P1 C1 A1 *)
subst P.
assert(P'=C1).

apply l8_9 in H6.
induction H6.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: False *)
contradiction.
assert(HH:= H1).
unfold Out in H1.
(* Goal: @Col Tn A B C *)
spliter.
apply out_col in HH.
(* Goal: @Col Tn Q A B *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
ColR.
(* Goal: @eq (@Tpoint Tn) P P' *)
subst P'.

(* Goal: or (and (not (@Col Tn Q P A)) (and (@Perp Tn Q P A B) (@Col Tn Q P B))) (and (@Col Tn Q P A) (@eq (@Tpoint Tn) B A)) *)
(* Goal: or (and (not (@Col Tn Q P A)) (and (@Perp Tn Q P A B) (@Col Tn Q P B))) (and (@Col Tn Q P A) (@eq (@Tpoint Tn) B A)) *)
left.

unfold Out in H1.
(* Goal: @Col Tn A B C *)
spliter.
induction H17.
eapply between_exchange3.
apply between_symmetry.
apply H17.
apply midpoint_bet.
(* Goal: @Le Tn A B C D *)
assumption.
eapply outer_transitivity_between2.
apply between_symmetry.
apply H17.
apply midpoint_bet.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Le Tn A B C D *)
assumption.

assert(~Col P C A).
apply per_not_col.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Le Tn A B C D *)
assumption.

assert(C <> C1).
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
subst C1.
assert(Col P P' C).
eapply per2__col.
apply H4.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Le Tn A B C D *)
assumption.

(* Goal: False *)
(* Goal: @Col Tn A B C *)
apply H2.

eapply l6_21.
apply not_col_permutation_2.
apply H17.
5:apply col_permutation_2.
5:apply H18.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: @Col Tn A B C *)
Col.

assert(HH:=ex_col A C C1).
assert(A <> C /\ A <> C1 /\ C <> C1).
(* Goal: and (@Bet Tn D C P') (@Cong Tn D P' A B) *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
repeat split; auto.
apply HH in H19.
ex_and H19 D.

(* Goal: or (and (not (@Col Tn Q P A)) (and (@Perp Tn Q P A B) (@Col Tn Q P B))) (and (@Col Tn Q P A) (@eq (@Tpoint Tn) B A)) *)
(* Goal: or (and (not (@Col Tn Q P A)) (and (@Perp Tn Q P A B) (@Col Tn Q P B))) (and (@Col Tn Q P A) (@eq (@Tpoint Tn) B A)) *)
left.
unfold Out in H1.
(* Goal: @Col Tn A B C *)
spliter.

induction H24.
assert(Bet A C C1).
(* Goal: @Col Tn A B C *)
apply (per_preserves_bet D A A P P' A C C1); try auto; try Col.
(* Goal: @Per Tn C1 C1 A1 *)
apply l8_2.
(* Goal: @Per Tn A1 C1 C1 *)
apply l8_5.
eapply per_col.
2:apply H4.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Col Tn A B C *)
Col.
eapply per_col.
2:apply H6.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Col Tn Q A B *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
ColR.
(* Goal: @Col Tn Q A B *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
ColR.
eapply between_exchange3.
apply between_symmetry.
apply H25.
apply midpoint_bet.
(* Goal: @Le Tn A B C D *)
assumption.

assert(Bet A C1 C).
(* Goal: @Col Tn A B C *)
apply (per_preserves_bet D A A P' P A C1 C); try auto; try Col.
(* Goal: @Per Tn C1 C1 A1 *)
apply l8_2.
(* Goal: @Per Tn A1 C1 C1 *)
apply l8_5.
eapply per_col.
2:apply H6.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Col Tn Q A B *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
ColR.
(* Goal: @Col Tn Q A B *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
ColR.
eapply per_col.
2:apply H4.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Col Tn Q A B *)
(* Goal: @eq (@Tpoint Tn) C C' *)
(* Goal: @eq (@Tpoint Tn) C C' *)
ColR.
eapply between_symmetry.
eapply outer_transitivity_between.
2: apply H25.
apply midpoint_bet.
(* Goal: @Midpoint Tn M A' A *)
(* Goal: @Col Tn B' A' A *)
(* Goal: False *)
apply l7_2.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Le Tn A B C D *)
assumption.
Qed.


Lemma per_one_side : forall A B P Q C C', A <> P -> C' <> P -> ~Col A B C -> Col P Q A -> Col P Q C' -> Perp A B P Q -> Per C C' P -> OS A B C C'.
(* Goal: forall (A B C : @Tpoint Tn) (_ : @Par Tn A B A C), @Col Tn A B C *)
intros.
assert(A <> B).
apply perp_not_eq_1 in H4.
(* Goal: @Le Tn A B C D *)
assumption.

assert(P <> Q).
apply perp_not_eq_2 in H4.
(* Goal: @Le Tn A B C D *)
assumption.

induction (eq_dec_points C C').
(* Goal: @Col Tn A B C' *)
subst C'.
(* Goal: @eq (@Tpoint Tn) C' C' *)
apply one_side_reflexivity.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
apply H1.
(* Goal: @Col Tn A B C *)
Col.

assert(Perp C C' C' P).
eapply per_perp_in in H5.
eapply perp_in_perp_bis in H5.
(* Goal: @Le Tn A B D C *)
induction H5.
apply perp_not_eq_1 in H5.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
tauto.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.

assert(Perp C C' P Q).
(* Goal: @Perp Tn C1 P1 A1 C1 *)
(* Goal: @Per Tn P1 C1 A1 *)
apply perp_sym.
eapply perp_col.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Perp Tn C1 P1 A1 C1 *)
(* Goal: @Per Tn P1 C1 A1 *)
apply perp_sym.
apply perp_right_comm.
apply H9.
(* Goal: @Col Tn A B C *)
Col.
assert(Par C C' A B).
eapply l12_9_2D.
apply H10.
(* Goal: @Le Tn A B C D *)
assumption.

assert(Par_strict C C' A B).
induction H11.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Col Tn A B C *)
spliter.
(* Goal: @Col Tn A B C *)
(* Goal: @Col Tn A B C *)
apply False_ind.
apply H1.
(* Goal: @Col Tn A B C *)
Col.
eapply l12_6.
apply par_strict_symmetry.
(* Goal: @Le Tn A B C D *)
assumption.
Qed.


Lemma one_side_eqo : forall A B X Y, OS A B X Y -> eqo A B X A B Y.
(* Goal: forall (A B C : @Tpoint Tn) (_ : @Par Tn A B A C), @Col Tn A B C *)
intros.
unfold eqo.
(* Goal: iff (@Bet Tn M A' B') (@Bet Tn M A B) *)
repeat split.
eapply one_side_not_col123.
apply H.
apply one_side_symmetry in H.
eapply one_side_not_col123.
apply H.

(* Goal: forall (A B C : @Tpoint Tn) (_ : @Par Tn A B A C), @Col Tn A B C *)
intros.
apply l7_3 in H6.
subst M.

induction(eq_dec_points C C1).
subst C1.
(* Goal: or (and (not (@Col Tn Q P A)) (and (@Perp Tn Q P A B) (@Col Tn Q P B))) (and (@Col Tn Q P A) (@eq (@Tpoint Tn) B A)) *)
(* Goal: or (and (not (@Col Tn Q P A)) (and (@Perp Tn Q P A B) (@Col Tn Q P B))) (and (@Col Tn Q P A) (@eq (@Tpoint Tn) B A)) *)
left.
apply midpoint_bet.
(* Goal: @Le Tn A B C D *)
assumption.

assert(A <> C).
apply perp_not_eq_2 in H0.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.

assert(A <> C1).
apply perp_not_eq_2 in H2.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.

assert(A <> C /\ A <> C1 /\ C <> C1).
(* Goal: and (@Bet Tn D C P') (@Cong Tn D P' A B) *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
repeat split; auto.

assert(Col A C C1).
eapply perp2__col.
apply perp_comm.
(* Goal: @Perp Tn C1 P1 A1 C1 *)
(* Goal: @Per Tn P1 C1 A1 *)
apply perp_sym.
(* Goal: False *)
apply H0.
apply perp_comm.
(* Goal: @Perp_at Tn B A B B C *)
(* Goal: not (@eq (@Tpoint Tn) A C) *)
Perp.

assert(HH:=ex_col A C C1 H12 H13).
ex_and HH D.

assert(Perp A B D C).
(* Goal: @Perp Tn C1 P1 A1 C1 *)
(* Goal: @Per Tn P1 C1 A1 *)
apply perp_sym.
apply perp_left_comm.
eapply perp_col.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Perp Tn C1 P1 A1 C1 *)
(* Goal: @Per Tn P1 C1 A1 *)
apply perp_sym.
(* Goal: False *)
apply H0.
(* Goal: @Col Tn A B C *)
Col.

assert(~Col A B X).
unfold OS in H.
ex_and H T.
unfold TS in H.
(* Goal: @Col Tn A B C *)
spliter.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
apply H.
(* Goal: @Col Tn A B C *)
Col.

assert(~Col A B Y).
unfold OS in H.
ex_and H T.
unfold TS in H22.
(* Goal: @Col Tn A B C *)
spliter.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
apply H22.
(* Goal: @Col Tn A B C *)
Col.

assert(OS A B X C).
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
eapply (per_one_side A B D); auto.
apply  col_permutation_3.
apply H14.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: @Le Tn A B C D *)
assumption.
eapply per_col.
2: apply H1.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Col Tn A B C *)
Col.

assert(OS A B Y C1).
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
eapply (per_one_side A B D); auto.
apply col_permutation_3.
apply H14.
apply col_permutation_2.
(* Goal: @Col Tn A B C *)
eapply (col_transitivity_1 _ A);Col.
(* Goal: @Le Tn A B C D *)
assumption.
eapply per_col.
2: apply H3.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
apply col_permutation_2.
eapply (col_transitivity_1 _ C);
(* Goal: @Col Tn A B C *)
Col.

assert(OS A B C C1).
eapply one_side_transitivity.
apply one_side_symmetry.
apply H23.
eapply one_side_transitivity.
apply H.
(* Goal: @Le Tn A B C D *)
assumption.

assert(A <> B).
apply perp_not_eq_1 in H0.
(* Goal: @Le Tn A B C D *)
assumption.

assert(~ Col C1 A B).
unfold OS in H24.
ex_and H24 T.
unfold TS in H27.
(* Goal: @Col Tn A B C *)
spliter.
(* Goal: @Le Tn A B C D *)
assumption.

assert(TS A B C1 C').
unfold TS.
(* Goal: and (@Bet Tn D C P') (@Cong Tn D P' A B) *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
repeat split; auto.

(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
unfold Midpoint in H8.
(* Goal: @Col Tn A B C *)
spliter.

assert(C'=A).
eapply l6_21.
apply not_col_permutation_1.
apply H27.
4: apply bet_col.
4: apply H8.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
auto.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: @Col Tn A B C' *)
subst C'.
apply cong_identity in H29.
subst C1.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
tauto.
(* Goal: @ex (@Tpoint Tn) (fun X : @Tpoint Tn => and (@Col Tn X A B) (@Col Tn X A C)) *)
(* Goal: @Col Tn A B C *)
exists A.
unfold Midpoint in H8.
(* Goal: @Col Tn A B C *)
spliter.
(* Goal: and (@Bet Tn D C P') (@Cong Tn D P' A B) *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
split; auto.
(* Goal: @Col Tn A B C *)
Col.

assert(TS A B C C').
eapply l9_8_2.
apply H28.
apply one_side_symmetry.
(* Goal: @Le Tn A B C D *)
assumption.

assert(Col A C C').
eapply (col_transitivity_1 _ C1).
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Col Tn A B C *)
Col.
unfold Midpoint in H8.
(* Goal: @Col Tn A B C *)
spliter.
apply bet_col in H8.
(* Goal: @Col Tn A B C *)
Col.

unfold TS in H29.
(* Goal: @Col Tn A B C *)
spliter.
ex_and H32 AA.
assert(AA=A).
eapply l6_21.
apply not_col_permutation_1.
apply H31.
4: apply col_permutation_2.
4: apply bet_col.
4: apply H33.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
(* Goal: @Col Tn A B C' *)
subst C'.
apply between_identity in H33.
subst AA.
apply H31.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: @Col Tn A B C *)
Col.

subst AA.
(* Goal: or (and (not (@Col Tn Q P A)) (and (@Perp Tn Q P A B) (@Col Tn Q P B))) (and (@Col Tn Q P A) (@eq (@Tpoint Tn) B A)) *)
(* Goal: or (and (not (@Col Tn Q P A)) (and (@Perp Tn Q P A B) (@Col Tn Q P B))) (and (@Col Tn Q P A) (@eq (@Tpoint Tn) B A)) *)
left.
(* Goal: @Le Tn A B C D *)
assumption.
Qed.

Lemma ex_col1 : forall A B C, A <> B -> Col A B C -> exists D, Col A B D /\ A <> D /\ B <> D /\ C <> D.
(* Goal: forall (A B C : @Tpoint Tn) (_ : @Par Tn A B A C), @Col Tn A B C *)
intros.
induction H0.
prolong A C D A C.
exists D.
(* Goal: iff (@Bet Tn M A' B') (@Bet Tn M A B) *)
repeat split.
apply bet_col.
eapply between_exchange4.
(* Goal: False *)
apply H0.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
subst D.
apply between_identity in H1.
(* Goal: False *)
subst C.
apply between_identity in H0.
(* Goal: False *)
contradiction.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
subst D.
assert(B = C).
eapply between_equality.
apply between_symmetry.
apply H1.
Between.
(* Goal: False *)
subst C.
apply cong_symmetry in H2.
apply cong_identity in H2.
(* Goal: False *)
contradiction.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
subst D.
apply cong_symmetry in H2.
apply cong_identity in H2.
(* Goal: False *)
subst C.
apply between_identity in  H0.
(* Goal: False *)
contradiction.

induction H0.
prolong B A D B A.
exists D.
(* Goal: iff (@Bet Tn M A' B') (@Bet Tn M A B) *)
repeat split.
apply bet_col in H1.
(* Goal: @Col Tn A B C *)
Col.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
subst D.
apply cong_symmetry in H2.
apply cong_identity in H2.
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
subst B.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
tauto.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
subst D.
apply between_identity in H1.
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
subst B.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
tauto.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
subst D.
assert(A = C).
eapply between_equality.
apply between_symmetry.
(* Goal: False *)
apply H0.
Between.
(* Goal: False *)
subst C.
apply cong_symmetry in H2.
apply cong_identity in H2.
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
subst B.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
tauto.

prolong C B D C B.
exists D.
(* Goal: iff (@Bet Tn M A' B') (@Bet Tn M A B) *)
repeat split.
apply bet_col.
eapply between_exchange3.
(* Goal: False *)
apply H0.
(* Goal: @Le Tn A B C D *)
assumption.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
subst D.
assert(A = B).
eapply between_equality.
apply between_symmetry.
apply H1.
Between.
(* Goal: False *)
contradiction.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
subst D.
apply cong_symmetry in H2.
apply cong_identity in H2.
(* Goal: False *)
subst C.
apply between_identity in H0.
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
subst B.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
tauto.
(* Goal: not (@eq (@Tpoint Tn) A C) *)
intro.
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
subst D.
apply between_identity in H1.
(* Goal: False *)
subst C.
apply between_identity in H0.
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
subst B.
(* Goal: @Le Tn C D A B *)
(* Goal: @Le Tn A B D C *)
(* Goal: @Le Tn A B D C *)
tauto.
Qed.

End Orientation.