Library parallel

Require Export angles.

Section T12.

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
   | H:(le ?X1 ?X2 ?X3 ?X3) |- _ => apply le_zero in H; smart_subst X2
   | H:(is_midpoint ?A ?A ?B) |- _ => apply is_midpoint_id in H; smart_subst A
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.

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


Definition coplanar := fun A B C D: Tpoint => True.

Definition Par_strict := fun A B C D =>
  A<>B /\ C<>D /\ coplanar A B C D /\ ~ exists X, Col X A B /\ Col X C D.

Definition Par := fun A B C D =>
  Par_strict A B C D \/ (A<>B /\ C<>D /\ Col A C D /\ Col B C D).

Lemma par_reflexivity : forall A B, A<>B -> Par A B A B.
Proof.
intros.
unfold Par.
unfold Par_strict.
right.
repeat split.
assumption.
assumption.
apply col_trivial_1.
apply col_trivial_3.
Qed.

Lemma par_strict_irreflexivity : forall A B, ~ Par_strict A B A B.
Proof.
intros.
intro.
unfold Par_strict in H.
spliter.
apply H2.
exists A.
split; apply col_trivial_1.
Qed.

Lemma par_strict_symmetry :forall A B C D, Par_strict A B C D -> Par_strict C D A B.
Proof.
unfold Par_strict.
intros.
spliter.
repeat split.
assumption.
assumption.
intro.
apply H2.
ex_and H3 X.
exists X.
split; assumption.
Qed.

Lemma parallel_symmetry :forall A B C D, Par A B C D -> Par C D A B.
Proof.
unfold Par.
intros.
induction H.
left.
apply par_strict_symmetry.
assumption.
spliter.
right.
repeat split;try assumption.
eapply (col_transitivity_1 _ D).
assumption.
Col.
Col.
eapply (col_transitivity_1 _ C).
auto.
Col.
Col.
Qed.

Lemma parallel_left_comm : forall A B C D, Par A B C D -> Par B A C D.
unfold Par.
intros.
induction H.
left.
unfold Par_strict in *.
spliter.
repeat split.
auto.
assumption.
intro.
apply H2.
ex_and H3 X.
exists X.
split; Col.
right.
spliter.
repeat split.
auto.
assumption.
Col.
Col.
Qed.

Lemma parallel_right_comm : forall A B C D, Par A B C D -> Par A B D C.
intros.
apply parallel_symmetry in H.
apply parallel_symmetry.
apply parallel_left_comm.
assumption.
Qed.

Lemma parallel_comm : forall A B C D, Par A B C D -> Par B A D C.
intros.
apply parallel_left_comm.
apply parallel_right_comm.
assumption.
Qed.

Lemma l12_6 : forall A B C D, Par_strict A B C D -> one_side A B C D.
intros.
unfold Par_strict in H.
spliter.
assert(HH:= not_two_sides_one_side A B C D H).

apply HH.

intro.
apply H2.
exists C.
split.
Col.
apply col_trivial_1.

intro.
apply H2.
exists D.
split.
Col.
apply col_trivial_3.
intro.
apply H2.
unfold two_sides in H3.
spliter.
ex_and H6 T.
exists T.
apply bet_col in H7.
split; Col.
Qed.

Lemma perp_perp_col : forall X Y Z A B, Perp X Y A B -> Perp X Z A B -> Col X Y Z.
intros.
induction(classic(Col A B X)).
induction(eq_dec_points X A).
subst A.
assert(X <> B).
apply perp_distinct in H.
spliter.
assumption.

apply perp_right_comm in H.
apply perp_perp_in in H.
apply perp_in_comm in H.
apply perp_in_per in H.

apply perp_right_comm in H0.
apply perp_perp_in in H0.
apply perp_in_comm in H0.
apply perp_in_per in H0.
apply col_permutation_2.

eapply (per_per_col).
apply H.
assumption.
assumption.

assert(Perp A X X Y ).
eapply perp_col.
auto.
apply perp_sym.
apply H.
assumption.

assert(Perp A X X Z).
eapply perp_col.
auto.
apply perp_sym.
apply H0.
assumption.

apply col_permutation_2.

eapply (per_per_col _ _ A).
apply perp_in_per.
apply perp_in_comm.
apply perp_perp_in.
apply perp_sym.
eapply perp_col.
auto.
apply perp_sym.
apply H.
assumption.
assumption.
apply perp_in_per.
apply perp_in_comm.
apply perp_perp_in.
apply perp_sym.
eapply perp_col.
auto.
apply perp_sym.
apply H0.
assumption.

assert(HH0:=H).
assert(HH1:=H0).
unfold Perp in H.
unfold Perp in H0.
ex_and H Y0.
ex_and H0 Z0.

assert(HH2:=H).
assert(HH3:=H2).

apply perp_in_col in H.
apply perp_in_col in H2.
spliter.

assert(Perp X Y0 A B).
eapply perp_col.
intro.
subst Y0.
contradiction.
apply HH0.
assumption.

assert(Perp X Z0 A B).
eapply perp_col.
intro.
subst Z0.
contradiction.
apply HH1.
assumption.

assert(Y0 = Z0).
eapply l8_18_unicity.
apply H1.
assumption.
apply perp_sym.
assumption.
assumption.
apply perp_sym.
assumption.
subst Z0.
eapply (col_transitivity_1 _ Y0).
intro.
subst Y0.
contradiction.
Col.
Col.
Qed.

Lemma perp_perp_col_col : forall X1 X2 Y1 Y2 A B, Perp X1 X2 A B -> Perp Y1 Y2 A B -> Col X1 Y1 Y2 -> Col X2 Y1 Y2.
intros.
assert(HH0:= H).
assert(HH1:= H0).
unfold Perp in HH0.
unfold Perp in HH1.
ex_and HH0 X0.
ex_and HH1 Y0.

induction(eq_dec_points X1 Y2).
subst Y2.

assert(Perp Y1 X1 A B).
eapply perp_col.
intro.

subst Y1.
apply perp_distinct in H0.
spliter.
absurde.
apply H0.
apply col_trivial_2.
apply col_permutation_1.
eapply perp_perp_col.
apply H.
apply perp_left_comm.
assumption.

assert(Perp Y2 X1 A B).
eapply perp_col.
auto.
apply perp_left_comm.
apply H0.
Col.
assert(Perp X1 Y2 A B).
eapply perp_left_comm.
assumption.

induction(eq_dec_points X1 Y1).
subst Y1.
apply col_permutation_2.
eapply perp_perp_col.
apply H6.
assumption.

assert(Perp X1 Y1 A B).
eapply perp_col.
assumption.
apply perp_left_comm.
apply H5.
Col.

induction (eq_dec_points X2 Y1).
subst Y1.
apply col_trivial_1.

assert(Perp X2 Y1 A B).
eapply perp_col.
assumption.
apply perp_left_comm.
apply H.
apply col_permutation_2.
eapply perp_perp_col.
apply H8.
assumption.


induction (eq_dec_points X2 Y2).
subst Y2.
apply col_trivial_3.

assert(Perp Y2 X2 A B).
eapply perp_col.
auto.
apply H5.
apply col_permutation_2.
eapply perp_perp_col.
apply H.
apply perp_left_comm.
assumption.

eapply perp_perp_col.
apply H10.
apply perp_left_comm.
assumption.
Qed.

Lemma l12_9 : forall A1 A2 B1 B2 C1 C2, coplanar A1 A2 B1 B2 -> Perp A1 A2 C1 C2 -> Perp B1 B2 C1 C2 -> Par A1 A2 B1 B2.
Proof.
intros.
unfold Par.
unfold Par_strict.
assert(A1 <> A2 /\ C1 <> C2).
apply perp_distinct.
assumption.
assert(B1 <> B2 /\ C1 <> C2).
apply perp_distinct.
assumption.
spliter.

induction(classic(Col A1 B1 B2)).
right.
repeat split; try assumption.

eapply perp_perp_col_col.
apply H0.
apply H1.
assumption.

left.
repeat split.
assumption.
assumption.
intro.
ex_and H7 AB.
apply H6.

induction(eq_dec_points AB A1).
subst AB.
assumption.

assert(Perp A1 AB C1 C2).
eapply perp_col.
auto.
apply H0.
Col.

eapply perp_perp_col_col.
apply perp_left_comm.
apply H10.
assumption.
assumption.
Qed.

Lemma parallel_existence : forall A B P, A <> B -> exists C, exists D, C<>D /\ Par A B C D /\ Col P C D.
Proof.
intros.
induction(classic(Col A B P)).
exists A.
exists B.
repeat split.
assumption.
apply par_reflexivity.
assumption.
Col.

