Library orthogonality

Require Export midpoint.

Section T8.

Context `{MT:Tarski}.


Ltac assert_cols :=
repeat
 match goal with
      | H:Bet ?X1 ?X2 ?X3 |- _ =>
     not_exist_hyp (Col X1 X2 X3);assert (Col X1 X2 X3) by (apply bet_col;apply H)
 end.

Ltac clean_trivial_hyps :=
  repeat
  match goal with
   | H:(Cong ?X1 ?X1 ?X2 ?X2) |- _ => clear H
   | H:(Cong ?X1 ?X2 ?X2 ?X1) |- _ => clear H
   | H:(Cong ?X1 ?X2 ?X1 ?X2) |- _ => clear H
   | H:(Bet ?X1 ?X1 ?X2) |- _ => clear H
   | H:(Bet ?X2 ?X1 ?X1) |- _ => clear H
   | H:(Col ?X1 ?X1 ?X2) |- _ => clear H
   | H:(Col ?X2 ?X1 ?X1) |- _ => clear H
   | H:(Col ?X1 ?X2 ?X1) |- _ => clear H
end.

Ltac smart_subst X := subst X;clean_trivial_hyps;clean_duplicated_hyps.

Ltac treat_equalities_aux :=
  match goal with
   | H:(?X1 = ?X2) |- _ => smart_subst X2
end.

Ltac treat_equalities :=
try treat_equalities_aux;
repeat
  match goal with
   | H:(Cong ?X3 ?X3 ?X1 ?X2) |- _ =>
      apply cong_symmetry in H; apply cong_identity in H;smart_subst X2
   | H:(Cong ?X1 ?X2 ?X3 ?X3) |- _ =>
      apply cong_identity in H;smart_subst X2
   | H:(Bet ?X1 ?X2 ?X1) |- _ => apply between_identity in H;smart_subst X2
end.

Ltac show_distinct X Y := assert (X<>Y);[unfold not;intro;treat_equalities|idtac].

Hint Resolve between_symmetry : Between.
Hint Resolve bet_col : Between.
Hint Resolve between_trivial between_trivial2 : Between_no_eauto.

Ltac eBetween := treat_equalities;eauto with Between.
Ltac Between := treat_equalities;auto with Between Between_no_eauto.

Ltac prolong A B x C D :=
 assert (sg:= segment_construction A B C D);
 ex_and sg x.

Hint Resolve cong_commutativity cong_reverse_identity cong_trivial_identity
             cong_left_commutativity cong_right_commutativity
             cong_transitivity cong_symmetry cong_reflexivity cong_identity : cong.
Hint Resolve cong_3_sym : Cong.
Hint Resolve cong_3_swap cong_3_swap_2 cong3_transitivity : Cong3.
Hint Unfold Cong_3 : Cong3.
Hint Resolve outer_transitivity_between2 between_inner_transitivity between_exchange3 between_exchange2: Between.
Hint Resolve outer_transitivity_between between_exchange4.

Ltac Cong := auto with cong.
Ltac eCong := eauto with cong.

Hint Resolve col_permutation_1 col_permutation_2
col_permutation_3 col_permutation_4 col_permutation_5 : Col.
Hint Immediate col_trivial_1 col_trivial_2 col_trivial_3: Col.
Hint Resolve col_transitivity_1 col_transitivity_2 : Col.

Ltac Col := auto with Col.
Ltac eCol := eauto with Col.


Definition Per := fun A B C => exists C', is_midpoint B C C' /\ Cong A C A C'.

Lemma l8_2 : forall A B C, Per A B C -> Per C B A.
Proof.
unfold Per.
intros.
ex_and H C'.

assert (exists A', is_midpoint B A A').
apply symmetric_point_construction.
ex_and H1 A'.

exists A'.
split.
assumption.

eapply cong_transitivity.
apply cong_commutativity.
apply H0.
eapply l7_13.
apply H.
apply l7_2.
assumption.
Qed.

Hint Resolve l8_2 : Perp.

Ltac Perp := eauto with Perp.

Lemma l8_3 : forall A B C A',
 Per A B C -> A<>B -> Col B A A' -> Per A' B C.
unfold Per.
intros.
ex_and H C'.

exists C'.
split.
assumption.
eapply l4_17.
apply H0.
apply col_permutation_4.
assumption.
assumption.
unfold is_midpoint in H.
spliter.
apply cong_left_commutativity.
assumption.
Qed.

Lemma l8_4 : forall A B C C', Per A B C -> is_midpoint B C C' -> Per A B C'.
Proof.
unfold Per.
intros.
ex_and H B'.
exists C.
split.
apply l7_2.
assumption.
assert (B' = C').
eapply symmetric_point_unicity;eauto.
subst B'.
Cong.
Qed.

Lemma l8_5 : forall A B, Per A B B.
Proof.
unfold Per.
intros.
exists B.
split.
apply l7_3_2.
apply cong_reflexivity.
Qed.

Hint Resolve l8_5 : Perp.

Lemma l8_6 : forall A B C A', Per A B C -> Per A' B C -> Bet A C A' -> B=C.
Proof.
unfold Per.
intros.
ex_and H C'.
ex_and H0 C''.
assert (C'=C'').
eapply symmetric_point_unicity;eauto.
subst C''.
assert (C = C').
eapply l4_19;eauto.
subst C'.
apply l7_3.
assumption.
Qed.

Ltac let_symmetric C P A :=
let id1:=fresh in (assert (id1:(exists A', is_midpoint P A A'));
[apply symmetric_point_construction|ex_and id1 C]).

Ltac symmetric B' A B :=
assert(sp:= symmetric_point_construction B A); ex_and sp B'.

Lemma l8_7 : forall A B C, Per A B C -> Per A C B -> B=C.
Proof.
intros.
unfold Per in H.
ex_and H C'.
symmetric A' C A.

induction (eq_dec_points B C).
assumption.

assert (Per C' C A).
eapply (l8_3 ).
eapply l8_2.
apply H0.
assumption.

unfold is_midpoint in H.
spliter.
unfold Col.
left.
assumption.

assert (Cong A C' A' C').
unfold Per in H4.
ex_and H4 Z.

assert (A' = Z).
eapply symmetric_point_unicity.
apply H2.
assumption.
subst Z.
apply cong_commutativity.
assumption.

unfold is_midpoint in *.
spliter.

assert (Cong A' C A' C').
eapply cong_transitivity.
apply cong_symmetry.
apply cong_commutativity.
apply H6.
eapply cong_transitivity.
apply cong_commutativity.
apply H1.
apply cong_left_commutativity.
assumption.

assert (Per A' B C).
unfold Per.
exists C'.

unfold is_midpoint.
repeat split;auto.

eapply l8_6.
apply H9.
unfold Per.
exists C'.
split.
unfold is_midpoint;auto.

apply H1.
Between.
Qed.

Hint Resolve l8_2 l8_5 l8_7: Perp.

Lemma l8_8 : forall A B, Per A B A -> A=B.
Proof.
intros.
eapply l8_7.
eapply l8_2.
eapply l8_5.
assumption.
Qed.

Lemma l8_9 : forall A B C, Per A B C -> Col A B C -> A=B \/ C=B.
Proof.
intros.
induction (eq_dec_points A B).
left.
assumption.
right.
eapply l8_7.

eapply l8_2.
eapply l8_5.

eapply l8_3;eCol.
Qed.

Lemma l8_10 : forall A B C A' B' C', Per A B C -> Cong_3 A B C A' B' C' -> Per A' B' C'.
Proof.
unfold Per.
intros.
ex_and H D.
prolong C' B' D' B' C'.
exists D'.
split.
unfold is_midpoint.
split.
assumption.
apply cong_left_commutativity.
apply cong_symmetry.
assumption.
unfold Cong_3, is_midpoint in *.
spliter.
induction (eq_dec_points C B).
treat_equalities;Cong.

assert(OFSC C B D A C' B' D' A').
unfold OFSC.
repeat split.
assumption.
assumption.
Cong.
eapply cong_transitivity.
apply cong_symmetry.
apply H4.
eapply cong_transitivity.
apply cong_commutativity.
apply H6.
Cong.

Cong.
Cong.

assert (Cong D A D' A').
eapply five_segments_with_def.
apply H8.
assumption.

eapply cong_transitivity.
apply cong_symmetry.
apply H5.

eapply cong_transitivity.
apply H1.
Cong.
Qed.

Definition Perp_in := fun X A B C D =>
   A<>B /\ C<>D /\ Col X A B /\ Col X C D /\ (forall U V, Col U A B -> Col V C D -> Per U X V).

Definition Perp := fun A B C D => exists X, Perp_in X A B C D.

Lemma l8_12 : forall A B C D X, Perp_in X A B C D -> Perp_in X C D A B.
Proof.
unfold Perp_in.
intros.
spliter.
repeat split;try assumption.
intros;eapply l8_2;eauto.
Qed.

Lemma col_col : forall A B X Y Z, A <> B -> Col A B X -> Col A B Y -> Col A B Z -> Col X Y Z.
Proof.
intros.
assert(Col A X Y) by eCol.
assert(Col A X Z) by eCol.
induction (eq_dec_points A X).
subst X.
eCol.
eCol.
Qed.

Lemma l4_3_1 : forall A B C A' B' C', Bet A B C -> Bet A' B' C' -> Cong A B A' B' -> Cong A C A' C' -> Cong B C B' C'.
Proof.
intros.
apply cong_commutativity.
eapply (l4_3);
eBetween;eCong.
Qed.

Lemma per_col : forall A B C D, B <> C -> Per A B C -> Col B C D -> Per A B D.
Proof.
unfold Per.
intros.
ex_and H0 C'.
prolong D B D' D B.
exists D'.

assert (is_midpoint B C C').
apply H0.
induction H5.

assert (is_midpoint B D D') by
 (unfold is_midpoint;split;Cong).

assert (is_midpoint B D D').
apply H7.

induction H8.

repeat split.
assumption.
apply cong_symmetry.
assumption.

unfold Col in H1.
induction H1.

assert (Bet B C' D').
eapply l7_15.
eapply l7_3_2.
apply H0.
apply H7.
assumption.

assert (Cong C D C' D').
eapply l4_3_1.
apply H1.
apply H10.
apply cong_left_commutativity.
assumption.
apply cong_left_commutativity.
assumption.

assert(OFSC B C D A B C' D' A).
unfold OFSC.
repeat split.
assumption.
assumption.
apply cong_left_commutativity.
assumption.
assumption.
Cong.
Cong.
apply cong_commutativity.

eapply five_segments_with_def.
apply H12.
assumption.
induction H1.

assert (Bet C' D' B).
eapply l7_15.
apply H0.
apply H7.
apply l7_3_2.
assumption.

assert (Cong C D C' D').
eapply l4_3.
apply H1.
apply H10.
apply cong_right_commutativity.
assumption.
apply cong_right_commutativity.
assumption.

assert(IFSC B D C A B D' C' A).
unfold IFSC.
repeat split.
apply between_symmetry.
assumption.
apply between_symmetry.
assumption.
apply cong_left_commutativity.
assumption.
apply cong_commutativity.
assumption.
apply cong_reflexivity.
apply cong_commutativity.
assumption.

apply cong_commutativity.

eapply l4_2.
apply H12.

assert (Bet D' B C').
eapply l7_15.
apply H7.
eapply l7_3_2.
apply H0.
assumption.

assert (Cong C D C' D').
eapply l2_l1.
apply between_symmetry.
apply H1.
apply between_symmetry.
apply H10.
apply cong_right_commutativity.
assumption.
apply cong_left_commutativity.
assumption.

assert(OFSC C B D A C' B D' A).
unfold OFSC.
repeat split.
apply between_symmetry.
assumption.
apply between_symmetry.
assumption.
apply cong_right_commutativity.
assumption.
apply cong_left_commutativity.
assumption.
apply cong_commutativity.
assumption.
apply cong_reflexivity.
apply cong_commutativity.

eapply five_segments_with_def.
apply H12.
auto.
Qed.

Lemma l8_13_2 : forall A B C D X,
   A <> B -> C <> D -> Col X A B -> Col X C D ->
  (exists U, exists V :Tpoint, Col U A B /\ Col V C D /\ U<>X /\ V<>X /\ Per U X V) ->
  Perp_in X A B C D.
Proof.
intros.
ex_and H3 U.
ex_and H4 V.
unfold Perp_in.
repeat split;try assumption.
intros.

assert (Per V X U0).
eapply l8_2.
eapply l8_3.
apply H7.
assumption.
eapply col_col.
apply H.
Col.
Col.
Col.

eapply per_col.
2:eapply l8_2.
2:apply H10.
auto.
eapply col_col.
apply H0.
Col.
Col.
Col.
Qed.

Definition DistLn := fun A B C D =>
(exists X, Col X A B /\ ~Col X C D) \/ (exists X, ~ Col X A B /\ Col X C D).

Lemma perBAB : forall A B, Per B A B -> A = B.
Proof.
intros.
eapply l8_7.
apply H.
eapply l8_2.
apply l8_5.
Qed.

Lemma l8_14_1 : forall A B, ~ Perp A B A B.
Proof.
intros.
unfold Perp.
intro.
ex_and H X.
unfold Perp_in in H0.
spliter.

assert (Per A X A).
apply H3.
apply col_trivial_1.
apply col_trivial_1.

assert (A = X).
eapply l8_7.
2: apply H4.
apply l8_2.
apply l8_5.

assert (Per B X B).
apply H3.
apply col_trivial_3.
apply col_trivial_3.

assert (B = X).
eapply l8_7.
2: apply H6.
apply l8_2.
apply l8_5.

apply H0.
congruence.
Qed.

Lemma l8_14_2_1a : forall X A B C D, Perp_in X A B C D -> Perp A B C D.
Proof.
intros.
spliter.
unfold Perp.
exists X.
assumption.
Qed.

Lemma l8_14_2_1b : forall X A B C D Y, Perp_in X A B C D -> Col Y A B -> Col Y C D -> X=Y.
Proof.
intros.
unfold Perp_in in H.
spliter.
eapply (H5 Y Y) in H1.
2:assumption.
apply perBAB.
assumption.
Qed.

Lemma l8_14_2_1b_bis : forall A B C D X, Perp A B C D -> Col X A B -> Col X C D -> Perp_in X A B C D.
Proof.
intros.
unfold Perp in H.
ex_and H Y.
assert (Y = X).
eapply (l8_14_2_1b Y _ _ _ _ X) in H2.
assumption.
assumption.
assumption.
subst Y.
assumption.
Qed.

Lemma l8_14_2_2 : forall X A B C D,
 Perp A B C D -> (forall Y, Col Y A B -> Col Y C D -> X=Y) -> Perp_in X A B C D.
Proof.
intros.
eapply l8_14_2_1b_bis.
assumption.
unfold Perp in H.
ex_and H Y.
unfold Perp_in in H1.
spliter.
assert (Col Y C D).
assumption.

apply (H0 Y H2) in H3.
subst Y.
assumption.

unfold Perp in H.
ex_and H Y.
unfold Perp_in in H1.
spliter.
assert (Col Y C D).
assumption.

apply (H0 Y H2) in H3.
subst Y.
assumption.
Qed.

Lemma l8_14_3 : forall A B C D X Y, Perp_in X A B C D -> Perp_in Y A B C D -> X=Y.
Proof.
intros.
eapply l8_14_2_1b.
apply H.
unfold Perp_in in H0.
spliter.
assumption.
eapply l8_12 in H0.
unfold Perp_in in H0.
spliter.
assumption.
Qed.

Lemma l8_15_1 : forall A B C X, A<>B -> Col A B X -> Perp A B C X -> Perp_in X A B C X.
Proof.
intros.
eapply l8_14_2_1b_bis.
assumption.
Col.
apply col_trivial_3.
Qed.

Lemma l8_15_2 : forall A B C X, A<>B -> Col A B X -> Perp_in X A B C X -> Perp A B C X.
intros.
eapply l8_14_2_1a.
apply H1.
Qed.

Lemma perp_in_per : forall A B C, Perp_in B A B B C-> Per A B C.
intros.
unfold Perp_in in H.
spliter.
apply H3.
apply col_trivial_1.
apply col_trivial_3.
Qed.

Lemma perp_sym : forall A B C D, Perp A B C D -> Perp C D A B.
unfold Perp.
intros.
ex_and H X.
exists X.
apply l8_12.
assumption.
Qed.

Lemma perp_col0 : forall A B C D X Y, Perp A B C D -> X <> Y -> Col A B X -> Col A B Y -> Perp C D X Y.
unfold Perp.
intros.
ex_and H X0.
exists X0.
unfold Perp_in in *.
spliter.
repeat split.
assumption.
assumption.
assumption.
eapply col_col.
apply H.
apply col_permutation_1.
assumption.
assumption.
assumption.
intros.
eapply l8_2.

apply H6.
2:assumption.

assert(Col A X Y).
eapply col_col.
apply H.
apply col_trivial_3.
assumption.
assumption.
assert (Col B X Y).
eapply col_col.
apply H.
apply col_trivial_2.
assumption.
assumption.

eapply col_col.
apply H0.
apply col_permutation_1.
assumption.
apply col_permutation_1.
assumption.
apply col_permutation_1.
assumption.
Qed.

Lemma l8_16_1 : forall A B C U X,
  A<>B -> Col A B X -> Col A B U -> U<>X -> Perp A B C X -> ~ Col A B C /\ Per C X U.
intros.
split.
intro.

assert (Perp_in X A B C X).
eapply l8_15_1.
assumption.
assumption.
assumption.

assert (X = U).
eapply l8_14_2_1b.
apply H5.
apply col_permutation_2 in H1.
apply H1.
eapply col_col.
apply H.
assumption.
assumption.
assumption.
apply H2.
subst X.
reflexivity.

eapply l8_14_2_1b_bis.

assert (Col A X U).
eapply col_col.
apply H.
apply col_trivial_3.
assumption.
assumption.
eapply perp_col0.
apply H3.
intro.
apply H2.
apply H5.
assumption.
assumption.
apply col_trivial_3.
apply col_trivial_3.
apply col_trivial_1.
apply col_trivial_1.
Qed.

Lemma per_perp_in : forall A B C, A <> B -> B <> C -> Per A B C -> Perp_in B A B B C.
intros.
unfold Perp.
repeat split.
assumption.
assumption.
apply col_trivial_3.
apply col_trivial_1.
intros.
eapply per_col.
apply H0.
eapply l8_2.
eapply per_col.
intro.
apply H.
apply sym_equal.
apply H4.
apply l8_2.
assumption.
apply col_permutation_3.
assumption.
apply col_permutation_1.
assumption.
Qed.

Lemma per_perp : forall A B C, A <> B -> B <> C -> Per A B C -> Perp A B B C.
intros.
apply per_perp_in in H1.
eapply l8_14_2_1a.
apply H1.
assumption.
assumption.
Qed.

Lemma perp_left_comm : forall A B C D, Perp A B C D -> Perp B A C D.
unfold Perp.
intros.
ex_and H X.
exists X.
unfold Perp_in in *.
spliter.
repeat split.
auto.
assumption.
apply col_permutation_5.
assumption.
assumption.
intros.
apply H3.
apply col_permutation_5.
assumption.
assumption.
Qed.

Lemma perp_right_comm : forall A B C D, Perp A B C D -> Perp A B D C.
unfold Perp.
intros.
ex_and H X.
exists X.
unfold Perp_in in *.
spliter.
repeat split.
assumption.
auto.
assumption.
apply col_permutation_5.
assumption.
intros.
apply H3.
assumption.
apply col_permutation_5.
assumption.
Qed.

Lemma perp_comm : forall A B C D, Perp A B C D -> Perp B A D C.
intros.
apply perp_left_comm.
apply perp_right_comm.
assumption.
Qed.

Lemma l8_16_2 : forall A B C U X,
  A<>B -> Col A B X -> Col A B U -> U<>X -> ~ Col A B C -> Per C X U -> Perp A B C X.
intros.

assert (C <> X).
intro.
subst X.
apply H3.
assumption.
unfold Perp.
exists X.
eapply l8_13_2.
assumption.
assumption.
apply col_permutation_2.
assumption.
apply col_trivial_3.
exists U.
exists C.
repeat split.
apply col_permutation_2.
assumption.
apply col_trivial_1.
assumption.
assumption.
apply l8_2.
assumption.
Qed.

Lemma l8_16_2' : forall A B C U X,
  A<>B -> Col A B X -> Col A B U -> U<>X -> ~ Col A B C -> Per C X U -> Perp A B C X.
intros.
apply l8_2 in H4.
apply per_perp in H4.
apply perp_sym.
eapply perp_col0.
apply perp_right_comm.
apply H4.
assumption.
eapply col_col.
apply H.
assumption.
assumption.
apply col_trivial_3.
eapply col_col.
apply H.
assumption.
assumption.
apply col_trivial_2.
assumption.
intro.
apply H3.
subst X.
assumption.
Qed.

Lemma l8_18_unicity : forall A B C X Y,
  ~ Col A B C -> Col A B X -> Perp A B C X -> Col A B Y -> Perp A B C Y -> X=Y.
Proof.
intros.

assert (A <> B).
intro.
subst B.
apply H.
apply col_trivial_1.

assert (Perp_in X A B C X).
eapply l8_15_1;assumption.

assert (Perp_in Y A B C Y).
eapply l8_15_1;assumption.

unfold Perp_in in *.
spliter.

eapply l8_7;
eapply l8_2;
[apply H14 |apply H10].
assumption.
apply col_trivial_1.
assumption.
apply col_trivial_1.
Qed.

Lemma is_midpoint_id : forall A B, is_midpoint A A B -> A = B.
Proof.
intros.
unfold is_midpoint in H.
spliter.
treat_equalities;reflexivity.
Qed.


Lemma distinct : forall A B X C C', ~Col A B C -> Col A B X -> is_midpoint X C C' -> C <> C'.
Proof.
intros.
intro.
subst C'.
apply H.
unfold is_midpoint in H1.
spliter.
treat_equalities.
assumption.
Qed.

Lemma l8_18_existence : forall A B C, ~ Col A B C -> exists X, Col A B X /\ Perp A B C X.
intros.

prolong B A Y A C.

assert (exists P, is_midpoint P C Y).
eapply l7_25.
apply cong_symmetry.
apply H1.
ex_and H2 P.

assert (Per A P Y).
unfold Per.
exists C.
split.
apply l7_2.
assumption.
assumption.

prolong A Y Z Y P.

prolong P Y Q Y A.

prolong Q Z Q' Q Z.

assert (is_midpoint Z Q Q').
unfold is_midpoint.
split.
assumption.
apply cong_symmetry.
assumption.

prolong Q' Y C' Y C.

assert (exists X, is_midpoint X C C').
eapply l7_25.
apply cong_symmetry.
apply H12.

ex_and H13 X.

assert (OFSC A Y Z Q Q Y P A).
unfold OFSC.
repeat split.
assumption.
apply between_symmetry.
assumption.
apply cong_commutativity.
apply cong_symmetry.
assumption.
assumption.
apply cong_pseudo_reflexivity.
assumption.

induction (eq_dec_points A Y).
subst Y.
apply cong_symmetry in H1.
apply cong_identity in H1.
subst C.
apply False_ind.
apply H.
apply col_trivial_3.

assert (Cong Z Q P A).
eapply five_segments_with_def.
apply H13.
assumption.

assert (Cong_3 A P Y Q Z Y).
unfold Cong_3.
repeat split.
apply cong_commutativity.
apply cong_symmetry.
assumption.
apply cong_commutativity.
apply cong_symmetry.
assumption.
apply cong_commutativity.
apply cong_symmetry.
assumption.

assert (Per Q Z Y).
eapply l8_10.
2:apply H17.
assumption.

assert (Per Y Z Q).
eapply l8_2.
assumption.

unfold Per in H19.
ex_and H19 Q''.

assert (Q' = Q'').
eapply symmetric_point_unicity.
apply H10.
assumption.
subst Q''.
clear H19.

assert( Q <> Y).
intro.
subst Q.
apply cong_symmetry in H7.
apply cong_identity in H7.
subst Y.
apply H15.
reflexivity.

assert (Per Y X C).
unfold Per.
exists C'.
split.
assumption.
apply cong_symmetry.
assumption.

assert (P <> Y).
intro.
subst P.
apply cong_identity in H5.
subst Z.
apply l7_2 in H3.
apply is_midpoint_id in H3.
subst Y.
apply H.
unfold Col.
right;right.
apply between_symmetry.
assumption.

assert (A <> B).
intro.
subst B.
apply H.
apply col_trivial_1.

assert(A <> C).
intro.
subst C.
apply H.
apply col_trivial_3.
assert (B <> C).
intro.
subst C.
apply H.
apply col_trivial_2.

assert (Y <> C).
intro.
subst Y.
apply H.
unfold Col.
right;right.
apply between_symmetry.
assumption.

assert (Col P Y Q).
unfold Col.
left.
assumption.
assert(Col P Y C).
unfold is_midpoint in H3.
spliter.
unfold Col.
right; right.
assumption.

assert (Col P Q C).
eapply col_transitivity_1.
apply H22.
assumption.
assumption.

assert (Col Y Q C).
eapply col_transitivity_2.
apply H22.
assumption.
assumption.

assert (Col A Y B).
unfold Col.
right;right.
assumption.

assert (Col A Y Z).
unfold Col.
left.
assumption.

assert (Col A B Z).
eapply col_transitivity_1.
apply H15.
assumption.
assumption.

assert (Col Y B Z).
eapply col_transitivity_2.
apply H15.
assumption.
assumption.

assert (Col Q Y P).
eapply col_permutation_3.
assumption.

assert(Q <> C).
intro.
subst Q.
unfold is_midpoint in *.
spliter.
apply H.
assert (Bet B Y Z).
eapply outer_transitivity_between2.
apply H0.
assumption.
assumption.
apply between_symmetry in H3.
assert (Y = P).
eapply between_egality.
apply H3.
assumption.
subst P.
apply cong_identity in H5.
subst Z.

apply cong_identity in H38.
subst Y.
unfold Col.
right;right.
apply between_symmetry.
assumption.

assert (Col Y B Z).
eapply col_transitivity_2.
apply H15.
assumption.
assumption.

assert (Y <> Q').
intro.
subst Q'.
apply cong_identity in H20.
subst Q.
absurde.

assert (Col Y Q' C').
unfold Col.
right; right.
apply between_symmetry.
assumption.

assert (Q <> Q').
intro.
subst Q'.
apply l7_3 in H10.
subst Q.
unfold OFSC, Cong_3 in *.
spliter.
apply cong_identity in H10.
subst P.
apply H.
eapply col_transitivity_1.
apply H15.
assumption.
eapply col_transitivity_1.
intro.
apply H15.
apply H10.
apply col_trivial_2.
assumption.

assert (C <> C').
intro.
subst C'.
apply l7_3 in H14.
subst X.

assert (Col Y Q' P).
eapply col_transitivity_1.
apply H26.
apply col_permutation_5.
assumption.
apply col_permutation_1.
assumption.

assert (Col C Q' P).
eapply col_transitivity_2.
apply H26.
unfold Col.
right;right.
assumption.
apply col_permutation_1.
assumption.

assert (Col Q' Y P).

apply col_permutation_4.
assumption.

assert (Col P Q Q').
eapply col_transitivity_1.
apply H22.
assumption.
apply col_permutation_3.
assumption.

assert (Col Y Q Q').
eapply col_transitivity_2.
apply H22.
assumption.
apply col_permutation_3.
assumption.

assert (Col Z Q Q').
unfold Col.
right; right.
apply between_symmetry.
assumption.

assert(Col Q Y Z).
eapply col_transitivity_1.
apply H40.
apply col_permutation_1.
assumption.
apply col_permutation_1.
assumption.

assert (Col Y P Z).
eapply col_transitivity_1.
intro.
apply H19.
apply sym_equal.
apply H47.
apply col_permutation_1.
assumption.
apply col_permutation_4.
assumption.

assert (Col Q Y C).
eapply col_transitivity_1.
apply H36.
apply col_permutation_1.
assumption.
apply col_trivial_2.

assert (Col Y Z C).
eapply col_transitivity_1.
intro.
apply H19.
apply sym_equal.
apply H49.
apply col_permutation_4.
assumption.
apply col_permutation_4.
assumption.

assert (Y <> Z).
intro.
subst Z.
unfold OFSC, Cong_3, is_midpoint in *.
spliter.
apply cong_symmetry in H54.
apply cong_identity in H54.
subst P.
absurde.
apply H.
eapply col_col.
apply H50.
apply col_permutation_1.
assumption.
apply col_permutation_5.
assumption.
assumption.

assert(OFSC Q Y C Z Q' Y C' Z).
unfold OFSC.
repeat split.
unfold OFSC, is_midpoint in *.
spliter.
eapply outer_transitivity_between.
apply between_symmetry.
apply H6.
apply between_symmetry.
assumption.
auto.
assumption.
apply cong_commutativity.
assumption.
apply cong_symmetry.
assumption.
unfold is_midpoint in H10.
spliter.
apply cong_right_commutativity.
assumption.
apply cong_reflexivity.

assert (Cong C Z C' Z).
eapply five_segments_with_def.
apply H42.
assumption.

assert (Col Z Y X).
eapply upper_dim.
apply H41.
apply cong_commutativity.
assumption.
apply cong_symmetry.
assumption.

unfold is_midpoint in H14.
spliter.
apply cong_left_commutativity.
assumption.

assert (Y <> Z).
intro.
subst Z.
unfold OFSC,Cong_3,is_midpoint in *.
spliter.
apply cong_identity in H51.
subst P.
apply cong_identity in H59.
subst Y.
absurde.

assert(C <> X).
intro.
subst X.
unfold OFSC,Cong_3,is_midpoint in *.
spliter.
apply cong_symmetry in H46.
apply cong_identity in H46.
subst C'.
absurde.

assert(X <> Y).
intro.
subst X.
unfold OFSC,Cong_3,is_midpoint in *.
spliter.
clean_duplicated_hyps.
clean_trivial_hyps.

assert (C' <> Y).
intro.
subst C'.
apply cong_identity in H47.
subst Y.
absurde.

assert (Col Y C' P ).
eapply col_transitivity_1.
apply H26.
unfold Col.
right;right.
apply between_symmetry.
assumption.
apply col_permutation_1.
assumption.

assert (P <> Q).
intro.
subst Q.
apply between_identity in H55.
subst P.
absurde.

assert (Col Y P Q').
eapply col_transitivity_2.
apply H10.
apply col_permutation_4.
assumption.
apply col_permutation_2.
assumption.

assert (Col Y Q Q').
eapply col_transitivity_2.
apply H22.
assumption.
apply col_permutation_4.
assumption.

assert (Col Q Y Z).
eapply col_transitivity_1.
apply H40.
apply col_permutation_1.
assumption.
unfold Col.
right;left.
apply between_symmetry.
assumption.

assert (Col Y Z C).
eapply col_transitivity_1.
intro.
apply H19.
apply sym_equal.
apply H53.
apply col_permutation_4.
assumption.
unfold Col.
right;right.
apply between_symmetry.
assumption.

apply H.
eapply col_col.
apply H45.
apply col_permutation_1.
assumption.
apply col_permutation_5.
assumption.
assumption.

assert (Perp_in X Y Z C X).
eapply l8_13_2.
assumption.
assumption.
apply col_permutation_3.
assumption.
apply col_trivial_3.

exists Y.
exists C.
repeat split.
apply col_trivial_1.
apply col_trivial_1.
auto.
assumption.
assumption.

assert (Col A B X).
eapply col_col.
apply H45.
apply col_permutation_1.
assumption.
apply col_permutation_5.
assumption.
apply col_permutation_4.
assumption.

exists X.
split.
assumption.

unfold Perp.
exists X.
unfold Perp_in.
repeat split.
assumption.
assumption.
apply col_permutation_2.
assumption.
apply col_trivial_3.

intros.

unfold Perp_in in H48.
spliter.
apply H55.
eapply col_col.
apply H23.

apply col_permutation_1.
assumption.
unfold Col.
right;right.
apply between_symmetry.
assumption.
assumption.
assumption.
Qed.

Lemma midpoint : forall A B C, Bet A B C -> Cong A B B C -> is_midpoint B A C.
intros.
unfold is_midpoint.
split;assumption.
Qed.

Lemma mid_bet : forall A B C, is_midpoint B A C -> Bet A B C.
unfold is_midpoint.
intros.
elim H.
intros.
assumption.
Qed.

Lemma mid_cong : forall A B C, is_midpoint B A C -> Cong A B B C.
unfold is_midpoint.
intros.
elim H.
intros.
assumption.
Qed.

Lemma mdp : forall A B, exists C, is_midpoint B A C.
intros.
prolong A B C A B.
exists C.
unfold is_midpoint.
split.
assumption.
apply cong_symmetry.
assumption.
Qed.

Ltac double A B A' :=
   assert (mp:= mdp A B);
   elim mp; intros A' ; intro; clear mp.

Lemma midpoint_id : forall A B C C', is_midpoint A B C -> is_midpoint A B C' -> C=C'.
intros.
eapply symmetric_point_unicity.
apply H.
apply H0.
Qed.

Lemma l8_20_1 : forall A B C C' D P,
  Per A B C -> is_midpoint P C' D -> is_midpoint A C' C -> is_midpoint B D C -> Per B A P.

intros.

double B A B'.
double D A D'.
double P A P'.

induction (eq_dec_points A B).
subst B.
unfold is_midpoint in H5.
spliter.
eapply l8_2.
eapply l8_5.

assert (Per B' B C).
eapply l8_3.
apply H.
assumption.
unfold Col.
left.
apply mid_bet.
assumption.

assert (Per B B' C').
eapply l8_10.
apply H7.
unfold Cong_3.
repeat split.
apply cong_pseudo_reflexivity.
eapply l7_13.
unfold is_midpoint.
split.
apply H3.
apply mid_cong.
assumption.
assumption.
eapply l7_13.
apply l7_2.
apply H3.
assumption.

assert(is_midpoint B' D' C').
eapply symmetry_preserves_midpoint.
apply H4.
apply H3.
apply l7_2.
apply H1.
assumption.

assert(is_midpoint P' C D').
eapply symmetry_preserves_midpoint.
apply H1.
apply H5.
apply H4.
assumption.

unfold Per.
exists P'.
split.
assumption.

unfold Per in H7.
ex_and H7 D''.
assert (D''= D).
eapply midpoint_id.
apply H7.
apply l7_2.
assumption.
subst D''.

unfold Per in H8.
ex_and H8 D''.

assert (D' = D'').
eapply midpoint_id.
apply l7_2.
apply H9.
assumption.
subst D''.

assert (is_midpoint P C' D).
eapply symmetry_preserves_midpoint.
apply l7_2.
apply H1.
apply l7_2.
apply H5.
apply l7_2.
apply H4.
assumption.

assert (Cong C D C' D').
eapply l7_13.
apply H1.
apply l7_2.
assumption.

assert (Cong C' D C D').
eapply l7_13.
apply l7_2.
apply H1.
apply l7_2.
assumption.

assert(Cong P D P' D').
eapply l7_13.
apply l7_2.
apply H5.
apply l7_2.
assumption.

assert (Cong P D P' C).
eapply cong_transitivity.
apply H16.
unfold is_midpoint in H10.
spliter.
apply cong_right_commutativity.
apply cong_symmetry.
assumption.

assert (IFSC C' P D B D' P' C B).
unfold IFSC.
repeat split.
apply mid_bet.
assumption.
apply mid_bet.
apply l7_2.
assumption.
apply cong_right_commutativity.
assumption.
assumption.
apply cong_commutativity.
assumption.
apply cong_right_commutativity.
apply mid_cong.
assumption.
assert (Cong P B P' B).
eapply l4_2.
apply H18.
apply cong_commutativity.
assumption.
Qed.

Lemma l8_20_2 : forall A B C C' D P,
  Per A B C -> is_midpoint P C' D -> is_midpoint A C' C -> is_midpoint B D C -> B<>C -> A<>P.
intros.
intro.
subst P.
assert (C = D).
eapply midpoint_id.
apply H1.
assumption.
subst D.
assert (B = C).
apply l7_3.
assumption.
subst C.
absurde.
Qed.

Lemma perp_col1 : forall A B C D X, A <> B -> C <> D -> C <> X -> Perp A B C D -> Col C D X -> Perp A B C X.
intros.

unfold Perp in *.
ex_and H2 P.
exists P.
unfold Perp_in in *.
spliter.
repeat split.
assumption.
assumption.
assumption.
apply col_permutation_2.
eapply col_transitivity_2.
intro.
apply H0.
apply sym_equal.
apply H8.
apply col_permutation_4.
assumption.
apply col_permutation_3.
assumption.
intros.
apply H7.
assumption.
apply col_permutation_2.
eapply col_transitivity_1.
apply H1.
apply col_permutation_5.
assumption.
apply col_permutation_1.
assumption.
Qed.

Lemma l8_21_aux : forall A B C,
 A<> B -> ~ Col A B C -> exists P, exists T, Perp A B P A /\ Col A B T /\ Bet C T P.
intros.
assert (exists X : Tpoint, Col A B X /\ Perp A B C X).
eapply l8_18_existence.
assumption.
ex_and H1 X.

assert (Perp_in X A B C X).
eapply l8_15_1;
assumption.

assert (Per A X C).
unfold Perp_in in H3.
spliter.
apply H7.
apply col_trivial_1.
apply col_trivial_1.

assert(HH:= H4).
unfold Per in H4.
ex_and H4 C'.

double C A C''.
assert (exists P, is_midpoint P C' C'').
eapply l7_25.
unfold is_midpoint in *.
spliter.
eapply cong_transitivity.
apply cong_symmetry.
apply H5.
apply cong_left_commutativity.
assumption;
spliter.
ex_elim H7 P.

assert (Per X A P).
eapply l8_20_1.
apply HH.
apply l7_2.
apply H8.
apply l7_2.
apply H6.
apply l7_2.
assumption.

assert (X <> C).
intro.
subst C.
apply H0.
assumption.

assert (A <> P).
eapply l8_20_2.
apply HH.
apply l7_2.
apply H8.
apply l7_2.
assumption.
apply l7_2.
assumption.
assumption.

assert (exists T, Bet P T C /\ Bet A T X).
eapply l3_17.
apply mid_bet.
apply l7_2.
apply H6.
apply mid_bet.
apply l7_2.
apply H4.
apply mid_bet.
apply l7_2.
apply H8.
ex_and H11 T.

induction (eq_dec_points A X).
subst X.
exists P.
exists T.
apply between_identity in H12.
subst T.
assert (C'= C'').
eapply midpoint_id.
apply H4.
assumption.
subst C''.
apply l7_3 in H8.
subst P.

assert (Col A C C').
unfold is_midpoint in H6.
spliter.
unfold Col.
right;right.
assumption.

repeat split.
eapply perp_col0.
apply perp_sym.
apply H2.
auto.
unfold Col.
left.
apply between_symmetry.
assumption.
apply col_trivial_2.
apply col_trivial_3.
apply between_symmetry.
assumption.

exists P.
exists T.

repeat split.
unfold Perp.
exists A.

unfold Perp_in.
repeat split.
assumption.
auto.
apply col_trivial_1.
apply col_trivial_3.

unfold Perp_in in H3.
spliter.
intros.
eapply per_col in H7.
apply l8_2 in H7.

eapply per_col in H7.
eapply l8_2 in H7.
apply H7.
assumption.
eapply col_transitivity_1.
apply H.
assumption.
apply col_permutation_1.
assumption.
assumption.
apply col_permutation_3.
assumption.
eapply col_transitivity_1.
apply H13.
apply col_permutation_5.
assumption.
unfold Col.
right; left.
apply between_symmetry.
assumption.
apply between_symmetry.
assumption.
Qed.

Lemma l8_21 : forall A B C,
 A<> B -> exists P, exists T, Perp A B P A /\ Col A B T /\ Bet C T P.
intros.
induction(classic(Col A B C)).
assert (exists C', ~ Col A B C').
eapply l6_25.
assumption.
ex_elim H1 C'.
assert ( exists P : Tpoint,
         (exists T : Tpoint, Perp A B P A /\ Col A B T /\ Bet C' T P)).
eapply l8_21_aux.
assumption.
assumption.
ex_elim H1 P.
ex_and H3 T.
exists P.
exists C.
repeat split.
assumption.
assumption.

apply between_trivial2.
eapply l8_21_aux.
assumption.
assumption.
Qed.

Lemma perp_in_sym : forall A B C D X, Perp_in X A B C D -> Perp_in X C D A B.
unfold Perp_in.
intros.
spliter.
repeat split.
assumption.
assumption.
assumption.
assumption.
intros.
apply l8_2.
apply H3.
assumption.
assumption.
Qed.

Lemma perp_in_left_comm : forall A B C D X, Perp_in X A B C D -> Perp_in X B A C D.
Proof.
unfold Perp_in.
intuition.
Qed.

Lemma perp_in_right_comm : forall A B C D X, Perp_in X A B C D -> Perp_in X A B D C.
Proof.
intros.
apply perp_in_sym.
apply perp_in_left_comm.
apply perp_in_sym.
assumption.
Qed.

Lemma perp_in_comm : forall A B C D X, Perp_in X A B C D -> Perp_in X B A D C.
Proof.
intros.
apply perp_in_left_comm.
apply perp_in_right_comm.
assumption.
Qed.

Lemma perp_in_col : forall A B C D X, Perp_in X A B C D -> Col A B X /\ Col C D X.
Proof.
unfold Perp_in.
intuition.
Qed.

Lemma perp_perp_in : forall A B C, Perp A B C A -> Perp_in A A B C A.
Proof.
intros.
apply l8_15_1.

unfold Perp in H.
ex_and H X.
unfold Perp_in in H0.
intuition.

apply col_trivial_3.
assumption.
Qed.

Lemma perp_id : forall A B C, A <> B -> Perp A B C A -> Perp_in A A B C A.
Proof.
intros.
apply l8_15_1.
assumption.
apply col_trivial_3.
unfold Perp_in.
assumption.
Qed.

Lemma perp_per_1 : forall A B C, A<>B -> Perp A B C A -> Per B A C.
Proof.
intros.
assert (Perp_in A A B C A).
apply perp_perp_in.
assumption.
unfold Perp_in in H1.
spliter.
apply H5.
apply col_trivial_3.
apply col_trivial_1.
Qed.

Lemma perp_per_2 : forall A B C, A<>B -> Perp A B A C -> Per B A C.
Proof.
intros.
apply perp_right_comm in H0.
apply perp_per_1;
assumption.
Qed.

Lemma perp_col : forall A B C D E, A<>E -> Perp A B C D -> Col A B E -> Perp A E C D.
Proof.
intros.
apply perp_sym.
eapply perp_col0.
apply H0.
assumption.
apply col_trivial_3.
assumption.
Qed.

Lemma perp_not_eq_1 : forall A B C D, Perp A B C D -> A<>B.
Proof.
intros.
unfold Perp in H.
ex_elim H X.
unfold Perp_in in H0.
tauto.
Qed.

Lemma perp_not_eq_2 : forall A B C D, Perp A B C D -> C<>D.
Proof.
intros.
apply perp_sym in H.
eapply perp_not_eq_1.
apply H.
Qed.

Lemma le_bet : forall A B C D, le C D A B -> exists X, Bet A X B /\ Cong A X C D.
Proof.
intros.
unfold le in H.
ex_and H Y.
exists Y;Cong.
Qed.

Lemma perp_distinct : forall A B C D, Perp A B C D -> A <> B /\ C <> D.
Proof.
intros.
unfold Perp in H.
ex_elim H X.
unfold Perp_in in H0.
tauto.
Qed.

Lemma bet_cong3 : forall A B C A' B', Bet A B C -> Cong A B A' B' -> exists C', Cong_3 A B C A' B' C'.
Proof.
unfold Col.
intros.
assert (exists x, Bet A' B' x /\ Cong B' x B C)
 by (apply segment_construction).
ex_and H1 x.
assert (Cong A C A' x).
eapply l2_l1.
apply H.
apply H1.
assumption.
Cong.
exists x;unfold Cong_3;Cong.
Qed.

Lemma diff_per_diff : forall A B P R ,
      A <> B -> Cong A P B R -> Per B A P -> Per A B R -> P <> R.
Proof.
intros.
intro.
subst.
assert (A = B).
eapply l8_7.
apply l8_2.
apply H1.
apply l8_2.
assumption.
intuition.
Qed.

Lemma per_not_colp : forall A B P R, A <> B -> A <> P -> B <> R -> Per B A P -> Per A B R -> ~Col P A R.
Proof.
intros.
intro.
assert (Perp A B P A).
apply perp_comm.
apply per_perp.
auto.
assumption.
assumption.
assert (Perp A B B R).
apply per_perp.
assumption.
assumption.
assumption.
assert (Per B A R).
eapply per_col.
apply H0.
assumption.
auto with Col.
apply l8_2 in H3.
apply l8_2 in H7.
assert (A = B).
eapply l8_7.
apply H7.
assumption.
contradiction.
Qed.

Lemma per_per_col : forall A B C X, Per A X C -> X <> C -> Per B X C -> Col A B X.
Proof.
intros.
unfold Per in *.
ex_and H C'.
ex_and H1 C''.
assert (C' = C'').
eapply midpoint_id.
apply H.
apply H1.
subst C''.
eapply upper_dim.
2:apply H2.
intro.
subst C'.
apply l7_3 in H1.
apply H0.
assumption.
assumption.
unfold is_midpoint in H.
spliter.
Cong.
Qed.

Lemma per_not_col : forall A B C, A <> B -> B <> C -> Per A B C -> ~Col A B C.
Proof.
intros.
intro.
unfold Per in H1.
ex_and H1 C'.
assert (C = C' \/ is_midpoint A C C').
eapply l7_20.
eapply col_transitivity_1.
intro.
apply H0.
apply sym_equal.
apply H4.
auto with Col.
unfold Col.
left.
apply mid_bet.
assumption.
assumption.
induction H4.
subst C'.
apply l7_3 in H1.
apply H0.
assumption.
apply H.
eapply l7_17.
apply H4.
assumption.
Qed.

Lemma per_cong : forall A B P R X ,
 A <> B -> A <> P ->
 Per B A P -> Per A B R ->
 Cong A P B R -> Col A B X -> Bet P X R ->
 Cong A R P B.
Proof.
intros.

assert (Per P A B).
apply l8_2.
assumption.
double B R Q.

assert (B <> R).
intro.
subst R.
apply cong_identity in H3.
subst P.
absurde.

assert (Per A B Q).
eapply per_col.
apply H8.
assumption.
unfold Col.
left.
apply mid_bet.
assumption.

assert (Per P A X).
eapply per_col.
apply H.
assumption.
assumption.

assert (B <> Q).
intro.
subst Q.
apply l7_3 in H7.
subst R.
absurde.

assert (Per R B X).
eapply per_col.
intro.
apply H.
apply sym_equal.
apply H12.
apply l8_2.
assumption.
apply col_permutation_4.
assumption.

assert (X <> A).
intro.
subst X.
assert (~Col P A R).
eapply per_not_colp.
apply H.
assumption.
assumption.
assumption.
assumption.
apply H13.
unfold Col.
left.
assumption.

double P A P'.
prolong P' X R' X R.
assert (exists M, is_midpoint M R R').
eapply l7_25.
apply cong_symmetry.
apply H16.
ex_elim H17 M.

assert (Per X M R).
unfold Per.
exists R'.
split.
assumption.
apply cong_symmetry.
assumption.
assert (Cong X P X P').
apply l8_2 in H10.
unfold Per in H10.
ex_and H10 P''.
assert (P'=P'').
eapply midpoint_id.
apply H14.
apply H10.
subst P''.
assumption.

assert (X <> P').
intro.
subst P'.
apply cong_identity in H19.
subst X.
apply l7_3 in H14.
subst P.
absurde.

assert (P <> P').
intro.
subst P'.
eapply l7_3 in H14.
subst P.
absurde.

assert(~Col X P P').
intro.
assert(Col X P A).
eapply col_col.
apply H21.
apply col_permutation_1.
assumption.
apply col_trivial_3.
unfold Col.
right;left.
apply between_symmetry.
apply mid_bet.
assumption.
apply col_permutation_1 in H23.
assert (P = A \/ X = A).
eapply l8_9.
assumption.
assumption.
induction H24.
subst P.
absurde.
apply H13.
assumption.

assert (Bet A X M).
eapply l7_22.
5:apply H14.
5:apply H18.
assumption.
assumption.
assumption.
apply cong_symmetry.
assumption.

assert (X <> R).
intro.
subst X.
apply cong_identity in H16.
subst R'.

apply l7_3 in H18.
subst M.

assert (Col B R A).
eapply (per_per_col).
apply l8_2.
apply H6.
assumption.
apply l8_2.
assumption.
assert (~Col A B R).
eapply per_not_col.
assumption.
assumption.
assumption.
apply H18.
apply col_permutation_2.
assumption.

assert (X <> R').
intro.
subst R'.
apply cong_symmetry in H16.
apply cong_identity in H16.
apply H24.
assumption.

assert (M <> X).
intro.
subst M.
apply H22.
eapply col_transitivity_1.
apply H24.
unfold Col.
right; right.
assumption.
eapply col_transitivity_1.
apply H25.
unfold Col.
right;right.
apply mid_bet.
assumption.
unfold Col.
right; right.
assumption.

assert (M = B).
eapply (l8_18_unicity A X R).
intro.
assert (Col A B R).
eapply col_transitivity_1.
intro.
apply H13.
apply sym_equal.
apply H28.
apply col_permutation_5.
assumption.
assumption.
eapply per_not_col.
apply H;

apply H12.
apply H8.
assumption.
assumption.
unfold Col.
left.
assumption;
eapply col_transitivity_1.

apply per_perp in H17.
apply perp_comm.
eapply perp_col.
assumption.
apply H17.
unfold Col.
right;right.
assumption.
auto.
intro.
subst M.
apply (midpoint_id R R R R') in H18.
subst R'.
apply H22.
eapply col_transitivity_1.
apply H25.
unfold Col.
right;right.
assumption.
unfold Col.
right; right.
assumption.
eapply l7_3_2.
apply col_permutation_5.
assumption.

apply per_perp in H10.
apply perp_comm.
eapply perp_col.
apply H13.
apply perp_comm.
eapply perp_col.
intro.
apply H13.
apply sym_equal.
apply H27.
apply perp_right_comm.
apply per_perp in H2.
apply H2.
assumption.
assumption.
assumption.
apply col_trivial_2.
auto.
intro.
apply H13.
subst X.
reflexivity.
subst M.

assert(OFSC P X R P' P' X R' P).
unfold OFSC.
repeat split.

assumption.
assumption.
apply cong_commutativity.
assumption.
apply cong_symmetry.
assumption.
apply cong_pseudo_reflexivity.
apply cong_symmetry.
assumption.
assert (Cong R P' R' P).
eapply five_segments_with_def.
apply H27.

intro.
subst X.
apply H22.
apply col_trivial_1.

assert (IFSC P' A P R R' B R P).
unfold IFSC.
repeat split.
apply between_symmetry.
apply mid_bet.
assumption.
apply between_symmetry.
apply mid_bet.
assumption.
eapply l2_l1.
apply between_symmetry.
apply mid_bet.
apply H14.
apply between_symmetry.
apply mid_bet.
apply H18.
eapply cong_transitivity.

apply mid_cong.
apply l7_2.
apply H14.
eapply cong_transitivity.
apply H3.

apply cong_commutativity.
apply mid_cong.
assumption.
assumption.
assumption.
apply cong_left_commutativity.
assumption.
apply cong_pseudo_reflexivity.

eapply cong_right_commutativity.
eapply l4_2.
eapply H29.
Qed.

Lemma perp_cong : forall A B P R X , A <> B -> A <> P -> Perp A B P A -> Perp A B R B ->
                                       Cong A P B R -> Col A B X -> Bet P X R -> Cong A R P B.
Proof.
intros.
apply (per_cong A B P R X).
assumption.
assumption.
eapply perp_per_1.
assumption.
assumption.
eapply perp_per_1.
auto.
apply perp_left_comm.
assumption.
assumption.
assumption.
assumption.
Qed.

Lemma midpoint_existence_aux : forall A B P Q T,
  A<>B -> Perp A B Q B -> Perp A B P A -> Col A B T -> Bet Q T P -> le A P B Q -> exists X : Tpoint, is_midpoint X A B.
Proof.
intros.
unfold le in H4.
ex_and H4 R.
assert (exists X, Bet T X B /\ Bet R X P).
eapply inner_pasch.
apply between_symmetry.
apply H3.
auto.
ex_and H6 X.
assert (Col A B X).
induction (eq_dec_points T B).
subst T.
apply between_identity in H6.
subst X.
apply col_trivial_2.

assert (Col B A X).
eapply col_transitivity_2.
apply H8.
apply col_permutation_3.
assumption.
apply col_permutation_5.
unfold Col.
left; assumption.
apply col_permutation_4.
assumption.

induction(classic (Col A B P)).

assert (B=A \/ P=A).
eapply l8_9.
apply perp_per_1.
assumption.
assumption.
apply col_permutation_4.
assumption.
induction H10.
exists A.
subst B.
eapply l7_3_2.
subst P.
apply cong_symmetry in H5.
apply cong_identity in H5.
subst R.
apply perp_distinct in H1.
spliter.
absurde.

assert (B <> R).
intro.
subst R.
apply cong_identity in H5.
subst P.
apply H9.
apply col_trivial_3.

assert (~Col A B Q).
intro.
assert (A=B \/ Q=B).
eapply l8_9.
apply perp_per_2.
auto.
apply perp_comm.
assumption.
assumption.
induction H12.
apply H.
assumption.
subst Q.
apply between_identity in H4.
contradiction.

assert (~Col A B R).
intro.
assert (Col B A Q).
eapply col_transitivity_1.
apply H10.
apply col_permutation_1.
assumption.
unfold Col.
left.
assumption.
apply H11.
apply col_permutation_4.
assumption.

assert (P <> R).
intro.
subst R.
apply between_identity in H7.
subst X.
apply H12.
assumption.

induction (eq_dec_points A P).
subst P.
apply perp_distinct in H1.
spliter.
absurde.
assert (Perp A B R B).
eapply perp_col.
assumption.
apply perp_sym.
apply perp_left_comm.
eapply perp_col.
assumption.
apply perp_left_comm.
apply perp_sym.
apply H0.
unfold Col.
right; left.
apply between_symmetry.
assumption.
apply col_trivial_2.
apply between_symmetry in H7.

assert (Cong A R P B).
apply (perp_cong A B P R X);
assumption.

assert (is_midpoint X A B /\ is_midpoint X P R).
apply (l7_21 A P B R X).
intro.
apply H9.
apply col_permutation_5.
assumption.
assumption.
assumption.
intros.
apply cong_commutativity.
apply cong_symmetry.
apply cong_right_commutativity.
assumption.
apply col_permutation_5.
assumption.
unfold Col.
left.
assumption.
spliter.
exists X.
assumption.
Qed.

Lemma midpoint_existence : forall A B, exists X, is_midpoint X A B.
Proof.
intros.
induction (eq_dec_points A B).
subst B.
exists A.
apply l7_3_2.

cut(exists Q, Perp A B B Q).
intro.
ex_elim H0 Q.
cut(exists P, exists T, Perp A B P A /\ Col A B T /\ Bet Q T P).
intros.
ex_elim H0 P.
ex_and H2 T.

assert (le A P B Q \/ le B Q A P).
apply le_cases.

induction H4.
eapply midpoint_existence_aux.
assumption.
apply perp_right_comm.
apply H1.
apply H0.
apply H2.
assumption.
assumption.

assert (exists X : Tpoint, is_midpoint X B A).
eapply (midpoint_existence_aux B A Q P T).
auto.
apply perp_left_comm.
assumption.
apply perp_comm.
assumption.
apply col_permutation_4.
assumption.
apply between_symmetry.
assumption.
assumption.
ex_elim H5 X.
exists X.
apply l7_2.
assumption.

eapply l8_21.
assumption.
assert (exists P : Tpoint,
         (exists T : Tpoint, Perp B A P B /\ Col B A T /\ Bet A T P)).
apply (l8_21 B A);auto.
ex_elim H0 P.
ex_elim H1 T.
spliter.
exists P.
apply perp_comm.
assumption.
Qed.

Lemma perp_in_id : forall A B C X, Perp_in X A B C A -> X = A.
intros.
assert (Perp A B C A).
unfold Perp.
exists X.
assumption.

assert (A <> B /\ C <> A).
apply perp_distinct.
assumption.
spliter.

assert (HH:=H0).
apply perp_perp_in in HH.

assert (l8_16_1:=l8_16_1 A B C B A).

assert (~Col A B C /\ Per C A B).
apply l8_16_1.
assumption.
apply col_trivial_3.
apply col_trivial_2.
auto.
assumption.
spliter.
unfold Perp_in in H.
spliter.

eapply l8_18_unicity.
apply H3.

apply col_permutation_1.
assumption.
apply perp_sym.
eapply perp_col.
intro.
subst X.
assert (~Col C A B).
apply per_not_col.
assumption.
assumption.
assumption.
apply H9.
assumption.
apply perp_sym.
apply H0.
apply col_permutation_1.
assumption.
apply col_trivial_3.
assumption.
Qed.

Lemma l8_22 : forall A B P R X , A <> B -> A <> P -> Per B A P -> Per A B R ->
                                       Cong A P B R -> Col A B X -> Bet P X R -> Cong A R P B /\ is_midpoint X A B /\ is_midpoint X P R.
intros.
assert (Cong A R P B).
apply (per_cong A B P R X);
assumption.
split.
assumption.
assert (~ Col B A P).
eapply per_not_col.
auto.
assumption.
assumption.

apply l7_21.
intro.
apply H7.
apply col_permutation_2.
assumption.

intro.
subst R.
eapply between_identity in H5.
subst X.
apply H7.
apply col_permutation_4.
assumption.
assumption.
apply cong_right_commutativity.
apply cong_symmetry.
assumption.
apply col_permutation_5.
assumption.
unfold Col.
left.
assumption.
Qed.

Lemma l8_22_bis : forall A B P R X , A <> B -> A <> P -> Perp A B P A -> Perp A B R B ->
                                       Cong A P B R -> Col A B X -> Bet P X R -> Cong A R P B /\ is_midpoint X A B /\ is_midpoint X P R.
intros.

apply l8_22.
assumption.
assumption.
apply perp_per_1.
assumption.
assumption.
apply perp_per_1.
auto.
apply perp_left_comm.
assumption.
assumption.
assumption.
assumption.
Qed.

Lemma perp_in_perp : forall A B C D X, Perp_in X A B C D -> Perp A B C D.
intros.
unfold Perp.
exists X.
assumption.
Qed.

Lemma perp_proj : forall A B C D, Perp A B C D -> ~Col A C D -> exists X, Col A B X /\ Perp A X C D.
intros.
unfold Perp in H.
ex_and H X.
exists X.
split.
unfold Perp_in in H1.
spliter.

apply col_permutation_1.
assumption.
eapply perp_col.
intro.
subst X.
unfold Perp_in in H1.
spliter.
apply H0.
assumption.
apply perp_in_perp in H1.
apply H1.
unfold Perp_in in H1.
spliter.
apply col_permutation_1.
assumption.
Qed.

Lemma l8_24 : forall A B P Q R T, Perp P A A B -> Perp Q B A B -> Col A B T -> Bet P T Q
    -> Bet B R Q -> Cong A P B R -> exists X, is_midpoint X A B /\ is_midpoint X P R.
intros.
unfold le in H4.
assert (exists X, Bet T X B /\ Bet R X P).
eapply inner_pasch.
apply H2.
assumption.
ex_and H5 X.
assert (Col A B X).
induction (eq_dec_points T B).
subst T.
apply between_identity in H5.
subst X.
apply col_trivial_2.

assert (Col T X B).
unfold Col.
left.
assumption.

apply col_permutation_4.

eapply col_transitivity_1.
intro.
apply H7.
apply sym_equal.
apply H9.
apply col_permutation_1.
assumption.
apply col_permutation_2.
assumption.

assert (A <> B).
apply perp_distinct in H.
spliter.
assumption.

assert (A <> P).
apply perp_distinct in H.
spliter.
auto.

induction(classic (Col A B P)).

assert (B=A \/ P=A).
eapply l8_9.
apply perp_per_1.
assumption.
apply perp_sym.
assumption.
apply col_permutation_4.
assumption.

induction H11.
exists A.
subst B.
absurde.
subst P.
absurde.

assert (B <> R).
intro.
subst R.
apply cong_identity in H4.
subst P.
absurde.

assert (Q <> B).
apply perp_distinct in H0.
spliter.
assumption.

assert (~Col A B Q).
intro.
assert (A=B \/ Q=B).
eapply l8_9.
apply perp_per_2.
auto.
apply perp_comm.
apply perp_sym.
assumption.
assumption.
induction H14.
contradiction.
subst Q.
absurde.

assert (~Col A B R).
intro.
assert (Col B A Q).
eapply col_transitivity_1.
apply H11.
apply col_permutation_1.
assumption.
unfold Col.
left.
assumption.
apply H13.
apply col_permutation_4.
assumption.

assert (P <> R).
intro.
subst R.
apply between_identity in H6.
subst X.
contradiction.

induction (eq_dec_points A P).
subst P.
apply perp_distinct in H.
spliter.
absurde.

assert (Perp A B R B).
eapply perp_col.
assumption.
apply perp_sym.
apply perp_left_comm.
eapply perp_col.
assumption.
apply perp_left_comm.
apply H0.
unfold Col.
right; left.
apply between_symmetry.
assumption.
apply col_trivial_2.

assert (Cong A R P B).
apply (perp_cong A B P R X).

assumption.
assumption.
apply perp_sym.
assumption.
assumption.
assumption.
assumption.
apply between_symmetry.
assumption.

intros.

assert (is_midpoint X A B /\ is_midpoint X P R).
apply (l7_21 A P B R X).
intro.
apply H10.
apply col_permutation_5.
assumption.
assumption.
assumption.
apply cong_right_commutativity.
apply cong_symmetry.
assumption.
apply col_permutation_5.
assumption.
unfold Col.
left.
apply between_symmetry.
assumption.
exists X.
assumption.
Qed.

End T8.