Library plane

Require Export orthogonality.

Section T9.

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.

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


Definition two_sides := fun A B P Q =>
  A<>B /\ ~ Col P A B /\ ~ Col Q A B /\ exists T, Col T A B /\ Bet P T Q.

Lemma l9_2 : forall A B P Q, two_sides A B P Q -> two_sides A B Q P.
unfold two_sides.
intros.
spliter.
repeat split;try assumption.
ex_and H2 T.
exists T.
split;
Between.
Qed.

Lemma inter_unicity : forall A B X Y M N, Col A B M-> Col X Y M -> Col A B N -> Col X Y N ->
                             ~ Col A X B -> X <> Y -> M = N.
intros.
eapply l6_21.
3:apply H.
4: apply H0.
intro.
apply H3.
apply col_permutation_5.
assumption.
assumption.
assumption.
assumption.
Qed.

Lemma col2 : forall A B X Y, A <> B -> Col A B X -> Col A B Y -> Col A X Y.
intros.
eapply col_transitivity_1.
apply H.
assumption.
assumption.
Qed.

Lemma colx : forall A B M N X, A <> B -> N <> M -> X <> M -> Col A B M -> Col A B N -> Col M N X -> Col A B X.
intros.
assert (Col A M N).
eapply col2.
apply H.
assumption.
assumption.

assert(Col B M N).
eapply (col2 B A).
auto.
apply col_permutation_4.
assumption.
apply col_permutation_4.
assumption.

assert (Col M A X).
eapply (col2 M N).
auto.
apply col_permutation_1.
assumption.
assumption.

assert(Col M B X).
eapply (col2 M N).
auto.
apply col_permutation_1.
assumption.
assumption.
apply col_permutation_2 in H6.
apply col_permutation_2 in H7.
apply col_permutation_1.

eapply (col2).
apply H1.
assumption.
apply col_permutation_2.
assumption.
Qed.

Lemma l9_3 : forall P Q A C M R B,
 two_sides P Q A C -> Col M P Q ->
 is_midpoint M A C -> Col R P Q ->
 out R A B -> two_sides P Q B C.
Proof.

intros.
unfold two_sides in *.
spliter.
ex_and H6 T.

assert (A <> C).
intro.
subst C.
eapply l7_3 in H1.
subst M.
apply H4.
assumption.

assert (T = M).
eapply inter_unicity.
apply col_permutation_1.
apply H6.
unfold Col.
right; left.
apply H7.
apply col_permutation_1.
assumption.
unfold Col.
right;left.
apply mid_bet.
assumption.
intro.
apply H5.
apply col_permutation_4.
assumption.
auto.
subst T.

repeat split.
assumption.
2:assumption.

induction(eq_dec_points C M).
subst M.
intro.
apply H5.
assumption.

intro.
clear H0.

assert (B <> R).
intro.
subst B.
unfold out in H3.
spliter.
absurde.

assert (Col P R B).
eapply col_transitivity_1.
apply H.
apply col_permutation_1.
assumption.
apply col_permutation_1.
assumption.

assert (Col P R A).
induction (eq_dec_points P B).
subst B.
unfold out in H3.
spliter.
induction H13.
unfold Col.
right; left.
apply H13.
unfold Col.
right; right.
apply between_symmetry.
assumption.

apply col_permutation_2.
eapply col_transitivity_2.
apply H0.
unfold Col.
unfold out in H3.
spliter.
induction H14.
right; left.
assumption.
right; right.
apply between_symmetry.
assumption.
apply col_permutation_3.
assumption.

induction (eq_dec_points P R).
subst R.
apply H4.
apply col_permutation_2.
eapply (col_transitivity_1 _ B).
unfold out in H3.
spliter.
auto.
apply col_permutation_4.
assumption.
unfold out in H3.
spliter.
unfold Col.
induction H14.
right; left.
apply between_symmetry.
assumption.
left.
assumption.

assert (Col P B A ).
eapply col_transitivity_1.
apply H13.
assumption.
assumption.
induction (eq_dec_points P B).
subst B.

apply H4.
apply col_permutation_2.
eapply (col_transitivity_1 _ R).
apply H0.
apply col_permutation_4.
assumption.
unfold out in H3.
spliter.
unfold Col.
induction H16.
right; left.
assumption.
right;right.
apply between_symmetry.
assumption.
apply H4.
apply col_permutation_2.
eapply col_transitivity_1.
apply H15.
apply col_permutation_4.
assumption.
assumption.

induction H3.
spliter.
induction H10.

Focus 2.

assert (exists X, Bet B X C /\ Bet M X R).
eapply inner_pasch.
apply H10.
apply between_symmetry.
assumption.

ex_and H11 X.
exists X.
induction (eq_dec_points M R).
subst R.
apply between_identity in H12.
subst X.
split; assumption.
induction (eq_dec_points R X).
subst X.
split; assumption.

split.

induction (eq_dec_points X M).
subst X.
assumption.

assert (Col P M R ).
eapply col_transitivity_1.
apply H.
apply col_permutation_1.
assumption.
apply col_permutation_1.
assumption.

assert (Col X P Q).
apply col_permutation_2.
eapply colx.
assumption.
apply H13.
auto.
apply col_permutation_1.
assumption.
apply col_permutation_1.
assumption.
unfold Col.
right; left.
assumption.
assumption.
assumption.

double B M B'.
double R M R'.
assert (Bet B' C R').
eapply l7_15.
apply H11.
apply H1.
apply H12.
apply between_symmetry.
assumption.