assert(exists P', Col A B P' /\ Perp A B P P').
eapply l8_18_existence.
assumption.
ex_and H1 P'.

assert(P <> P').
intro.
subst P'.
contradiction.

induction(eq_dec_points P' A).
subst P'.

assert(exists Q, Per Q P A /\ Cong Q P A B /\ one_side A P Q B).
eapply ex_per_cong.
auto.
assumption.
apply col_trivial_2.
intro.
apply H0.
Col.
ex_and H4 Q.

exists P.
exists Q.
assert(P <> Q).
intro.
subst Q.
apply cong_symmetry in H5.
apply cong_identity in H5.
contradiction.

repeat split.
assumption.
eapply l12_9.
apply I.
apply H2.

apply per_perp_in in H4.
apply perp_in_perp in H4.
induction H4.
apply perp_distinct in H4.
spliter.
absurde.
apply perp_left_comm.
assumption.
auto.
assumption.
apply col_trivial_1.

assert(exists Q, Per Q P P' /\ Cong Q P A B /\ one_side P' P Q A).
eapply ex_per_cong.
auto.
assumption.
apply col_trivial_2.
intro.
apply H0.
eapply (col_transitivity_1 _ P').
auto.
Col.
Col.
ex_and H5 Q.
exists P.
exists Q.

assert(P <> Q).
intro.
subst Q.
apply cong_symmetry in H6.
apply cong_identity in H6.
contradiction.

repeat split.
assumption.
eapply l12_9.
apply I.
apply H2.
apply per_perp_in in H5.
apply perp_in_perp in H5.
induction H5.
apply perp_distinct in H5.
spliter.
absurde.
apply perp_left_comm.
assumption.
auto.
assumption.
apply col_trivial_1.
Qed.

Lemma par_not_col : forall A B C D X, Par_strict A B C D -> Col X A B -> ~Col X C D.
intros.
unfold Par_strict in H.
spliter.
intro.
apply H3.
exists X.
split; assumption.
Qed.

Lemma not_diff_eq : forall A B : Tpoint, ~ A <> B -> A = B.
intros.
induction(classic (A = B)).
assumption.
contradiction.
Qed.

Lemma not_not : forall P : Prop, ~~P -> P.
intros.
induction(classic P).
assumption.
contradiction.
Qed.

Lemma not_par_strict_inter_exists : forall A1 B1 A2 B2, ~Par_strict A1 B1 A2 B2 -> exists X, Col A1 B1 X /\ Col A2 B2 X.
intros.
unfold Par_strict in H.
apply not_and in H.
induction H.
exists A2.
apply not_diff_eq in H.
subst B1.
split.
apply col_trivial_1.
apply col_trivial_3.
apply not_and in H.
induction H.
apply not_diff_eq in H.
subst B2.
exists A1.
split.
apply col_trivial_3.
apply col_trivial_1.
apply not_and in H.
induction H.
apply False_ind.
apply H.
unfold coplanar.
apply I.
apply not_not in H.
ex_and H X.
exists X.
split.
Col.
Col.
Qed.

Lemma not_par_inter_exists : forall A1 B1 A2 B2, ~Par A1 B1 A2 B2 -> exists X, Col A1 B1 X /\ Col A2 B2 X.
intros.
unfold Par in H.
apply not_or in H.
spliter.
apply not_par_strict_inter_exists.
assumption.
Qed.

Lemma not_strict_par1 : forall A B C D X, Par A B C D -> Col A B X -> Col C D X -> Col A B C.
intros.
unfold Par in H.
induction H.
unfold Par_strict in H.
spliter.
assert(exists X, Col X A B /\ Col X C D).
exists X.
split; Col.
contradiction.
spliter.
apply col_permutation_1.
eapply col_transitivity_1.
apply H2.
Col.
Col.
Qed.

Lemma not_strict_par2 : forall A B C D X, Par A B C D -> Col A B X -> Col C D X -> Col A B D.
intros.
eapply not_strict_par1.
apply parallel_right_comm.
apply H.
apply H0.
Col.
Qed.

Lemma not_strict_par : forall A B C D X, Par A B C D -> Col A B X -> Col C D X -> Col A B C /\ Col A B D.
intros.
split.

eapply not_strict_par1.
apply H.
apply H0.
assumption.
eapply not_strict_par2.
apply H.
apply H0.
assumption.
Qed.

Lemma not_par_not_col : forall A B C, A <> B -> A <> C -> ~Par A B A C -> ~Col A B C.
intros.
intro.
apply H1.
unfold Par.
right.
repeat split.
assumption.
assumption.
apply col_trivial_1.
Col.
Qed.

Lemma not_par_inter_unicity : forall A B C D X Y, A <> B -> C <> D -> ~Par A B C D -> Col A B X -> Col C D X -> Col A B Y -> Col C D Y -> X = Y.
intros.

induction(eq_dec_points C Y).
subst Y.

induction (eq_dec_points C X).
subst X.
reflexivity.
eapply inter_unicity.
apply H2.
apply H3.
assumption.
assumption.
intro.
apply H1.
apply parallel_symmetry.
unfold Par.
right.
repeat split.
assumption.
assumption.
Col.

assert(Col A C X).
eapply (col_transitivity_1 _ B).
assumption.
Col.
assumption.

assert(Col A C D).

apply col_permutation_2.
eapply (col_transitivity_1 _ X).
assumption.
Col.
Col.

apply col_permutation_2.
eapply (col_transitivity_1 _ C).
intro.
subst C.
apply not_par_not_col in H1.
apply H1.

eapply (col_transitivity_1 _ _).
apply H6.
Col.
Col.
assumption.
assumption.
Col.
assumption.
assumption.

eapply inter_unicity.
apply H2.
apply H3.
assumption.
assumption.
intro.
apply H1.
unfold Par.
right.
repeat split; try assumption.

assert(Col A C Y).
eapply (col_transitivity_1 _ B).
assumption.
Col.
assumption.

apply col_permutation_2.
eapply (col_transitivity_1 _ Y).
assumption.
Col.
Col.

assert(Col B C Y).

eapply (col_transitivity_1 _ A).
auto.
Col.
Col.
apply col_permutation_2.
eapply (col_transitivity_1 _ Y).
assumption.
Col.
Col.
assumption.
Qed.

Lemma not_par_two_sides : forall A B C D, A <> B -> C <> D -> ~Par A B C D -> exists X, exists Y, Col C D X /\ Col C D Y /\ two_sides A B X Y.
intros.
assert(HH:=H1).
apply not_par_inter_exists in H1.
ex_and H1 T.
induction(eq_dec_points C T).
subst T.
prolong D C Y D C.
exists D.
exists Y.
repeat split.
apply col_trivial_2.
apply bet_col in H3.
Col.
assumption.
intro.
apply HH.
apply parallel_symmetry.
unfold Par.
right.
repeat split; try assumption.
Col.

induction(eq_dec_points A C).
subst C.
intro.
apply HH.
apply parallel_symmetry.
unfold Par.
right.
repeat split; try assumption.
Col.
apply col_permutation_2.
eapply (col_transitivity_1 _ Y).
intro.
subst Y.
apply cong_symmetry in H4.
apply cong_identity in H4.
subst D.
absurde.
Col.
apply bet_col in H3.
Col.

intro.
apply HH.
apply parallel_symmetry.
unfold Par.
right.
repeat split; try assumption.
Col.
assert(Col Y A C).
apply col_permutation_2.
eapply col_transitivity_1.
apply H.
assumption.
Col.
assert(Col A C D).
apply col_permutation_2.
eapply (col_transitivity_1 _ Y).
intro.
subst Y.
apply cong_symmetry in H4.
apply cong_identity in H4.
subst D.
absurde.
apply bet_col in H3.
Col.
Col.

apply col_permutation_2.
eapply (col_transitivity_1 _ _).
apply H5.
Col.
assumption.
exists C.
split; Col.

prolong C T Y C T.
exists C.
exists Y.
repeat split.
apply col_trivial_3.

eapply (col_transitivity_1 _ T).
assumption.
Col.
apply bet_col in H4.
assumption.
assumption.
intro.
assert(C=T).
eapply not_par_inter_unicity.
3:apply HH.
assumption.
assumption.
Col.
apply col_trivial_3.
assumption.
Col.
contradiction.
intro.
assert(Y= T).
eapply not_par_inter_unicity.
3: apply HH.
assumption.
assumption.
Col.
eapply (col_transitivity_1 _ T).
assumption.
Col.
apply bet_col.
assumption.
assumption.
Col.
subst Y.
apply cong_symmetry in H5.
apply cong_identity in H5.
contradiction.
exists T.
split.
Col.
assumption.
Qed.

Lemma not_par_other_side : forall A B C D P, A <> B -> C <> D -> ~Par A B C D -> ~Col A B P -> exists Q, Col C D Q /\ two_sides A B P Q.
intros.
assert(exists X, exists Y, Col C D X /\ Col C D Y /\ two_sides A B X Y).
apply not_par_two_sides.
assumption.
assumption.
assumption.
ex_and H3 X.
ex_and H4 Y.

induction(classic(two_sides A B P X)).
exists X.
split; assumption.
apply not_two_sides_one_side in H6.
exists Y.
split.
assumption.
eapply l9_8_2.
apply H5.
apply one_side_symmetry.
assumption.
assumption.
intro.
apply H2.
Col.
unfold two_sides in H5.
spliter.
assumption.
Qed.

Lemma inter_unicity_not_par : forall A B C D P, ~Col A B C -> Col A B P -> Col C D P -> ~Par A B C D.
intros.
intro.
unfold Par in H2.
induction H2.
unfold Par_strict in H2.
spliter.
apply H5.
exists P.
split; Col.
spliter.
apply H.
apply col_permutation_1.
eapply col_transitivity_1.
apply H3.
Col.
Col.
Qed.

Lemma par_strict_one_side : forall A B C D P, Par_strict A B C D -> Col C D P -> one_side A B C P.
Proof.
intros.
assert(HH:= H).
unfold Par_strict in HH.
spliter.
apply l12_6 in H.
unfold one_side in *.
ex_and H C'.
exists C'.
split.
assumption.
apply not_one_side_two_sides.
assumption.
intro.
apply H4.
exists P.
split; Col.
unfold two_sides in H.
spliter.
assumption.
intro.
apply H4.
unfold one_side in H6.
ex_and H6 P'.
assert(one_side A B P C').
eapply l9_8_1.
apply H6.
assumption.
assert(two_sides A B P C).
eapply l9_8_2.
apply l9_2.
apply H.
apply one_side_symmetry.
assumption.
unfold two_sides in H9.
spliter.
ex_and H12 T.
exists T.
split.
assumption.

induction(eq_dec_points C P).
subst P.
apply between_identity in H13.
subst T.
apply col_trivial_1.

eapply col_permutation_2.
eapply (col_transitivity_1 _ P).
assumption.
Col.
apply bet_col in H13.
Col.
Qed.

Lemma col_not_col_not_par : forall A B C D, (exists P, Col A B P /\ Col C D P) -> (exists Q, Col C D Q /\ ~Col A B Q) -> ~Par A B C D.
intros.
ex_and H P.
ex_and H0 Q.
intro.
unfold Par in H3.
induction H3.
unfold Par_strict in H3.
spliter.
apply H6.
exists P.
split; Col.
spliter.
apply H2.
eapply col3.
apply H4.
Col.
Col.
Col.
Qed.

Lemma par_distincts : forall A B C D, Par A B C D -> (Par A B C D /\ A <> B /\ C <> D).
intros.
split.
assumption.
unfold Par in H.
induction H.
unfold Par_strict in H.
spliter.
split; assumption.
spliter.
split; assumption.
Qed.

Lemma par_not_col_strict : forall A B C D P, Par A B C D -> Col C D P -> ~Col A B P -> Par_strict A B C D.
intros.
apply parallel_symmetry in H.
unfold Par in H.
induction H.
apply par_strict_symmetry.
assumption.
spliter.
unfold Par_strict.
repeat split; try assumption.
intro.
ex_and H5 X.
apply H1.
assert(Col A C D).
eapply (col_transitivity_1 _ B).
assumption.
Col.
Col.
assert(Col B C D).
eapply (col_transitivity_1 _ A).
auto.
Col.
Col.
eapply col3.
apply H.
Col.
Col.
Col.
Qed.

Lemma par_strict_all_one_side : forall A B C D, Par_strict A B C D -> (forall P, Col C D P -> one_side A B C P).
intros.
eapply par_strict_one_side.
apply H.
assumption.
Qed.

Lemma all_one_side_par_strict : forall A B C D, C <> D -> (forall P, Col C D P -> one_side A B C P) -> Par_strict A B C D.
intros.
unfold Par_strict.
repeat split.
assert(HH:=H0 D (col_trivial_2 _ _)).
unfold one_side in HH.
ex_and HH C0.
unfold two_sides in H1.
spliter.
assumption.
assumption.
intro.
ex_and H1 X.
assert(HH:= H0 X (col_permutation_1 _ _ _ H2) ).
unfold one_side in HH.
ex_and HH M.
unfold two_sides in H4.
spliter.
contradiction.
Qed.

Lemma col_eq : forall A B X Y, A <> X -> Col A X Y -> Col B X Y -> ~Col A X B -> X = Y.
intros.
eapply inter_unicity.
apply col_trivial_2.
3: apply H0.
apply col_trivial_2.
apply H1.
intro.
apply H2.
Col.
assumption.
Qed.

Lemma par_col_par : forall A B C D D', C <> D' -> Par A B C D -> Col C D D' -> Par A B C D'.
intros.
unfold Par in *.
induction H0.
left.
unfold Par_strict in *.
spliter.
repeat split.
assumption.
assumption.
intro.
apply H4.
ex_and H5 P.
exists P.
split.
assumption.
apply col_permutation_2.
eapply col_transitivity_1.
apply H.
Col.
Col.
right.
spliter.
repeat split.
assumption.
assumption.
apply col_permutation_2.
eapply col_transitivity_1.
apply H2.
assumption.
Col.
apply col_permutation_2.
eapply col_transitivity_1.
apply H2.
assumption.
Col.
Qed.

Lemma par_col2_par : forall A B C D E F, E <> F -> Par A B C D -> Col C D E -> Col C D F -> Par A B E F.
intros.
induction (eq_dec_points C E).
subst E.
eapply par_col_par.
assumption.
apply H0.
assumption.
eapply par_col_par.
assumption.
apply parallel_right_comm.
eapply par_col_par.
apply H3.
apply H0.
assumption.
apply col_permutation_2.
eapply col2.
apply par_distincts in H0.
spliter.
apply H5.
assumption.
assumption.
Qed.

Lemma par_strict_col2_par_strict : forall A B C D E F, E <> F -> Par_strict A B C D -> Col C D E -> Col C D F -> Par_strict A B E F.
intros.
unfold Par_strict in *.
spliter.
repeat split.
assumption.
assumption.
intro.
apply H5.
ex_and H6 X.
exists X.
split.
assumption.
assert(Col C E F).
eapply col2.
apply H3.
assumption.
assumption.
assert(Col D E F).
eapply (col2 _ C).
auto.
Col.
Col.
eapply col3.
apply H.
Col.
Col.
Col.
Qed.

Lemma parallel_unicity : forall A1 A2 B1 B2 C1 C2 P,
 ~ Col P A1 A2 ->
 Par A1 A2 B1 B2 -> Col P B1 B2 ->
 Par A1 A2 C1 C2 -> Col P C1 C2 ->
 Col C1 B1 B2 /\ Col C2 B1 B2.
intros.
apply par_distincts in H0.
apply par_distincts in H2.
spliter.

assert(Par_strict A1 A2 B1 B2).
eapply (par_not_col_strict _ _ _ _ P).
assumption.
Col.
intro.
apply H.
Col.

assert(Par_strict A1 A2 C1 C2).
eapply (par_not_col_strict _ _ _ _ P).
assumption.
Col.
intro.
apply H.
Col.
induction(classic(Col C1 B1 B2 /\ Col C2 B1 B2)).
assumption.
apply not_and in H10.

assert(exists C', Col C1 C2 C' /\ two_sides B1 B2 A1 C').
apply not_par_other_side.
assumption.
assumption.
apply col_not_col_not_par.
exists P.
split; Col.

induction H10.
exists C1.
split.
apply col_trivial_3.
intro.
apply H10.
Col.
exists C2.
split.
apply col_trivial_2.
intro.
apply H10.
Col.
intro.
unfold Par_strict in H8.
spliter.
apply H14.
exists A1.
split.
apply col_trivial_1.
Col.

ex_and H11 C'.

assert(HH:=H12).
unfold two_sides in H12.
spliter.
ex_and H15 B.
double C' P C.
unfold is_midpoint in H17.
spliter.
assert(exists D, Bet B D C /\ Bet P D A1).
eapply inner_pasch.
apply H16.
apply between_symmetry.
assumption.
ex_and H19 D.

assert(C' <> P).
intro.
subst C'.
contradiction.

assert (Par A1 A2 C' P).
eapply par_col2_par.
assumption.
apply H2.
Col.
Col.
assert(Par_strict A1 A2 C' P).
eapply (par_not_col_strict _ _ _ _ P).
assumption.
apply col_trivial_2.
intro.
apply H.
Col.

assert(B <> P).
intro.
subst B.
eapply (par_not_col _ _ _ _ A1) in H23.
apply H23.
apply bet_col in H16.
Col.
apply col_trivial_1.

assert(P <> C).
intro.
subst C.
apply cong_identity in H18.
subst C'.
absurde.

assert(Col B P B1).
apply col_permutation_1.
eapply col_transitivity_1.
apply H8.
Col.
Col.

assert(Col B P B2).
apply col_permutation_1.
eapply (col_transitivity_1 _ B1).
auto.
Col.
Col.

assert(Col C' P C1).
induction(eq_dec_points C' C1).
subst C1.
apply col_trivial_3.
apply col_permutation_1.
eapply (col_transitivity_1 _ ).
apply H5.
assumption.
Col.

assert(Col C P C1).
induction(eq_dec_points C' C1).
subst C1.
apply bet_col in H17.
Col.

apply col_permutation_1.
eapply (col_transitivity_1 _ C').
auto.
apply col_permutation_2.
eapply col_transitivity_1.
apply H21.
apply bet_col.
assumption.
Col.
Col.

assert(Col C' P C2).
induction(eq_dec_points C' C2).
subst C2.
apply col_trivial_3.
apply col_permutation_1.
eapply (col_transitivity_1 _ C1).
auto.
Col.
Col.

assert(Col C P C2).
induction(eq_dec_points C' C2).
subst C2.
apply bet_col in H17.
Col.

apply col_permutation_1.
eapply (col_transitivity_1 _ C').
auto.
apply col_permutation_2.
eapply col_transitivity_1.
apply H21.
apply bet_col.
assumption.
Col.
Col.

assert(~Col B P C).
intro.
assert(Col B P C').
apply col_permutation_2.
eapply col_transitivity_1.
apply H25.
apply bet_col in H17.
Col.
Col.
apply H14.
apply (col3 B P); assumption.

assert(P <> D).
intro.
subst D.
apply bet_col in H19.
contradiction.

assert(HE:=euclid P B C D A1 H20 H19 H33).
ex_and HE X.
ex_and H34 Y.

assert(Hx:= l12_6 A1 A2 P X).
induction(eq_dec_points P X).
subst X.
apply between_identity in H34.
subst B.
absurde.

assert(Par_strict A1 A2 P X).
eapply (par_strict_col2_par_strict _ _ B1 B2).
assumption.
eapply (par_not_col_strict _ _ _ _ P).
assumption.
Col.
intro.
apply H.
Col.
Col.
eapply col3.
apply H24.
assumption.
assumption.
apply bet_col in H34.
Col.
apply Hx in H38.

assert(Hy:= l12_6 A1 A2 P Y).
induction(eq_dec_points P Y).
subst Y.
apply between_identity in H35.
subst C.
absurde.

assert(Par_strict A1 A2 P Y).
eapply (par_strict_col2_par_strict _ _ C1 C2).
assumption.
eapply (par_not_col_strict _ _ _ _ P).
assumption.
Col.
intro.
apply H.
Col.
Col.
eapply (col3 C P).
auto.
assumption.
assumption.
apply bet_col in H35.
Col.
apply Hy in H40.

assert(one_side A1 A2 X Y).
eapply one_side_transitivity.
2:apply H40.
unfold one_side in H38.
unfold one_side.
ex_and H38 Z.
exists Z.
split.
assumption.
assumption.

assert(Ho:=H41).
unfold one_side in H41.
ex_and H41 Z.
unfold two_sides in H41.
unfold two_sides in H42.
spliter.

assert(two_sides A1 A2 X Y).
unfold two_sides.
repeat split.
assumption.
assumption.
assumption.
exists A1.
split.
apply col_trivial_1.
assumption.
apply l9_9 in H49.
contradiction.
Qed.

Lemma par_trans : forall A1 A2 B1 B2 C1 C2, Par A1 A2 B1 B2 -> Par B1 B2 C1 C2 -> Par A1 A2 C1 C2.
intros.
apply par_distincts in H.
apply par_distincts in H0.
spliter.

induction(classic(Par A1 A2 C1 C2)).
assumption.

apply not_par_inter_exists in H5.
ex_and H5 X.

induction(classic(Col X B1 B2)).

unfold Par in H, H0.
induction H.
eapply (par_not_col _ _ _ _ X) in H.
contradiction.
Col.
induction H0.
eapply (par_not_col _ _ _ _ X) in H0.
apply False_ind.
apply H0.
Col.
assumption.
spliter.
unfold Par.
right.
repeat split; try assumption.
eapply (col3 B1 B2).
assumption.
Col.
apply col_permutation_1.
eapply col_transitivity_1.
apply H8.
Col.
Col.
apply col_permutation_1.
eapply (col_transitivity_1 _ C1).
auto.
Col.
Col.
eapply (col3 B1 B2).
assumption.
Col.
apply col_permutation_1.
eapply col_transitivity_1.
apply H8.
Col.
Col.
apply col_permutation_1.
eapply (col_transitivity_1 _ C1).
auto.
Col.
Col.
apply parallel_symmetry in H.
apply col_permutation_2 in H5.
apply col_permutation_2 in H6.

assert(HH:=parallel_unicity B1 B2 A1 A2 C1 C2 X H7 H H5 H0 H6).
spliter.
apply parallel_symmetry .
unfold Par.
right.
repeat split; try assumption.
Qed.

Definition inter A1 A2 B1 B2 X := (exists P, Col P B1 B2 /\ ~Col P A1 A2) /\ Col A1 A2 X /\ Col B1 B2 X.

Lemma inter_trivial : forall A B X, ~Col A B X -> inter A X B X X.
intros.
unfold inter.
split.
exists B.
split.
Col.
intro.
apply H.
Col.
split; Col.
Qed.

Lemma inter_sym : forall A B C D X, C <> D -> inter A B C D X -> inter C D A B X.
intros.

unfold inter in *.
spliter.
ex_and H0 P.

assert(A <> B).
intro.
subst B.
apply H3.
Col.

split.

induction(eq_dec_points A X).
treat_equalities.
exists B.
split.
Col.
intro.
apply H3.
eapply col3.
apply H.
Col.
Col.
Col.

exists A.
split.
Col.
intro.
apply H3.

assert(Col A P X).
eapply col3.
apply H.
Col.
Col.
Col.
apply col_permutation_2.
eapply col_transitivity_1.
apply H5.
Col.
Col.
split; assumption.
Qed.

Lemma inter_left_comm : forall A B C D X, inter A B C D X -> inter B A C D X.
intros.
unfold inter in *.
spliter.
ex_and H P.
split.
exists P.
split.
assumption.
intro.
apply H2.
Col.
split; Col.
Qed.

Lemma inter_right_comm : forall A B C D X, inter A B C D X -> inter A B D C X.
intros.
unfold inter in *.
spliter.
ex_and H P.
split.
exists P.
split.
Col.
assumption.
split; Col.
Qed.

Lemma inter_comm : forall A B C D X, inter A B C D X -> inter B A D C X.
intros.
apply inter_left_comm.
apply inter_right_comm.
assumption.
Qed.

Lemma l12_16 : forall A1 A2 B1 B2 C1 C2 X, Par A1 A2 B1 B2 -> inter A1 A2 C1 C2 X -> exists Y, inter B1 B2 C1 C2 Y.
intros.
assert(HH:= H).
unfold Par in H.
induction H.
unfold inter in H0.
spliter.
ex_and H0 P.

assert(~Col B1 B2 X).
intro.
unfold Par_strict in H.
spliter.
apply H7.
exists X.
auto with Col.
assert(HH1:= l8_18_existence B1 B2 X H4).
ex_and HH1 X0.

assert(~Par B1 B2 C1 C2).
intro.
assert(Par A1 A2 C1 C2).
eapply (par_trans _ _ B1 B2).
unfold Par.
left.
assumption.
assumption.
assert(~Par A1 A2 C1 C2).
apply col_not_col_not_par.
exists X.
auto with Col.
exists P.
auto with Col.
contradiction.
apply not_par_inter_exists in H7.
ex_and H7 Y.
exists Y.
split.
exists X.
split.
auto with Col.
intro.
apply H4.
auto with Col.
auto with Col.
unfold inter in H0.
spliter.
ex_and H0 P.
exists X.
split.
exists P.
split.
auto with Col.
intro.
apply H6.
eapply (col3 B1 B2); auto with Col.
split.
apply parallel_symmetry in HH.
unfold Par in HH.
induction HH.
unfold Par_strict in H7.
spliter.
apply False_ind.
apply H10.
exists A1.
split.
auto with Col.
apply col_trivial_1.
spliter.
apply (col3 A1 A2); auto with Col.
auto with Col.
Qed.

Lemma l12_17 : forall A B C D P, A <> B -> is_midpoint P A C -> is_midpoint P B D -> Par A B C D.
intros.
induction(classic(Col A B P)).

unfold Par.

right.

induction(eq_dec_points A P).
subst P.
apply is_midpoint_id in H0.
subst C.
repeat split.
assumption.
intro.
treat_equalities.
apply l7_2 in H1.
apply is_midpoint_id in H1.
contradiction.
apply col_trivial_1.
unfold is_midpoint in H1.
spliter.
apply bet_col.
assumption.

induction(eq_dec_points B P).
subst P.
apply is_midpoint_id in H1.
subst D.
repeat split.
assumption.
intro.
subst C.
apply l7_2 in H0.
apply is_midpoint_id in H0.
auto.
unfold is_midpoint in H0.
spliter.
apply bet_col in H0 .
Col.
apply col_trivial_3.

assert(HH0 := H0).
assert(HH1:= H1).

unfold is_midpoint in H0.
unfold is_midpoint in H1.
spliter.
apply bet_col in H1.
apply bet_col in H0.

assert(Col B C P).
eapply col_permutation_1.
eapply (col_transitivity_1 _ A).
auto.
Col.
Col.

assert(Col B C D).
eapply (col_transitivity_1 _ P).
assumption.
Col.
Col.

repeat split.
assumption.
intro.
treat_equalities.
assert(A = B).
eapply midpoint_id.
apply l7_2.
apply HH0.
apply l7_2.
assumption.
contradiction.

induction(eq_dec_points A D).
subst D.
apply col_trivial_3.

assert(Col C D P).
eapply (col_transitivity_1 _ B).
intro.
subst C.
assert(A = D).
eapply midpoint_id.
eapply l7_2.
apply HH0.
assumption.
contradiction.
Col.
Col.

induction(eq_dec_points C P).
treat_equalities.
intuition.

apply col_permutation_2.
eapply (col_transitivity_1 _ P).
assumption.
Col.
Col.
assumption.


assert(exists E, Col A B E /\ Perp A B P E).
eapply l8_18_existence.
assumption.
ex_and H3 E.

assert(A <> P).
intro.
treat_equalities.
apply H2.
apply col_trivial_3.

induction(eq_dec_points A E).
treat_equalities.
assert(Per P A B).
eapply perp_in_per.
apply perp_in_comm.
eapply perp_perp_in.
apply perp_sym.
apply perp_comm.
assumption.

prolong B A B' B A.
prolong B' P D' B' P.
assert(is_midpoint C D D').
eapply symmetry_preserves_midpoint.
apply H1.
apply H0.
split.
apply H8.
Cong.
split.
assumption.
Cong.

assert(Per P A B').
eapply per_col.
apply H.
assumption.
apply bet_col in H6.
Col.

ex_and H3 B''.
assert(B' = B'').
eapply symmetric_point_unicity.
split.
apply H6.
Cong.
assumption.
subst B''.

assert(Cong P D P D').
apply (cong_transitivity _ _ B P).
unfold is_midpoint in H1.
spliter.
Cong.
apply (cong_transitivity _ _ B' P).
Cong.
Cong.

assert(Per P C D).
unfold Per.
exists D'.
split; assumption.
apply per_perp_in in H14.
apply perp_in_perp in H14.
induction H14.
apply perp_distinct in H14.
intuition.

eapply l12_9.
apply I.
apply H4.
apply perp_sym.
eapply perp_col.
auto.
apply H14.
unfold is_midpoint in H0.
spliter.
apply bet_col in H0.
Col.
intro.
treat_equalities.
apply l7_2 in H0.
eapply is_midpoint_id in H0.
auto.
intro.
subst D.
assert(C = D').
apply is_midpoint_id.
assumption.
subst D'.
assert(A = B).
eapply midpoint_id.
apply l7_2.
apply H0.
apply l7_2.
assumption.
auto.

prolong E P F E P.

assert(Col C D F).
eapply mid_preserves_col.
2: apply H0.
2:apply H1.
apply H3.
split.
assumption.
Cong.

prolong A E A' A E.
prolong A' P C' A' P.
assert(is_midpoint F C C').
eapply symmetry_preserves_midpoint.
apply H0.
split.
apply H7.
Cong.
split.
apply H12.
Cong.
split.
assumption.
Cong.

assert(Per P E A).
eapply perp_in_per.
apply perp_in_comm.
apply perp_perp_in.
apply perp_sym.
eapply perp_col.
assumption.
apply perp_right_comm.
apply H4.
Col.

assert(Cong P C P C').
eapply (cong_transitivity _ _ P A).
unfold is_midpoint in H0.
spliter.
Cong.
eapply (cong_transitivity _ _ P A').
unfold Per in H15.
ex_and H15 A''.
assert( A' = A'').
eapply symmetric_point_unicity.
split.
apply H10.
Cong.
assumption.
subst A''.
assumption.
Cong.
assert(Per P F C).
unfold Per.
exists C'.
split.
assumption.
assumption.
apply per_perp_in in H17.
apply perp_in_comm in H17.
apply perp_in_perp in H17.
induction H17.
eapply l12_9.
apply I.
apply H4.
eapply perp_col.
intro.
subst D.
assert (A = B).
eapply midpoint_id.
apply l7_2.
apply H0.
apply l7_2.
assumption.
auto.
apply perp_sym.
eapply perp_col.
intro.
treat_equalities.
apply perp_distinct in H17.
spliter.
auto.
apply perp_left_comm.
apply H17.
apply bet_col in H7.
Col.
Col.
apply perp_distinct in H17.
spliter.
tauto.

intro.
treat_equalities.
apply perp_distinct in H4.
spliter.
tauto.
intro.
subst C.

assert(F = C').
apply is_midpoint_id .
assumption.
treat_equalities.
assert(A = E).
eapply midpoint_id.
apply l7_2.
apply H0.
split.
apply between_symmetry.
assumption.
Cong.
tauto.
Qed.

Lemma l12_18_a : forall A B C D P, Cong A B C D -> Cong B C D A -> ~Col A B C ->
                                  B <> D -> Col A P C -> Col B P D
                                  -> Par A B C D.
intros.
assert(is_midpoint P A C /\ is_midpoint P B D) by (apply l7_21; assumption).
spliter.
eapply l12_17.
intro.
subst B.
apply H1.
apply col_trivial_1.
apply H5.
apply H6.
Qed.

Lemma l12_18_b : forall A B C D P, Cong A B C D -> Cong B C D A -> ~Col A B C ->
                                  B <> D -> Col A P C -> Col B P D
                                  -> Par B C D A.
intros.
assert(is_midpoint P A C /\ is_midpoint P B D) by (apply l7_21; assumption).
eapply l12_18_a.
assumption.
Cong.
intro.
apply H1.
assert(Col B C P).
eapply col_transitivity_1.
apply H2.
Col.
Col.
apply col_permutation_1.
eapply (col2 _ P).
intro.
subst P.
spliter.
apply l7_2 in H5.
apply is_midpoint_id in H5.
subst C.
apply H1.
apply col_trivial_3.
Col.
Col.
intro.
subst C.
apply H1.
apply col_trivial_3.
apply H4.
Col.
Qed.

Lemma l12_18_c : forall A B C D P, Cong A B C D -> Cong B C D A -> ~Col A B C ->
                                  B <> D -> Col A P C -> Col B P D
                                  -> two_sides B D A C.
intros.
assert(is_midpoint P A C /\ is_midpoint P B D) by (apply l7_21; assumption).
unfold two_sides.
repeat split.
assumption.
intro.
apply H1.
assert(Col A B P).
apply col_permutation_2.
eapply (col2 _ D).
assumption.
Col.
Col.
eapply (col2 _ P).
intro.
subst P.
spliter.
apply is_midpoint_id in H5.
subst C.
apply H1.
apply col_trivial_3.
Col.
Col.
intro.
apply H1.
assert(Col B P C).

eapply (col2 _ D).
assumption.
Col.
Col.
apply col_permutation_1.
eapply (col2 _ P).
intro.
subst P.
spliter.
apply l7_2 in H5.
apply is_midpoint_id in H5.
subst C.
apply H1.
apply col_trivial_3.
Col.
Col.
exists P.
split.
Col.
spliter.
unfold is_midpoint in H5.
tauto.
Qed.

Lemma l12_18_d : forall A B C D P, Cong A B C D -> Cong B C D A -> ~Col A B C ->
                                  B <> D -> Col A P C -> Col B P D
                                  -> two_sides A C B D.
intros.
assert(is_midpoint P A C /\ is_midpoint P B D) by (apply l7_21; assumption).
eapply (l12_18_c _ _ _ _ P).
Cong.
Cong.
intro.
apply H1.
assert(Col A B P).
eapply col_permutation_2.
eapply col2.
apply H2.
Col.
Col.
eapply (col2 _ P).
intro.
subst P.
spliter.
apply is_midpoint_id in H5.
subst C.
contradiction.
Col.
Col.
intro.
subst C.
apply H1.
apply col_trivial_3.
Col.
Col.
Qed.

Lemma l12_18 : forall A B C D P, Cong A B C D -> Cong B C D A -> ~Col A B C ->
                                  B <> D -> Col A P C -> Col B P D
                                  -> Par A B C D /\ Par B C D A /\
                                  two_sides B D A C /\ two_sides A C B D.
intros.
split.
apply (l12_18_a _ _ _ _ P); assumption.
split.
apply (l12_18_b _ _ _ _ P); assumption.
split.
apply (l12_18_c _ _ _ _ P); assumption.
apply (l12_18_d _ _ _ _ P); assumption.
Qed.

Lemma l12_19 : forall A B C D , ~Col A B C -> Par A B C D -> Par B C D A ->
                                  Cong A B C D /\ Cong B C D A /\
                                  two_sides B D A C /\ two_sides A C B D.
intros.
assert(exists P, is_midpoint P A C) by (eapply midpoint_existence).
ex_and H2 P.
double B P D'.

assert(Cong C D' A B).
eapply (l7_13 P); assumption.
assert(Cong B C D' A).
eapply (l7_13 P).
apply l7_2.
assumption.
assumption.

assert(Par A B C D').
eapply l12_17.
intro.
subst B.
apply H.
apply col_trivial_1.
apply H3.
assumption.

assert(Par C D C D').
eapply par_trans.
apply parallel_symmetry.
apply H0.
apply H6.

assert(Col C D D').
unfold Par in H7.
induction H7.
unfold Par_strict in H7.
spliter.
apply False_ind.
apply H10.
exists C.
split; apply col_trivial_1.
spliter.
Col.

assert(Par B C D' A).
eapply l12_17.
intro.
subst B.
apply H.
apply col_trivial_2.
apply H2.
apply l7_2.
assumption.

assert(Par D A D' A).
eapply par_trans.
apply parallel_symmetry.
apply H1.
assumption.

assert(Col A D D').
unfold Par in H10.
induction H10.
unfold Par_strict in H10.
spliter.
apply False_ind.
apply H13.
exists A.
split; apply col_trivial_3.
spliter.
Col.

assert(D = D').
eapply inter_unicity.
3: apply H11.
apply col_trivial_2.
2: apply H8.
apply col_trivial_2.
intro.
apply H.

assert(Col P C D).
apply col_permutation_2.
eapply (col_transitivity_1 _ A).
intro.
subst C.
apply H.
apply col_trivial_3.
Col.
unfold is_midpoint in H3.
spliter.
apply bet_col in H3.
Col.

assert(Col P C D').
apply col_permutation_2.
eapply (col2 _ D).
apply par_distincts in H0.
spliter.
assumption.
Col.
Col.

assert(Col P A D').
eapply (col2 _ C).
intro.
subst P.
apply l7_2 in H3.
apply is_midpoint_id in H3.
subst C.
apply H.
apply col_trivial_3.
unfold is_midpoint in H3.
spliter.
apply bet_col in H3.
Col.
assumption.
eapply (col3 P D').
intro.
subst D'.
apply l7_2 in H2.
apply is_midpoint_id in H2.
subst P.
apply H.
unfold is_midpoint in H3.
spliter.
apply bet_col.
assumption.
Col.
unfold is_midpoint in H2.
spliter.
apply bet_col in H2.
Col.
Col.
apply par_distincts in H0.
spliter.
assumption.
subst D'.
split.
Cong.
split.
Cong.

assert(B <> D).
intro.
subst D.
apply l7_3 in H2.
subst P.
apply H.
unfold Par in H0.
induction H0.
unfold Par_strict in H0.
spliter.
apply False_ind.
apply H13.
exists B.
split; apply col_trivial_3.
spliter.
Col.
unfold is_midpoint in *.
spliter.

split.

eapply l12_18_c.
Cong.
Cong.
assumption.
assumption.
apply bet_col.
apply H3.
apply bet_col.
assumption.

eapply l12_18_d.
Cong.
Cong.
assumption.
assumption.
apply bet_col.
apply H3.
apply bet_col.
assumption.
Qed.

Lemma par_two_sides_two_sides : forall A B C D, Par A B C D -> two_sides B D A C -> two_sides A C B D.
intros.
apply par_distincts in H.
spliter.
unfold Par in H.
induction H.

Focus 2.

unfold two_sides in H0.
spliter.
apply False_ind.
apply H3.
apply col_permutation_1.
eapply (col_transitivity_1 _ C).
auto.
Col.
Col.

assert(A <> C).
intro.
subst C.
unfold Par_strict in H.
spliter.
apply H5.
exists A.
split; apply col_trivial_1.

unfold two_sides in *.
spliter.
ex_and H6 T.
repeat split.
assumption.

intro.
assert(Col T B C).
apply col_permutation_1.
eapply (col_transitivity_1 _ A).
auto.
apply bet_col in H7.
Col.
Col.
apply H5.
apply col_permutation_2.
eapply (col_transitivity_1 _ T).
intro.
treat_equalities.
unfold Par_strict in H.
spliter.
apply H10.
exists C.
split.
Col.
apply col_trivial_1.
Col.
Col.
intro.

assert(Col T C D).
apply col_permutation_2.
apply (col_transitivity_1 _ A).
auto.
Col.
apply bet_col in H7.
Col.
apply H5.
apply col_permutation_1.
apply (col_transitivity_1 _ T).
intro.
treat_equalities.
unfold Par_strict in H.
spliter.
apply H10.
exists A.
split.
apply col_trivial_1.
Col.
Col.
Col.
exists T.

split.
apply bet_col in H7.
Col.

unfold Col in H6.
induction H6.

assert(HH:= outer_pasch C D T A B (between_symmetry _ _ _ H7) (between_symmetry _ _ _ H6)).
ex_and HH X.
unfold Par_strict in H.
spliter.
apply False_ind.
apply H12.
exists X.
apply bet_col in H8.
apply bet_col in H9.
split; Col.

induction H6.
assert(HH:= outer_pasch A B T C D H7 H6).
ex_and HH X.
apply False_ind.
unfold Par_strict in H.
spliter.
apply H12.
exists X.
apply bet_col in H8.
apply bet_col in H9.
split; Col.
apply between_symmetry.
assumption.
Qed.

Lemma out_one_side : forall A B C D X, A <> B -> ~ Col A B C -> Col A B X -> out X C D -> one_side A B C D.
intros.

induction (eq_dec_points C D).
subst D.
apply one_side_reflexivity.
intro.
apply H0.
Col.

prolong C X C' C X.
exists C'.
assert(two_sides A B C C').
unfold two_sides.
repeat split.
assumption.
intro.
apply H0.
Col.
intro.
assert(C'=X).
eapply (inter_unicity A B C D).
Col.
apply out_col in H2.
eapply (col_transitivity_1 _ X).
intro.
treat_equalities.
contradiction.
Col.
apply bet_col in H4.
Col.
assumption.
apply out_col in H2.
Col.
intro.
apply H0.
Col.
assumption.
treat_equalities.
unfold out in H2.
tauto.
exists X.
split; Col.
assert(two_sides A B D C').
eapply (l9_5 _ _ _ _ X).
apply H6.
Col.
assumption.
split; assumption.
Qed.

Lemma l12_20_bis : forall A B C D, Par A B C D -> Cong A B C D -> two_sides B D A C ->
                               Par B C D A /\ Cong B C D A /\ two_sides A C B D.
intros.

induction(eq_dec_points B C).
subst C.
unfold two_sides in H1.
spliter.
apply False_ind.
apply H3.
apply col_trivial_1.

induction(eq_dec_points A D).
subst D.
unfold two_sides in H1.
spliter.
apply False_ind.
apply H3.
apply col_trivial_3.

assert(~ Col A B C).
intro.
assert(Col A B D).
eapply not_strict_par1.
2: apply H4.
2: apply col_trivial_2.
apply parallel_right_comm.
assumption.

unfold two_sides in H1.
spliter.
contradiction.

assert(exists P, is_midpoint P A C) by (apply midpoint_existence).
ex_and H5 P.
double B P D'.

assert(Par B C D' A).
eapply l12_17.
assumption.
apply H5.
apply l7_2.
assumption.

assert(Par A B C D').
eapply l12_17.
intro.
subst B.
apply H4.
apply col_trivial_1.
apply H6.
assumption.

assert(Cong C D' A B).
eapply (l7_13 P); assumption.
assert(Cong B C D' A).
eapply (l7_13 P).
apply l7_2.
assumption.
assumption.

assert(Par C D C D').
eapply par_trans.
apply parallel_symmetry.
apply H.
assumption.

assert(Col C D D').
unfold Par in H11.
induction H11.
unfold Par_strict in H11.
spliter.
apply False_ind.
apply H14.
exists C.
split; apply col_trivial_1.
spliter.
Col.

assert(Cong C D C D').
eapply (cong_transitivity _ _ A B).
Cong.
Cong.

assert(D = D' \/ is_midpoint C D D').
eapply l7_20.
Col.
assumption.

induction H14.
subst D'.
assert(Par B C D A).
eapply l12_17.
assumption.
apply H5.
apply l7_2.
assumption.
split.
assumption.
assert(HH:=l12_19 A B C D H4 H H14).
spliter.
split; assumption.


assert(two_sides A C B D).
apply par_two_sides_two_sides.
assumption.
assumption.
assert(HH:= H15).
assert(HH1:=H1).
unfold two_sides in H15, H1.
spliter.
ex_and H21 T.
ex_and H18 T'.

assert(T = T').
apply bet_col in H22.
apply bet_col in H23.
eapply (inter_unicity A C B D); Col.
subst T'.

assert(~Col B C T).
intro.
apply H16.
apply col_permutation_1.
eapply (col_transitivity_1 _ T).
intro.
treat_equalities.
apply H20.
apply bet_col in H23.
Col.
Col.
Col.

assert(one_side B C T D).
eapply out_one_side.
assumption.
assumption.
apply col_trivial_3.
apply bet_out in H23.
assumption.
intro.
treat_equalities.
apply H24.
apply col_trivial_3.
auto.

assert(one_side B C T A).
eapply out_one_side.
assumption.
assumption.
apply col_trivial_2.
apply between_symmetry in H22.
apply bet_out in H22.
assumption.
intro.
treat_equalities.
apply H24.
apply col_trivial_2.
assumption.

assert(one_side B C A D).
apply (one_side_transitivity _ _ _ T).
apply one_side_symmetry.
assumption.
assumption.

assert(two_sides B C D D').
unfold two_sides.
repeat split.
assumption.
intro.
apply H20.
Col.
intro.
apply H20.
eapply (col_transitivity_1 _ D').
intro.
treat_equalities.
apply H17.
apply col_trivial_3.
Col.
Col.

exists C.
split.
apply col_trivial_3.
unfold is_midpoint in H14.
spliter.
assumption.

assert(two_sides B C A D').
eapply l9_8_2.
apply H28.
apply one_side_symmetry.
assumption.
unfold Par in H7.
induction H7.
unfold Par_strict in H7.
spliter.
apply False_ind.
apply H32.
unfold two_sides in H29.
spliter.
ex_and H35 X.
exists X.
split.
assumption.
apply bet_col in H36.
Col.
spliter.

apply False_ind.
apply H4.
eapply (col_transitivity_1 _ P).
intro.
subst P.
apply is_midpoint_id in H6.
tauto.
apply col_permutation_1.
eapply (col_transitivity_1 _ D').
intro.
treat_equalities.
apply l7_3 in H5.
subst P.

apply H4.
unfold is_midpoint in H6.
spliter.
auto.
apply bet_col.
assumption.
Col.

unfold is_midpoint in H5.
spliter.
apply bet_col in H5.
Col.
unfold is_midpoint in H6.
spliter.
apply bet_col in H6.
Col.
Qed.

Lemma l12_20 : forall A B C D, Par A B C D -> Cong A B C D -> two_sides A C B D ->
                               Par B C D A /\ Cong B C D A /\ two_sides A C B D.
intros.

assert(two_sides B D A C).
apply par_two_sides_two_sides.
apply parallel_comm.
assumption.
assumption.

assert(HH:=l12_20_bis A B C D H H0 H2).
spliter.
split.
assumption.
split.
assumption.
assumption.
Qed.

Lemma par_one_or_two_sides : forall A B C D, Par_strict A B C D
            -> two_sides A C B D /\ two_sides B D A C \/ one_side A C B D /\ one_side B D A C.
intros.
induction(classic (two_sides A C B D)).
left.
split.
assumption.
apply par_two_sides_two_sides.
apply parallel_comm.
unfold Par.
left.
assumption.
assumption.
right.

assert(HH:=H).
unfold Par_strict in H.
spliter.

assert(A <> C).
intro.
subst C.
apply H3.
exists A.
split; Col.

assert(B <> D).
intro.
subst D.
apply H3.
exists B.
split; Col.

split.

apply not_two_sides_one_side.
assumption.
intro.
apply H3.
exists C.
split; Col.
intro.
apply H3.
exists A.
split; Col.
assumption.

apply not_two_sides_one_side.
assumption.
intro.
apply H3.
exists D.
split; Col.
intro.
apply H3.
exists B.
split; Col.
intro.
apply H0.
apply par_two_sides_two_sides.
left.
assumption.
assumption.
Qed.

Lemma l12_21_a : forall A B C D, two_sides A C B D -> (Par A B C D -> Conga B A C D C A).
intros.

assert(two_sides B D A C).
apply par_two_sides_two_sides.
apply parallel_comm.
assumption.
assumption.

assert(B <> C).
intro.
subst B.
unfold two_sides in H.
spliter.
apply H2.
apply col_trivial_3.

assert(~Col B C D).
unfold two_sides in H1.
spliter.
intro.
apply H4.
Col.

assert(inter B C D C C).
repeat split.
exists D.
split.
apply col_trivial_1.
intro.
apply H3.
Col.
apply col_trivial_2.
apply col_trivial_2.

assert(HH:= parallel_existence B C A H2).
ex_and HH X.
ex_and H5 Y.

assert(HH:=l12_16 B C X Y D C C H6 H4).
ex_and HH D'.

apply par_distincts in H0.
spliter.

assert(~Col A B C).
intro.
unfold Par in H0.
induction H0.
unfold Par_strict in H0.
spliter.
apply H14.
exists C.
split; Col.
spliter.
contradiction.

assert(Par B C A D').
eapply par_col2_par.
intro.
subst D'.

unfold Par in H0.
induction H0.
unfold Par_strict in H0.
spliter.
apply H14.

unfold inter in H7.
ex_and H8 P.
exists A.
split; Col.
spliter.
contradiction.
apply H6.
Col.
unfold inter in H8.
spliter.
assumption.

assert(Par_strict A B C D).
unfold Par in H0.
induction H0.
assumption.
spliter.
apply False_ind.
apply H11.
apply col_permutation_1.
eapply (col2 _ D).
assumption.
Col.
Col.

assert(Par_strict B C A D').
unfold Par in H12.
induction H12.
assumption.
spliter.
unfold Par_strict.
repeat split; try assumption.
intro.
ex_and H17 P.
apply H11.
eapply col2.
apply H14.
Col.
Col.

assert(Par A B C D').
eapply par_col_par.
intro.
subst D'.

unfold Par_strict in H14.
spliter.
apply H17.
exists C.
split; Col.
apply H0.
unfold inter in H8.
spliter.
Col.

apply parallel_right_comm in H12.

assert(HH:= l12_19 A B C D' H11 H15 H12).
spliter.

assert(A <> C).
unfold two_sides in H19.
spliter.
assumption.

assert(Conga B A C D' C A).
apply cong3_conga.
auto.
auto.
repeat split; Cong.

eapply l11_10.
apply H21.
apply out_trivial.
auto.
apply out_trivial.
auto.

unfold inter in H8.
spliter.
induction H23.

assert(one_side A C D D').
eapply l9_8_1.
apply l9_2.
apply H.
apply l9_2.
assumption.
assert(two_sides A C D D').
unfold two_sides.
repeat split.
assumption.
unfold two_sides in H.
spliter.
assumption.
unfold two_sides in H19.
spliter.
assumption.
exists C.
split.
apply col_trivial_3.
assumption.
apply l9_9 in H25.
contradiction.
induction H23.
apply bet_out in H23.
apply l6_6.
assumption.
intro.
treat_equalities.
auto.
auto.
apply between_symmetry in H23.
apply bet_out in H23.
assumption.
auto.
intro.
treat_equalities.
auto.
apply out_trivial.
auto.
Qed.

Lemma midpoint_preserves_out : forall A B C A' B' C' M, out A B C ->
                                        is_midpoint M A A' -> is_midpoint M B B' -> is_midpoint M C C'
                                        -> out A' B' C'.
intros.
unfold out in H.
spliter.
unfold out.
repeat split.
intro.
subst B'.
assert (A = B).
eapply symmetric_point_unicity.
apply l7_2.
apply H0.
apply l7_2.
assumption.
auto.

intro.
subst C'.
assert (A = C).
eapply symmetric_point_unicity.
apply l7_2.
apply H0.
apply l7_2.
assumption.
auto.

induction H4.
left.
apply (l7_15 A B C A' B' C' M); assumption.
right.
eapply (l7_15 A C B A' C' B' M); assumption.
Qed.

Lemma l12_21_b : forall A B C D, two_sides A C B D -> (Conga B A C D C A -> Par A B C D).
intros.

apply conga_diff in H0.
spliter.

assert(~Col A B C).
intro.
unfold two_sides in H.
spliter.
apply col_permutation_4 in H5.
assert(Col D C A).
eapply col_conga_col.
apply H5.
assumption.
contradiction.

assert(A <> B /\ C <> D).
auto.
spliter.

assert(HH:=segment_construction_3 C D A B H7 H6).
ex_and HH D'.

assert(Conga B A C D' C A).
eapply l11_10.
apply H0.
apply out_trivial.
assumption.
apply out_trivial.
assumption.
apply l6_6.
assumption.
apply out_trivial.
assumption.

assert(Cong D' A B C).
eapply cong2_conga_cong.
apply conga_sym.
apply H10.
Cong.
Cong.

assert(two_sides A C D' B).
eapply l9_5.
apply l9_2.
apply H.
apply col_trivial_3.
assumption.
unfold two_sides in H12.
spliter.
ex_and H15 M.

assert(B <> D').

intro.
treat_equalities.
contradiction.

assert(is_midpoint M A C /\ is_midpoint M B D').
apply l7_21.
assumption.
assumption.
Cong.
Cong.
Col.
apply bet_col in H16.
Col.
spliter.

assert(Par A B C D').

eapply l12_17.
assumption.
apply H18.
assumption.
eapply par_col_par.
auto.
apply H20.
apply out_col in H8.
Col.
Qed.

Lemma l12_21 : forall A B C D , two_sides A C B D -> (Conga B A C D C A <-> Par A B C D).
intros.
split.
intro.
apply l12_21_b ; assumption.
intro.
apply l12_21_a; assumption.
Qed.

Lemma par_id : forall A B C, Par A B A C -> Col A B C.
intros.
unfold Par in H.
induction H.
unfold Par_strict in H.
spliter.
apply False_ind.
apply H2.
exists A.
split; Col.
spliter.
Col.
Qed.

Lemma not_par_strict_id : forall A B C, ~ Par_strict A B A C.
intros.
intro.
unfold Par_strict in H.
spliter.
apply H2.
exists A.
split; Col.
Qed.

Lemma l6_7_1 : forall A B C D, out A B C -> out A B D -> out A C D.
intros.
unfold out in *.
spliter.
repeat split.
assumption.
assumption.
induction H4; induction H2.
eapply l5_1.
2: apply H4.
auto.
assumption.
right.
eapply between_exchange4.
apply H2.
assumption.
left.
eapply between_exchange4.
apply H4.
assumption.
eapply l5_3.
apply H4.
apply H2.
Qed.

Lemma l12_22_a : forall A B C D P, out P A C -> one_side P A B D -> Par A B C D -> Conga B A P D C P.
intros.

unfold Par in H1.
induction H1.

assert(~Col A B C).
intro.
unfold Par_strict in H1.
spliter.
apply H5.
exists C.
split; Col.

assert( A <> C).
intro.
treat_equalities.
assert(HH := not_par_strict_id A B D).
contradiction.
assert(HH:= parallel_existence A C B H3).
ex_and HH X.
ex_and H4 Y.

assert(inter A C C D C).

apply inter_right_comm.
apply inter_trivial.
intro.
unfold Par_strict in H1.
spliter.
apply H10.
exists A.
split; Col.

assert(HH:= l12_16 A C X Y C D C H5 H7).
ex_and HH D'.

assert(Par A C B D').
eapply par_col2_par.
intro.
unfold Par_strict in H1.
spliter.
unfold inter in H8.
spliter.
treat_equalities.
apply H12.
exists B.
split; Col.
apply H5.
Col.
unfold inter in H8.
spliter.
assumption.

assert(Par A B C D').
eapply par_col_par.
intro.
treat_equalities.
apply H2.
apply parallel_comm in H9.
apply par_id in H9.
Col.
unfold Par.
left.
apply H1.
unfold inter in H8.
spliter.
assumption.

assert(Par_strict A C B D').
unfold Par in H9.
induction H9.
assumption.
spliter.
apply False_ind.
apply H2.
apply col_permutation_2.
eapply (col_transitivity_1 _ D').
assumption.
Col.
Col.

assert(Cong A B D' C /\
     Cong B D' C A /\ two_sides B C A D' /\ two_sides A D' B C).

eapply l12_19.
eapply par_not_col.
apply H11.
Col.
apply parallel_right_comm.
assumption.
apply parallel_symmetry.
apply parallel_left_comm.
assumption.
spliter.


prolong C A C' C A.

assert(Par B D' A C').
eapply par_col_par.
intro.
treat_equalities.
tauto.

unfold Par.
left.

apply par_strict_symmetry.
apply H11.
apply bet_col in H16.
Col.

assert(Cong B D' A C').
eCong.

assert(Par_strict A B C D').
unfold Par in H10.
induction H10.
assumption.
spliter.
apply False_ind.
apply H2.
apply col_permutation_1.
eapply (col_transitivity_1 _ D').
intro.
treat_equalities.
tauto.
Col.
Col.

assert(HH := l12_6 A B C D' H20).

assert(two_sides A B C C').
unfold two_sides.
repeat split.
intro.
treat_equalities.
apply H2.
Col.
intro.
apply H2.
Col.
intro.
apply H2.

eapply (col_transitivity_1 _ C').
intro.
treat_equalities.
tauto.
Col.
apply bet_col in H16.
Col.
exists A.
split.
Col.
assumption.

assert(two_sides A B D' C').
eapply l9_8_2.
apply H21.
assumption.

assert(two_sides C' D' A B).
apply par_two_sides_two_sides.
apply parallel_comm.
apply parallel_symmetry.
assumption.
apply l9_2.
assumption.
apply l9_2 in H23.

apply invert_two_sides in H22.
assert(HH1:= l12_20 B D' A C' H18 H19 H22).
spliter.

assert(Cong_3 D' C A B A C').
repeat split; Cong.
apply cong3_conga in H27.

assert(one_side A C D D').
eapply one_side_transitivity.
eapply col_one_side.
Focus 3.
apply invert_one_side.
apply one_side_symmetry.
apply H0.
apply out_col in H.
Col.
assumption.
apply l12_6.
induction H9.
assumption.
spliter.
apply False_ind.
apply H2.
apply col_permutation_2.
eapply (col_transitivity_1 _ D').
assumption.
Col.
Col.

assert(out C D' D).
unfold inter in H8.
spliter.

induction H30.
apply l6_6.
apply bet_out.
intro.
treat_equalities.
unfold Par_strict in H1.
tauto.
intro.
treat_equalities.
unfold two_sides in H14.
spliter.
apply H12.
Col.
assumption.

induction H30.
apply bet_out.
intro.
treat_equalities.
unfold Conga in H27.
tauto.

intro.
treat_equalities.
unfold Conga in H27.
tauto.

apply between_symmetry.

assumption.

assert(two_sides A C D D').
unfold two_sides.
repeat split.
auto.

unfold one_side in H28.
ex_and H28 K.
unfold two_sides in H28.
tauto.

unfold one_side in H28.
ex_and H28 K.
unfold two_sides in H31.
tauto.
exists C.
split.
Col.
apply between_symmetry.
assumption.
apply l9_9 in H31.
contradiction.

unfold out in H.
spliter.
induction H31.

assert(out C A C').
unfold out.
repeat split.
assumption.
intro.
subst C'.
apply between_identity in H16.
subst C.

assert(HX:=not_par_strict_id A B D').
apply HX.
contradiction.
left.
assumption.

assert(Conga D' C A D C P).
eapply l11_10.
apply conga_refl.
3: apply H29.
3:apply H32.
intro.
treat_equalities.
unfold out in H29.
tauto.
intro.
treat_equalities.
unfold two_sides in H22.
spliter.
apply H12.
Col.
apply out_trivial.
intro.
treat_equalities.
unfold out in H29.
tauto.

unfold out.
repeat split.
intro.
treat_equalities.
unfold Conga in H27.
tauto.
intro.
treat_equalities.
unfold two_sides in H14.
spliter.
apply H13.
Col.

unfold out in H32.
spliter.
induction H34.
eapply (l5_1 _ A).
auto.
apply between_symmetry.
assumption.
assumption.
right.
eapply between_exchange4.
apply H34.
apply between_symmetry.
assumption.

assert(Conga B A P B A C').
eapply l11_10.
apply (conga_refl B A P).
intro.
treat_equalities.
apply H2.
Col.
intro.
treat_equalities.
tauto.
apply out_trivial.
intro.
treat_equalities.
unfold Conga in H33.
tauto.
apply out_trivial.
intro.
treat_equalities.
tauto.
apply out_trivial.
intro.
treat_equalities.
unfold Conga in H33.
tauto.

unfold out.
repeat split.
intro.
treat_equalities.
unfold out in H32.
tauto.
auto.
eapply (l5_2 C).
auto.
assumption.
apply between_symmetry.
assumption.

eapply conga_trans.
apply H34.
eapply conga_trans.
apply conga_sym.
apply H27.
assumption.
apply conga_comm.

assert(Conga D C A B A C').
eapply l11_10.
apply H27.
apply l6_6.
assumption.
apply out_trivial.
assumption.
apply out_trivial.
intro.
treat_equalities.
apply H2.
Col.
apply out_trivial.
intro.
treat_equalities.
apply H2.
Col.

eapply l11_13.
apply conga_comm.
apply conga_sym.
apply H32.

eapply outer_transitivity_between.
apply between_symmetry.
apply H16.
apply between_symmetry.
assumption.
assumption.
auto.
apply between_symmetry.
assumption.
auto.
intro.
treat_equalities.
unfold two_sides in H14.
spliter.
apply H13.
Col.
assumption.
spliter.

induction(eq_dec_points A C).
treat_equalities.

unfold out in H.
spliter.

assert(HH:= H0).
unfold one_side in HH.
ex_and HH T.
unfold two_sides in *.
spliter.

induction H4.
assert(two_sides P A B D).
unfold two_sides.
repeat split.
auto.
assumption.
assumption.
exists A.
split.
Col.
assumption.
apply l9_9 in H14.
contradiction.

induction H4.
eapply l11_10.
apply (conga_refl B A P).
auto.
auto.
apply out_trivial.
auto.
apply out_trivial.
auto.
unfold out.
repeat split.
auto.
auto.
left.
assumption.
apply out_trivial.
auto.
eapply l11_10.
apply (conga_refl B A P).
auto.
auto.
apply out_trivial.
auto.
apply out_trivial.
auto.
unfold out.
repeat split.
auto.
auto.
right.
apply between_symmetry.
assumption.
apply out_trivial.
auto.

unfold one_side in H0.
ex_and H0 T.
unfold two_sides in *.
spliter.

apply False_ind.
apply H7.
apply col_permutation_1.
eapply (col_transitivity_1 _ C).
assumption.
Col.
unfold out in H.
spliter.
induction H14; apply bet_col in H14; Col.
Qed.

Lemma l12_22_aux : forall A B C D P, Distincts P A C -> Bet P A C -> one_side P A B D -> Conga B A P D C P -> Par A B C D.
intros.
prolong B A B' B A .
unfold Distincts in H.
spliter.

assert(Conga P A B C A B').
apply l11_14.
assumption.
repeat split; auto.
assumption.
repeat split.
unfold Conga in H2.
tauto.
intro.
treat_equalities.
unfold Conga in H2.
tauto.
intro.
treat_equalities.
unfold Conga in H2.
tauto.

assert(Conga D C A D C P).
eapply l11_10.
apply conga_refl.
3: apply out_trivial.
unfold Conga in H2.
tauto.
5:apply out_trivial.
auto.
unfold Conga in H2.
tauto.
apply between_symmetry in H0.
apply bet_out in H0.
assumption.
auto.
auto.
apply out_trivial.
unfold Conga in H2.
tauto.
auto.

assert(Par A B' C D).
eapply l12_21_b.

assert(~Col B P A).
unfold one_side in H1.
ex_and H1 T.
unfold two_sides in H1.
tauto.

assert(two_sides P A B B').
unfold two_sides.
repeat split.
auto.
assumption.
intro.
apply H9.
apply col_permutation_1.
eapply (col_transitivity_1 _ B').
intro.
treat_equalities.
unfold Conga in H2.
tauto.
apply bet_col in H3.
Col.
Col.
exists A.
split.
Col.
assumption.
apply l9_2.
eapply l9_8_2.
eapply col_two_sides.
3:apply invert_two_sides.
3: apply H10.
apply bet_col in H0.
Col.
assumption.
eapply col_one_side.
3: apply invert_one_side.
3: apply H1.
apply bet_col in H0.
Col.
assumption.
eapply conga_trans.
apply conga_sym.
apply conga_comm.
apply H7.
eapply conga_trans.
apply H2.
apply conga_sym.
assumption.
apply parallel_symmetry.
eapply par_col_par.
2: apply parallel_symmetry.
2:apply H9.
unfold Conga in H2.
spliter.
auto.
apply bet_col in H3.
Col.
Qed.

Lemma l12_22_b : forall A B C D P, out P A C -> one_side P A B D -> Conga B A P D C P -> Par A B C D.
intros.

induction(eq_dec_points A C).
subst C.
unfold Par.
right.
repeat split.
unfold Conga in H1.
spliter.
auto.
unfold Conga in H1.
spliter.
auto.
Col.
apply conga_comm in H1.
apply l11_22_aux in H1.
induction H1.
apply out_col in H1.
Col.
apply l9_9 in H1.
contradiction.

unfold out in H.
spliter.

induction H4.
eapply l12_22_aux.
2:apply H4.
repeat split; auto.
assumption.
assumption.
apply parallel_symmetry.

eapply l12_22_aux.
2:apply H4.
repeat split; auto.

eapply (col_one_side _ A).
apply bet_col in H4.
Col.
auto.
apply one_side_symmetry.
assumption.
apply conga_sym.
assumption.
Qed.

Lemma l11_22 : forall A B C D P, out P A C -> one_side P A B D -> (Conga B A P D C P <-> Par A B C D).
intros.
split;
intro.
eapply (l12_22_b _ _ _ _ P); assumption.
apply l12_22_a; assumption.
Qed.


Lemma l12_23 : forall A B C, ~Col A B C -> exists B', exists C' , two_sides A C B B' /\ two_sides A B C C' /\
                                                                  Bet B' A C' /\ Conga A B C B A C' /\ Conga A C B C A B'.
intros.

assert(exists B0, is_midpoint B0 A B) by (apply midpoint_existence).
assert(exists C0, is_midpoint C0 A C) by (apply midpoint_existence).
ex_and H0 B0.
ex_and H1 C0.
prolong B C0 B' B C0.
prolong C B0 C' C B0.
exists B'.
exists C'.

assert(two_sides A C B B').

eapply mid_two_sides.
intro.
treat_equalities.
apply H.
Col.
apply H0.

intro.
apply H.
Col.
split.
assumption.
Cong.

assert(two_sides A B C C').

eapply mid_two_sides.
intro.
treat_equalities.
apply H.
Col.
apply H2.
assumption.
split.
assumption.
Cong.

split.
assumption.
split.
assumption.

assert(Par A B' C B).
eapply l12_17.
intro.
treat_equalities.

assert(C0 = B0).
eapply l7_17.
2: apply H2.
split.
apply between_symmetry.
assumption.
Cong.
subst C0.
assert(B=C).
eapply symmetric_point_unicity.
apply H2.
assumption.
subst C.
apply H.
Col.
apply H0.
split.
apply between_symmetry.
assumption.
Cong.

assert(Par A C' B C).
eapply l12_17.
intro.
treat_equalities.

assert(C0 = B0).
eapply l7_17.
apply H0.
split.
apply between_symmetry.
assumption.
Cong.
subst C0.
assert(B=C).
eapply symmetric_point_unicity.
apply H2.
assumption.
subst C.
apply H.
Col.
apply H2.
split.
apply between_symmetry.
assumption.
Cong.

assert(Par A B' A C').
eapply par_trans.
apply H8.
apply parallel_symmetry.
apply parallel_right_comm.
assumption.
apply par_id in H10.

assert(one_side A C B0 C').
eapply out_one_side.
intro.
treat_equalities.
apply H.
Col.
intro.
apply H.
eapply (col_transitivity_1 _ B0).
intro.
treat_equalities;
unfold two_sides.
apply H.
Col.
unfold is_midpoint in H2.
spliter.
apply bet_col in H2.
Col.
Col.
apply col_trivial_2.
unfold out.
repeat split.
intro.
treat_equalities.
unfold two_sides in H7.
spliter.
ex_and H11 T.
apply between_identity in H12.
subst T.
contradiction.
intro.
treat_equalities;
repeat split.
unfold two_sides in H7.
spliter.
unfold is_midpoint in H2.
spliter.
apply bet_col in H2.
apply H7.
Col.
left.
assumption.

assert(one_side A C B0 B).
eapply out_one_side.
intro.
treat_equalities.
apply H.
Col.
intro.
apply H.
eapply (col_transitivity_1 _ B0).
intro.
treat_equalities;
unfold two_sides.
apply H.
Col.
unfold is_midpoint in H2.
spliter.
apply bet_col in H2.
Col.
Col.
apply col_trivial_3.
unfold out.
repeat split.
intro.
treat_equalities.
unfold two_sides in H7.
tauto.
intro.
treat_equalities;
repeat split.
unfold two_sides in H7.
tauto.
unfold is_midpoint in H2.
spliter.
left.
assumption.

assert(one_side A C B C').
eapply one_side_transitivity.
2:apply H11;

intro.
apply one_side_symmetry.
assumption.

assert(two_sides A C B' C').
apply l9_2.
eapply l9_8_2.
apply H6.
assumption.

split.
unfold two_sides in H14.
spliter.
ex_and H17 T.
assert(A = T).

eapply (inter_unicity A C B' C').
Col.
Col.
Col.
apply bet_col in H18.
Col.
intro.
apply H15.
Col.
intro.
treat_equalities.
contradiction.
subst T.
assumption.

split.
apply l9_2 in H7.

assert(HH:= l12_21_a A C' B C H7 H9).
apply conga_comm.
apply conga_sym.
assumption.

apply parallel_symmetry in H8.
apply invert_two_sides in H6.
assert(HH:= l12_21_a C B A B' H6 H8).
apply conga_comm.
assumption.
Qed.

End T12.