assert (exists X, Bet M X R' /\ Bet C X B).
eapply inner_pasch.
apply mid_bet.
apply H11.
apply between_symmetry.
assumption.
ex_and H14 X.
exists X.

split.

assert (Col P M R ).
eapply col_transitivity_1.
apply H.
apply col_permutation_1.
assumption.
apply col_permutation_1.
assumption.

assert (Col Q M R).
eapply (col_transitivity_1 _ P).
auto.
apply col_permutation_3.
assumption.
apply col_permutation_3.
assumption.

induction (eq_dec_points M X).
subst X.
assumption.

induction (eq_dec_points M R').
subst R'.
apply between_identity in H14.
subst X.
absurde.

assert (M <> R).
intro.
subst R.

eapply (midpoint_id) in H12.
apply H19.
apply H12.
apply l7_3_2.

apply col_permutation_2.
eapply (colx _ _ M R).
assumption.
auto.
auto.
apply col_permutation_1.
assumption.
apply col_permutation_1.
assumption.

eapply (col_transitivity_1).
apply H20.
apply col_trivial_2.
eapply col_transitivity_1.
apply H19.
unfold Col.
right; right.
apply mid_bet.
assumption.
unfold Col.
right; left.
apply between_symmetry.
assumption.

apply between_symmetry.
assumption.
Qed.

Definition is_symmetric (A A' C : Tpoint) := is_midpoint C A A'.

Lemma sym_sym : forall A C A', is_symmetric A A' C -> is_symmetric A' A C.
unfold is_symmetric.
intros.
apply l7_2.
assumption.
Qed.

Lemma distinct : forall P Q R : Tpoint, P <> Q -> (R <> P \/ R <> Q).
Proof.
intros.
assert (~ (R = P /\ R = Q) -> (R <> P \/ R <> Q)).
intro.
induction (eq_dec_points P R).
subst R.
right.
intro.
apply H0.
split.
reflexivity.
assumption.
left.
intro.
apply H1.
subst R.
reflexivity.
apply H0.
intro.
spliter.
subst P.
subst Q.
apply H.
reflexivity.
Qed.

Lemma diff_col_ex : forall A B, exists C, A <> C /\ B <> C /\ Col A B C.
intros.
assert (exists C, Bet A B C /\ B <> C).
apply point_construction_different.
ex_and H C.
exists C.
split.
intro.
induction (eq_dec_points A B).
subst B.
subst C.
apply H0.
reflexivity.
subst C.
apply between_identity in H.
subst B.
apply H0.
reflexivity.
split.
assumption.
unfold Col.
left.
assumption.
Qed.

Lemma diff_bet_ex3 : forall A B C,
 Bet A B C ->
 exists D, A <> D /\ B <> D /\ C <> D /\ Col A B D.
Proof.
intros.

induction (eq_dec_points A B).
induction (eq_dec_points B C).

assert (exists D, Bet B C D /\ C <> D).
apply point_construction_different.
ex_and H2 D.
exists D.
repeat split.
subst C.
subst A.
assumption.
subst A.
subst C.
assumption.
assumption.
unfold Col.
left.
subst A.
subst C.
assumption.

assert (exists D, Bet B C D /\ C <> D).
apply point_construction_different.
ex_and H2 D.
exists D.
repeat split.
intro.
subst D.

apply between_symmetry in H.
apply H1.
eapply between_egality.
apply H2.
apply H.
intro.
subst D.
subst A.
apply between_identity in H2.
apply H3.
subst B.
reflexivity.
assumption.
unfold Col.
left.
eapply outer_transitivity_between.
apply H.
apply H2.
assumption.

induction (eq_dec_points B C).
subst C.
cut(exists D : Tpoint, A <> D /\ B <> D /\ Col A B D).
intro.
ex_and H1 D.
exists D.
repeat split.
assumption.
assumption.
assumption.
assumption.
apply diff_col_ex.

assert (exists D, Bet B C D /\ C <> D).
apply point_construction_different.
ex_and H2 D.
exists D.
repeat split.
intro.
subst D.
assert (B = C).
eapply between_egality.
apply H2.
apply between_symmetry.
assumption.
apply H1.
assumption.
intro.
subst D.
apply between_identity in H2.
subst C.
apply H1.
reflexivity.
assumption.
unfold Col.
left.
eapply outer_transitivity_between.
apply H.
assumption.
assumption.
Qed.

Lemma diff_col_ex3 : forall A B C,
 Col A B C -> exists D, A <> D /\ B <> D /\ C <> D /\ Col A B D.
Proof.
intros.

assert(cas1 := diff_bet_ex3 A B C).
assert(cas2 := diff_bet_ex3 B C A).
assert(cas3 := diff_bet_ex3 C A B).
unfold Col in H.
induction H.
apply (diff_bet_ex3 A B C).
assumption.
induction H.
assert (HH:=H).

induction (eq_dec_points B C).
subst C.
assert (exists C, A <> C /\ B <> C /\ Col A B C).
apply (diff_col_ex).
ex_and H0 D.
exists D.
repeat split; assumption.
apply cas2 in HH.
ex_and HH D.
exists D.
repeat split; try assumption.
apply col_permutation_2.
eapply col_transitivity_1.
apply H0.
assumption.
unfold Col.
left.
assumption.

induction (eq_dec_points A C).
subst C.
assert (exists C, A <> C /\ B <> C /\ Col A B C).
apply (diff_col_ex).
ex_and H0 D.
exists D.
repeat split; assumption.
assert (HH:=H).
apply cas3 in HH.
ex_and HH D.
exists D.
repeat split; try assumption.
apply col_permutation_5.
eapply col_transitivity_1.
apply H0.
apply col_permutation_4.
assumption.
unfold Col.
right;right.
apply between_symmetry.
assumption.
Qed.

Lemma mid_preserve_col : forall A B C M A' B' C',
   Col A B C ->
  is_midpoint M A A' ->
  is_midpoint M B B' ->
  is_midpoint M C C' ->
  Col A' B' C'.
Proof.
intros.
induction H.
assert (Bet A' B' C').
eapply l7_15.
apply H0.
apply H1.
apply H2.
assumption.
unfold Col.
left.
assumption.
induction H.
assert (Bet B' C' A').
eapply l7_15.
apply H1.
apply H2.
apply H0.
assumption.
unfold Col.
right; left.
assumption.
assert (Bet C' A' B').
eapply l7_15.
apply H2.
apply H0.
apply H1.
assumption.
unfold Col.
right; right.
assumption.
Qed.

Lemma per_mid_per : forall A B X Y M,
   A <> B -> Per X A B -> is_midpoint M A B -> is_midpoint M X Y ->
   Cong A X B Y /\ Per Y B A.
Proof.
intros.
assert (Cong A X B Y).
eapply l7_13.
apply l7_2.
apply H1.
apply l7_2.
assumption.
split.
assumption.

unfold Per in H0.
ex_and H0 B'.

double A B A'.

assert (Cong B X A Y).
eapply l7_13.
apply H1.
apply l7_2.
assumption.

assert (OFSC B A B' X A B A' Y).
unfold OFSC.
repeat split.
apply mid_bet.
assumption.
apply mid_bet.
assumption.
apply cong_pseudo_reflexivity.
unfold is_midpoint in *.
spliter.
eapply cong_transitivity.
apply cong_symmetry.
apply H8.
apply cong_left_commutativity.
assumption.
assumption.
assumption.
unfold Per.
exists A'.
split.
assumption.
assert (Cong B' X A' Y).
eapply five_segments_with_def.
apply H7.
intro.
apply H.
subst B.
reflexivity.
eapply cong_transitivity.
apply cong_commutativity.
apply cong_symmetry.
apply H6.
eapply cong_transitivity.
apply H4.
apply cong_commutativity.
assumption.
Qed.

Lemma perp_in_perp : forall A B C D X,
 Perp_in X A B C D -> Perp X B C D \/ Perp A X C D.
Proof.
intros.
induction (eq_dec_points X A).
subst X.
left.
unfold Perp.
exists A.
assumption.
right.
unfold Perp.
exists X.
unfold Perp_in in *.
spliter.
repeat split.
intro.
apply H0.
subst X.
reflexivity.
assumption.
apply col_trivial_3.
assumption.
intros.
apply H4.
apply col_permutation_2.
eapply col_transitivity_1.
intro.
apply H0.
apply sym_equal.
apply H7.
apply col_permutation_4.
assumption.
apply col_permutation_1.
assumption.
assumption.
Qed.

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

unfold Perp in *.
ex_elim H M.
exists M.
unfold Perp_in in *.
spliter.
repeat split.

assumption.
assumption.
eapply col_col.
apply H.
Col.
assumption.
assumption.
assumption.

intros.
apply H6.
eapply col_col.
apply H0.
Col.
eapply col_col.
apply H.
assumption.
assumption.
Col.
eapply col_col.
apply H.
assumption.
assumption.
Col.
assumption.
Qed.

Lemma sym_preserve_diff : forall A B M A' B',
 A <> B -> is_midpoint M A A' -> is_midpoint M B B' -> A'<> B'.
Proof.
intros.
intro.
subst B'.
assert (A = B).
eapply l7_9.
apply H0.
assumption.
contradiction.
Qed.

Lemma perp_col2 : forall P Q R S A B,
 Perp P Q A B -> Col P Q R -> Col P Q S -> R <> S ->
 Perp R S A B.
Proof.
intros.

induction (eq_dec_points P R).
induction (eq_dec_points P S).
subst R.
subst S.
absurde.
subst P.

eapply perp_col.
2:apply H.
assumption.
assumption.

induction (eq_dec_points Q R).
induction (eq_dec_points Q S).
subst R.
subst Q.
absurde.
subst Q.
eapply perp_col.
2:apply perp_left_comm.
2 :apply H.
assumption.
apply col_permutation_4.
assumption.

eapply perp_col.
2: apply perp_left_comm.
2: eapply perp_col.
3:apply H.
assumption.
assumption.
assumption.
eapply col_col.
apply perp_distinct in H.
spliter.
apply H.
assumption.
apply col_trivial_3.
assumption.
Qed.

Lemma l9_4_1_aux : forall P Q A C R S M,
 le S C R A ->
 two_sides P Q A C -> Col R P Q -> Perp P Q A R -> Col S P Q ->
 Perp P Q C S -> is_midpoint M R S ->
 (forall U C',is_midpoint M U C' -> (out R U A <-> out S C C')).
Proof.
intros.
induction (eq_dec_points R S).

subst S.
apply l7_3 in H5.
subst R.
unfold two_sides in H0.
spliter.
ex_and H8 T.
assert (T=M).
eapply inter_unicity.
apply col_permutation_1.
apply H8.
unfold Col.
right; left.
apply H9.
apply col_permutation_1.
assumption.
induction (eq_dec_points M P).
assert(Q <> M).
intro.
subst P.
subst Q.
apply perp_distinct in H2.
apply H0.
reflexivity.
assert(M <> Q).
intro.
apply H11.
subst Q.
reflexivity.
assert (Perp Q M A M).
eapply perp_col.
assumption.
apply perp_left_comm.
apply H2.
apply col_permutation_3.
assumption.
apply perp_left_comm in H13.
eapply perp_id in H13.
apply perp_in_comm in H13.
eapply perp_in_per in H13.
assert (Perp Q M C M).
eapply perp_col.
assumption.
apply perp_left_comm.
apply H4.
apply col_permutation_3.
assumption.
apply perp_left_comm in H14.
eapply perp_id in H14.
apply perp_in_comm in H14.
eapply perp_in_per in H14.
eapply per_per_col.
apply l8_2.
apply H14.
assumption.
apply l8_2.
assumption.
assumption.
assumption.
assert (Perp P M A M).
eapply perp_col.
intro.
apply H10.
subst P.
reflexivity.
apply H2.
apply col_permutation_1.
assumption.
apply perp_left_comm in H11.
eapply perp_id in H11.
apply perp_in_comm in H11.
eapply perp_in_per in H11.
assert (Perp P M C M).
eapply perp_col.
intro.
apply H10.
subst P.
reflexivity.
apply H4.
apply col_permutation_1.
assumption.
apply perp_left_comm in H12.
eapply perp_id in H12.
apply perp_in_comm in H12.
eapply perp_in_per in H12.
eapply per_per_col.
apply l8_2.
apply H12.
assumption.
apply l8_2.
assumption.
assumption.
assumption.
intro.
apply H7.
apply col_permutation_4.
assumption.
intro.
subst C.
apply between_identity in H9.
subst A.
apply H5.
assumption.

subst T.
split.
intro.
unfold out in *.
spliter.
repeat split.
intro.
subst C.
apply perp_distinct in H4.
spliter.
absurde.
intro.
subst C'.
apply l7_2 in H6.
eapply (midpoint_id _ _ M) in H6.
apply H10.
apply sym_equal.
apply H6.
apply l7_3_2.
induction H12.
assert (Bet U M C).
eapply between_exchange3.
apply between_symmetry.
apply H12.
assumption.
unfold is_midpoint in H13.
spliter.
eapply l5_2.
apply H10.
assumption.
apply mid_bet.
assumption.
assert (Bet U M C).
eapply outer_transitivity_between2.
apply between_symmetry.
apply H12.
assumption.
assumption.
eapply l5_2.
apply H10.
assumption.
unfold is_midpoint in H6.
spliter.
assumption.
intro.
unfold out in *.
spliter.
repeat split.
intro.
subst U.
eapply is_midpoint_id in H6.
subst C'.
apply H11.
reflexivity.
intro.
subst A.
apply perp_distinct in H2.
spliter.
apply H13.
reflexivity.
unfold is_midpoint in H6.
spliter.
assert (Bet A M C').
induction H12.

eapply outer_transitivity_between.
apply H9.
assumption.
intro.
apply H10.
subst C.
reflexivity.
eapply between_inner_transitivity.
apply H9.
assumption.
eapply l5_2.
apply H11.
apply between_symmetry.
assumption.
apply between_symmetry.
assumption.


unfold le in H.
ex_and H D.

assert (C <> S).
intro.
subst S.
apply perp_distinct in H4.
spliter.
absurde.

assert (R <> D).
intro.
subst D.
apply cong_identity in H8.
apply H9.
subst S.
reflexivity.

assert (Perp R S A R).
eapply perp_col2.
apply H2.
apply col_permutation_1.
assumption.
apply col_permutation_1.
assumption.
assumption.

assert(exists M, is_midpoint M S R /\ is_midpoint M C D).
unfold two_sides in H0.
spliter.
ex_and H14 T.
eapply (l8_24 S R C A D T).
apply perp_sym.
apply perp_left_comm.
eapply perp_col2.
apply H4.
apply col_permutation_1.
assumption.
apply col_permutation_1.
assumption.
assumption.
apply perp_right_comm.
apply perp_sym.
assumption.
eapply col_col.
apply H0.
apply col_permutation_1.
assumption.
apply col_permutation_1.
assumption.
apply col_permutation_1.
assumption.
apply between_symmetry.
assumption.
assumption.
assumption.

ex_and H12 M'.
apply l7_2 in H12.
assert (M = M').
eapply l7_17.
apply H5.
apply H12.
subst M'.

split.
intro.
unfold out in H14.
spliter.
unfold out.
repeat split.
assumption.
eapply sym_preserve_diff.
2:apply H6.
apply H14.
assumption.

induction H16.

Focus 2.
left.
eapply l7_15.
apply H5.
apply l7_2.
apply H13.
apply H6.
eapply between_exchange4.
apply H.
apply H16.

assert(Bet R U D \/ Bet R D U).
eapply l5_3.
apply H16.
assumption.
induction H17.
right.
eapply l7_15.
apply H5.
apply H6.
apply l7_2.
apply H13.
assumption.
left.
eapply l7_15.
apply H5.
apply l7_2.
apply H13.
apply H6.
assumption.

unfold out.
intros.
spliter.
repeat split.
eapply sym_preserve_diff.
apply H15.
apply l7_2.
apply H6.
apply l7_2.
assumption.
intro.
subst R.
apply perp_distinct in H11.
spliter.
absurde.

induction H16.
eapply l5_1.
apply H10.
eapply l7_15.
apply l7_2.
apply H12.
apply H13.
apply l7_2.
apply H6.
assumption.
assumption.
left.
eapply between_exchange4.
eapply l7_15.
apply l7_2.
apply H12.
apply l7_2.
apply H6.
apply H13.
assumption.
assumption.
Qed.

Lemma per_col_eq : forall A B C, Per A B C -> Col A B C -> B <> C -> A = B.
Proof.
intros.
unfold Per in H.
ex_and H C'.

assert (Col A C C').
eapply col_col.
apply H1.
apply col_permutation_1.
assumption.
apply col_trivial_2.
unfold Col.
right; right.
apply between_symmetry.
apply mid_bet.
assumption.

assert (C = C' \/ is_midpoint A C C').
eapply l7_20.
apply col_permutation_4.
assumption.
assumption.
induction H4.
subst C'.
apply l7_3 in H.
contradiction.
eapply l7_17.
apply H4.
assumption.
Qed.

Lemma l9_4_1 : forall P Q A C R S M, two_sides P Q A C -> Col R P Q -> Perp P Q A R -> Col S P Q ->
Perp P Q C S -> is_midpoint M R S -> (forall U C',is_midpoint M U C' -> (out R U A <-> out S C C')).
intros.

assert (le S C R A \/ le R A S C).
apply le_cases.
induction H6.
apply (l9_4_1_aux P Q A C R S M); assumption.

assert((out R A U <-> out S C' C) -> (out R U A <-> out S C C')).
intro.
induction H7.
split.
intro.
eapply l6_6.
apply H7.
apply l6_6.
assumption.
intro.
apply l6_6.
apply H8.
apply l6_6.
assumption.
apply H7.

assert((out S C' C <-> out R A U) -> (out R A U <-> out S C' C)).
intro.
induction H8.
split.
intro.
apply H9.
assumption.
intro.
apply H8.
assumption.
apply H8.

eapply (l9_4_1_aux).
assumption.
apply l9_2.
apply H.
assumption.
assumption.
assumption.
assumption.
apply l7_2.
apply H4.
apply l7_2.
assumption.
Qed.

Lemma mid_two_sides : forall A B M X Y, A <> B -> is_midpoint M A B -> ~Col A B X -> is_midpoint M X Y -> two_sides A B X Y.
intros.
unfold two_sides.
repeat split.
assumption.
intro.
apply col_permutation_1 in H3.
contradiction.
intro.
apply H1.
unfold is_midpoint in *.
spliter.

assert (Col A M Y).
eapply col_transitivity_1.
apply H.
unfold Col.
right; left.
apply between_symmetry.
assumption.
apply col_permutation_1.
assumption.

assert (Col B M Y).
eapply col_transitivity_1.
intro.
apply H.
apply sym_equal.
apply H7.
unfold Col.
right; left.
assumption.
apply col_permutation_3.
assumption.

assert (Y <> M).
intro.
subst M.
apply cong_identity in H4.
subst Y.
apply H1.
apply col_permutation_1.
assumption.

assert (Col Y A X).
eapply col_transitivity_1.
apply H8.
apply col_permutation_3.
assumption.
unfold Col.
left.
apply between_symmetry.
assumption.

assert (Col Y B X).
eapply col_transitivity_1.
apply H8.
apply col_permutation_3.
assumption.
unfold Col.
left.
apply between_symmetry.
assumption.

assert (X <> Y).
intro.
subst Y.
apply between_identity in H2.
contradiction.

apply col_permutation_1.
eapply col_transitivity_1.
apply H11.
apply col_permutation_2.
assumption.
apply col_permutation_2.
assumption.
exists M.
unfold is_midpoint in *.
spliter.
split.
unfold Col.
right; right.
apply between_symmetry.
assumption.
assumption.
Qed.

Lemma col_preserves_two_sides : forall A B C D X Y, A <> B -> C <> D -> Col A B C -> Col A B D -> two_sides A B X Y -> two_sides C D X Y.
intros.
unfold two_sides in *.
spliter.
repeat split.
assumption.
intro.
apply H4.
apply col_permutation_1.

eapply col_col.
apply H0.
apply col_permutation_1.
eapply col_transitivity_1.
intro.
apply H3.
apply sym_equal.
apply H8.
apply col_permutation_4.
assumption.
apply col_permutation_4.
assumption.
apply col_permutation_1.
assumption.
apply col_permutation_1.
eapply col_transitivity_1.
apply H.
assumption.
assumption.

intro.
apply H5.
apply col_permutation_1.

eapply col_col.
apply H0.
apply col_permutation_1.
eapply col_transitivity_1.
intro.
apply H3.
apply sym_equal.
apply H8.
apply col_permutation_4.
assumption.
apply col_permutation_4.
assumption.
apply col_permutation_1.
assumption.
apply col_permutation_1.
eapply col_transitivity_1.
apply H.
assumption.
assumption.

ex_and H6 T.
exists T.
split.

eapply col_col.
apply H3.
apply col_permutation_1.
assumption.
assumption.
assumption.
assumption.
Qed.

Lemma out_out_two_sides : forall A B X Y U V I, A <> B -> two_sides A B X Y -> Col I A B -> Col I X Y
        -> out I X U -> out I Y V -> two_sides A B U V.
intros.

unfold two_sides in *.
spliter.
repeat split.
assumption.
intro.
apply H5.
unfold out in H3.
spliter.
apply col_permutation_2.
eapply colx.
assumption.
apply H9.
assumption.
apply col_permutation_1.
assumption.
apply col_permutation_1.
assumption.
unfold Col.
induction H10.
right; left.
apply between_symmetry.
assumption.
left.
assumption.
intro.
apply H6.
unfold out in H4.
spliter.
apply col_permutation_2.
eapply colx.
assumption.
apply H9.
assumption.
apply col_permutation_1.
assumption.
apply col_permutation_1.
assumption.
unfold Col.
induction H10.
right; left.
apply between_symmetry.
assumption.
left.
assumption.

ex_and H7 T.
assert (I = T).
eapply inter_unicity.
apply col_permutation_1.
apply H1.
apply col_permutation_1.
apply H2.
apply col_permutation_1.
assumption.
unfold Col.
right; left.
apply between_symmetry.
assumption.
intro.
apply H5.
apply col_permutation_4.
assumption.
intro.
subst Y.
apply between_identity in H8.
subst X.
apply H5.
assumption.
subst I.
exists T.
split.
assumption.
unfold out in *.
spliter.
induction H12; induction H10.
assert (Bet U T Y).
eapply outer_transitivity_between2.
apply between_symmetry.
apply H12.
assumption.
assumption.
eapply outer_transitivity_between.
apply H13.
assumption.
auto.
assert (Bet U T Y).
eapply outer_transitivity_between2.
apply between_symmetry.
apply H12.
assumption.
assumption.
eapply between_inner_transitivity.
apply H13.
assumption.
assert (Bet U T Y).
eapply between_exchange3.
apply between_symmetry.
apply H12.
assumption.
eapply outer_transitivity_between.
apply H13.
assumption.
intro.
subst Y.
apply H6.
assumption.
assert (Bet V T X).
eapply between_exchange3.
apply between_symmetry.
apply H10.
apply between_symmetry.
assumption.
eapply between_exchange3.
apply between_symmetry.
apply H12.
apply between_symmetry.
assumption.
Qed.

Lemma out_out_two_sides1 : forall P Q A C M U V,
two_sides P Q A C -> Col M P Q -> Perp P Q A M ->
Perp P Q C M -> out M U A -> out M V C -> two_sides P Q U V.
intros.
eapply out_out_two_sides.
unfold two_sides in H.
spliter.
assumption.
apply H.
apply H0.
unfold two_sides in H.
spliter.
ex_and H7 T.
induction(eq_dec_points M P).

assert(M <> Q).
intro.
subst P.
subst Q.
absurde.
subst P.

apply perp_id in H1.
apply perp_in_comm in H1.
eapply perp_in_per in H1.
apply perp_id in H2.
apply perp_in_comm in H2.
eapply perp_in_per in H2.

apply col_permutation_2.
eapply per_per_col.
apply l8_2.
apply H1.
assumption.
apply l8_2.
assumption.
assumption.
assumption.

assert (Perp M P A M).
apply perp_left_comm.
eapply perp_col.
auto.
apply H1.
apply col_permutation_1.
assumption.
assert(Perp M P C M).
apply perp_left_comm.
eapply perp_col.
auto.
apply H2.
apply col_permutation_1.
assumption.
apply perp_id in H10.
apply perp_id in H11.
apply perp_in_comm in H10.
eapply perp_in_per in H10.
apply perp_in_comm in H11.
eapply perp_in_per in H11.
apply col_permutation_2.
eapply per_per_col.
apply l8_2.
apply H10.
assumption.
apply l8_2.
assumption.
assumption.
assumption.
apply l6_6.
assumption.
apply l6_6.
assumption.
Qed.

Lemma mid_preserves_col : forall A B C A' B' C' M, Col A B C -> is_midpoint M A A' -> is_midpoint M B B' -> is_midpoint M C C'
-> Col A' B' C'.
intros.
unfold Col in *.
induction H.
left.
eapply l7_15.
apply H0.
apply H1.
apply H2.
assumption.
induction H.
right; left.
eapply l7_15.
apply H1.
apply H2.
apply H0.
assumption.
right; right.
eapply l7_15.
apply H2.
apply H0.
apply H1.
assumption.
Qed.

Lemma l9_4_2_aux : forall P Q A C R S U V, le S C R A ->
two_sides P Q A C -> Col R P Q -> Perp P Q A R -> Col S P Q ->
Perp P Q C S -> out R U A -> out S V C -> two_sides P Q U V.
intros.

induction (eq_dec_points R S).
subst S.
eapply out_out_two_sides1.
apply H0.
apply H1.
assumption.
assumption.
assumption.
assumption.


assert(P <> Q).
apply perp_distinct in H4.
spliter.
assumption.

assert (two_sides R S A C).

eapply (col_preserves_two_sides P Q).
assumption.

apply H7.
apply col_permutation_1.
assumption.
apply col_permutation_1.
assumption.
assumption.

eapply (col_preserves_two_sides R S).
assumption.
assumption.

eapply col_permutation_1.

eapply col2.
apply H8.
apply col_permutation_1.
assumption.
apply col_permutation_1.
assumption.
apply col_permutation_1.
eapply (col_transitivity_1 _ P).
auto.
apply col_permutation_3.
assumption.
apply col_permutation_3.
assumption.

assert (Perp R S A R).
eapply perp_col2.
apply H2.
apply col_permutation_1.
assumption.
apply col_permutation_1.
assumption.
assumption.
assert (Perp R S C S).
eapply perp_col2.
apply H4.
apply col_permutation_1.
assumption.
apply col_permutation_1.
assumption.
assumption.

assert (HH9:=H9).
unfold two_sides in HH9.
spliter.
ex_and H15 T.

unfold le in H.
ex_and H C'.

assert (exists M, is_midpoint M S R /\ is_midpoint M C C').

eapply (l8_24 S R C A C' T).
apply perp_sym.
apply perp_left_comm.
assumption.
apply
perp_sym.
apply perp_left_comm.
assumption.
apply col_permutation_3.
assumption.
apply between_symmetry.
assumption.
assumption.
assumption.
ex_and H18 M.

double U M U'.

assert (R <> U).
intro.
subst U.
unfold out in H5.
spliter.
absurde.

assert (two_sides R S U U').

eapply mid_two_sides.
assumption.
apply l7_2.
apply H18.
intro.

apply H13.
eapply col_permutation_2.
eapply col_transitivity_1.
apply H21.
apply col_permutation_5.
assumption.
induction H5.
spliter.
induction H24.
unfold Col.
left.
assumption.
unfold Col.
right; left.
apply between_symmetry.
assumption.
assumption.

apply l9_2.
eapply l9_3.
apply l9_2.
apply H22.
unfold Col.
right; right.
apply mid_bet.
apply H18.
apply l7_2.
assumption.
apply col_trivial_3.

assert (forall X Y, is_midpoint M X Y -> (out R X A <-> out S C Y)).
eapply l9_4_1.
apply H9.
apply col_trivial_1.
assumption.
apply col_trivial_3.
assumption.
apply l7_2.
assumption.
assert (out R U A <-> out S C U').
eapply H23.
assumption.
destruct H24.

eapply l6_7.
apply l6_6.
apply H24.
assumption.
apply l6_6.
assumption.
Qed.

Lemma l9_4_2 : forall P Q A C R S U V,
two_sides P Q A C -> Col R P Q -> Perp P Q A R -> Col S P Q ->
Perp P Q C S -> out R U A -> out S V C -> two_sides P Q U V.
intros.

assert( le S C R A \/ le R A S C).
apply le_cases.
induction H6.
eapply l9_4_2_aux.
apply H6.
assumption.
assumption.
assumption.
assumption.
assumption.
assumption.
assumption.

apply l9_2.

eapply l9_4_2_aux.
apply H6.
apply l9_2.
assumption.
assumption.
assumption.
assumption.
assumption.
assumption.
assumption.
Qed.

Lemma l9_5 : forall P Q A C R B,
 two_sides P Q A C -> Col R P Q -> out R A B -> two_sides P Q B C.
intros.

assert (P <> Q).
unfold two_sides in H.
spliter.
assumption.

assert(exists A0, Col P Q A0 /\ Perp P Q A A0).
eapply l8_18_existence.
intro.
unfold two_sides in H.
spliter.
apply H4.
apply col_permutation_2.
assumption.

assert(exists C0, Col P Q C0 /\ Perp P Q C C0).
eapply l8_18_existence.
unfold two_sides in H.
spliter.
intro.
apply H5.
apply col_permutation_2.
assumption.

assert(exists B0, Col P Q B0 /\ Perp P Q B B0).
eapply l8_18_existence.

assert (HH1:=H1).
unfold out in HH1.
unfold two_sides in H.
spliter.
intro.

assert (Col P B R).
eapply col2.
apply H.
assumption.
apply col_permutation_1.
assumption.

assert (R <> B).
intro.
subst B.
absurde.

assert(Col R P A ).
eapply col2.
apply H13.
eapply col_permutation_3.
assumption.
apply col_permutation_5.
apply out_col.
assumption.

apply H8.
eapply col_permutation_2.
eapply col2.

apply H.
apply col_trivial_2.

eapply colx.
assumption.
3:apply col_permutation_1.
3:apply H0.
3: apply H11.
assumption.
assumption.
apply col_permutation_5.
apply out_col.
assumption.

ex_and H3 A'.
ex_and H4 C'.
ex_and H5 B'.

assert (exists M, is_midpoint M A' C').
apply midpoint_existence.
ex_and H9 M.

double A M D.

assert (out C' D C <-> out A' A A).
eapply l9_4_1.
apply l9_2.
apply H.
apply col_permutation_2.
assumption.
assumption.
apply col_permutation_2.
assumption.
assumption.
apply l7_2.
apply H10.
apply l7_2.
assumption.

destruct H11.
assert (out C' D C).
apply H12.
unfold out.
repeat split.
intro.
subst A'.
apply perp_distinct in H6.
spliter.
absurde.

intro.
subst A'.
apply perp_distinct in H6.
spliter.
absurde.
left.
apply between_trivial.

assert (two_sides P Q A D).
eapply l9_4_2.
apply H.
apply col_permutation_2.
apply H3.
assumption.
apply col_permutation_2.
apply H4.
apply H7.
unfold out.
repeat split.
intro.
subst A'.
apply perp_distinct in H6.
spliter.
absurde.
intro.
subst A'.
apply perp_distinct in H6.
spliter.
absurde.
left.
apply between_trivial.
assumption.

assert (two_sides P Q B D).
eapply l9_3.

apply H14.
2:apply H9.
2: apply H0.2:assumption.

induction (eq_dec_points A' C').
subst C'.
apply l7_3 in H10.
subst A'.
apply col_permutation_2.
assumption.

eapply col_permutation_2.
eapply colx.

assumption.

apply H15.
intro.
subst C'.
eapply l7_2 in H10.
eapply midpoint_id in H10.
apply H15.
apply sym_equal.
apply H10.

apply l7_3_2.
assumption.
assumption.
unfold Col.
right;left.
apply mid_bet.
assumption.
try assumption.

eapply l9_4_2.
apply H15.
2: apply H8.
apply col_permutation_2.
assumption.
apply col_permutation_2.
apply H4.
apply perp_sym.
apply perp_left_comm.
eapply perp_col.
intro.
subst D.
unfold out in H13.
spliter.
absurde.
apply perp_sym.
apply perp_right_comm.
apply H7.
apply col_permutation_5.
apply out_col.
assumption.
eapply out_trivial.
intro.
subst B.
apply perp_distinct in H8.
spliter.
absurde.
apply l6_6.
assumption.
Qed.

Lemma outer_pasch : forall A B C P Q,
 Bet A C P -> Bet B Q C -> exists X, Bet A X B /\ Bet P Q X.
Proof.
intros.
induction(classic (Col P Q C)).
induction(classic (Bet P Q C)).
exists A.
split.
apply between_symmetry.
apply between_trivial.
eapply between_exchange4.
apply H2.
apply between_symmetry.
assumption.
assert (out Q P C).
eapply l6_4_2.
split;trivial.
exists B.
split.
apply between_trivial.
unfold out in H3.
spliter.
induction H5.
eapply between_exchange3.
apply between_symmetry.
apply H5.
apply between_symmetry.
assumption.
eapply outer_transitivity_between2.
apply between_symmetry.
apply H5.
apply between_symmetry.
assumption.
assumption.

induction (eq_dec_points B Q).
subst Q.
exists B.
split; apply between_trivial.

assert (A <> P).
intro.
subst P.
apply between_identity in H.
subst C.
apply False_ind.
apply H1.
apply col_trivial_3.

assert (P <> Q).
intro.
subst Q.
apply H1.
apply col_trivial_1.

assert (P <> B).
intro.
subst P.
apply H1.
unfold Col.
left.
assumption.

assert(two_sides P Q C B).
unfold two_sides.
repeat split.
assumption.
intro.
apply H1.
apply col_permutation_1.
assumption.
intro.
apply H1.

assert (Col B P C ).
eapply col2.
apply H2.
apply col_permutation_5.
assumption.
unfold Col.
left.
assumption.

eapply col2.
apply H5.
apply col_permutation_4.
assumption.
apply col_permutation_4.
assumption.
exists Q.
split.
apply col_trivial_3.
apply between_symmetry.
assumption.
assert (two_sides P Q A B).
eapply l9_5.
apply H6.
apply col_trivial_1.
unfold out.
repeat split.
intro.
subst P.
apply H1.
apply col_trivial_3.
assumption.
left.
apply between_symmetry.
assumption.

unfold two_sides in H7.
spliter.
ex_and H10 X.
exists X.

split.
assumption.

assert (exists T, Bet X T P /\ Bet C T B).
eapply inner_pasch.
apply between_symmetry.
apply H11.
apply between_symmetry.
assumption.

ex_and H12 T.

assert (T = Q).
eapply inter_unicity.
unfold Col.
right; left.
apply H12.
unfold Col.
right; left.
apply H13.
apply col_permutation_4.
assumption.
unfold Col.
right; left.
apply between_symmetry.
assumption.
intro.
apply H9.
eapply col_permutation_2.
eapply col2.
2: apply col_permutation_4.
2:apply H10.
intro.
subst X.

apply H8.
eapply colx.
assumption.
3: unfold Col.
3:right; left.
3:apply between_symmetry.
3:apply H.
3: unfold Col.
3: left.
3: apply H11.
intro.
subst C.
apply between_identity in H13.
subst T.
apply between_identity in H12.
subst P.
apply H1.
apply col_trivial_3.
intro.
subst Q.
unfold two_sides in H6.
spliter.
apply H15.
apply col_trivial_3.
unfold Col.
right; left.
assumption.
apply col_permutation_5.
assumption.
intro.
subst C.
apply between_identity in H13.
subst T.
apply between_identity in H0.
subst Q.
apply H1.
apply col_trivial_2.
subst T.
apply between_symmetry.
assumption.
Qed.

Definition one_side := fun P Q A B =>
 exists C, two_sides P Q A C /\ two_sides P Q B C.

Lemma l9_8_1 : forall P Q A B C, two_sides P Q A C -> two_sides P Q B C -> one_side P Q A B.

intros.
unfold one_side.
exists C.
split; assumption.
Qed.

Lemma not_two_sides_id : forall A P Q, ~ two_sides P Q A A.
intros.
intro.
unfold two_sides in H.
spliter.
ex_and H2 T.
apply between_identity in H3.
subst T.
apply H0.
apply H2.
Qed.

Lemma l9_8_2 : forall P Q A B C, two_sides P Q A C -> (one_side P Q A B -> two_sides P Q B C).
intros.

unfold one_side in H0.
ex_and H0 D.

assert (HH:= H).
assert (HH0:=H0).
assert (HH1:=H1).
unfold two_sides in HH.
unfold two_sides in HH0.
unfold two_sides in HH1.
spliter.
ex_and H13 T.
ex_and H9 X.
ex_and H5 Y.

assert (exists M , Bet Y M A /\ Bet X M B).
eapply inner_pasch.
apply H16.
apply H15.
ex_and H17 M.

assert (A <> D).
intro.
subst D.
apply not_two_sides_id in H0.
assumption.

assert (B <> D).
intro.
subst D.
apply not_two_sides_id in H1.
assumption.

induction (classic(Col A B D)).

induction (eq_dec_points M Y).
subst M.

assert (X = Y).
eapply inter_unicity.
apply col_permutation_1.
apply H9.
unfold Col.
right; left.
apply H15.
apply col_permutation_1.
assumption.
eapply (col2 _ B).
auto.
apply col_permutation_3.
assumption.
apply bet_col in H16.
Col.
intro.
Col.
auto.

subst Y.
eapply l9_5.
apply H.
apply H9.
unfold out.
repeat split.
intro.
subst X.
apply H11.
assumption.
intro.
subst X.
apply H3.
assumption.
unfold Col in H21.
induction H21.
right.
eapply between_exchange3.
apply between_symmetry.
apply H16.
apply between_symmetry.
assumption.
induction H21.

assert (Bet D B A \/ Bet D A B).
eapply (l5_1 _ X).
intro.
subst X.
apply H4.
assumption.
apply between_symmetry.
assumption.
apply between_symmetry.
assumption.
induction H22.

assert (D = B).
eapply between_egality.
apply H22.
apply H21.
subst D.
absurde.

assert (D = A).
eapply between_egality.
apply H22.
apply between_symmetry.
assumption.
subst D.
absurde.
eapply (l5_2 D).
intro.
subst X.
apply H8.
assumption.
apply between_symmetry.
assumption.
apply between_symmetry.
assumption.

induction (eq_dec_points M X).
subst M.

assert (X = Y).
eapply inter_unicity.
apply col_permutation_1.
apply H9.
unfold Col.
right; left.
apply H15.
apply col_permutation_1.
assumption.
eapply (col2 _ B).
auto.
Col.
apply bet_col in H16.
Col.
intro.
apply H4.
apply col_permutation_4.
assumption.
auto.

subst Y.
absurde.

eapply (l9_5 _ _ M _ X).

eapply l9_5.
apply H.
apply H5.

unfold out.
repeat split.
intro.
subst Y.
apply between_identity in H17.
subst M.
absurde.
assumption.
right.
assumption.
assumption.
unfold out.

assert (out Y M A).
unfold out.
repeat split.
assumption.
intro.
subst Y.
apply H11.
assumption.
left.
assumption.
repeat split.
assumption.
intro.
subst X.
apply between_identity in H18.
subst M.
absurde.
left.
apply H18.

eapply (l9_5 _ _ M).
eapply l9_5.
apply H.
apply H5.
unfold out.
repeat split.
intro.
subst Y.
apply H7.
assumption.
intro.
subst Y.

assert(Col B D X).
eapply (col2 _ M).
intro.
subst M.
apply H3.
assumption.
unfold Col.
left.
assumption.
unfold Col.
left.
apply between_symmetry.
assumption.
apply H21.
apply col_permutation_1.
eapply (col2 _ X).
intro.
subst X.
apply H4.
assumption.
unfold Col.
left.
apply between_symmetry.
assumption.
apply col_permutation_1.
assumption.
right.
assumption.
apply H9.
unfold out.
repeat split.
intro.
subst X.

assert (Col A D Y).
eapply (col2 _ M).
intro.
subst M.
apply H7.
assumption.
unfold Col.
left.
assumption.
unfold Col.
left.
apply between_symmetry.
assumption.
apply H21.
apply col_permutation_1.
eapply (col2 _ Y).
intro.
subst Y.
apply H4.
assumption.
apply col_permutation_1.
assumption.
unfold Col.
left.
apply between_symmetry.
assumption.
intro.
subst X.
apply H3.
assumption.
left.
assumption.
Qed.

Lemma l9_9 : forall P Q A B, two_sides P Q A B -> ~ one_side P Q A B.
intros.
intro.
assert(L:=l9_8_2).
apply (L P Q A B B )in H.
apply not_two_sides_id in H.
assumption.
assumption.
Qed.

Lemma l9_9_bis : forall P Q A B, one_side P Q A B -> ~ two_sides P Q A B.
intros.
intro.
unfold one_side in H.
ex_and H C.
assert (one_side P Q A B).
eapply l9_8_1.
apply H.
assumption.
assert (~ one_side P Q A B).
apply l9_9.
assumption.
contradiction.
Qed.

Lemma l9_10 : forall P Q A,
 P<>Q -> ~ Col A P Q -> exists C, two_sides P Q A C.
Proof.
intros.
double A P A'.
exists A'.
unfold two_sides.
repeat split.
assumption.
assumption.
intro.
apply H0.
eapply col_permutation_2.
eapply (col2 _ A').
intro.
subst A'.
apply l7_2 in H1.
eapply is_midpoint_id in H1.
subst A.
apply H0.
assumption.
apply col_permutation_4.
assumption.
unfold Col.
right; right.
apply mid_bet.
assumption.
exists P.
split.
apply col_trivial_1.
apply mid_bet.
assumption.
Qed.

Lemma one_side_reflexivity : forall P Q A,
 ~ Col A P Q -> one_side P Q A A.
Proof.
intros.
unfold one_side.
double A P C.
exists C.

assert (two_sides P Q A C).
repeat split.
intro.
subst Q.
apply H.
apply col_trivial_2.
assumption.

intro.
apply H.
apply col_permutation_2.
eapply (col2 _ C).
intro.
subst C.
apply l7_2 in H0.
apply is_midpoint_id in H0.
subst A.
apply H.
assumption.
apply col_permutation_4.
assumption.
unfold Col.
right; right.
apply mid_bet.
assumption.

exists P.
split.
apply col_trivial_1.
apply mid_bet.
assumption.
split; assumption.
Qed.

Lemma one_side_symmetry : forall P Q A B,
 one_side P Q A B -> one_side P Q B A.
Proof.
unfold one_side.
intros.
ex_and H C.
exists C.
split; assumption.
Qed.

Lemma one_side_transitivity : forall P Q A B C,
one_side P Q A B -> one_side P Q B C -> one_side P Q A C.
Proof.
intros.

unfold one_side in *.

ex_and H X.
ex_and H0 Y.
exists X.
split.
assumption.
apply l9_2.
eapply l9_8_2.
apply l9_2.
apply H2.
eapply l9_8_1.
apply l9_2.
apply H0.
apply l9_2.
assumption.
Qed.

End T9.