Library Ch09_plane

Require Export Ch08_orthogonality.

Ltac clean_reap_hyps :=
  repeat
  match goal with
   | H:(is_midpoint ?A ?B ?C), H2 : is_midpoint ?A ?C ?B |- _ ⇒ clear H2
   | H:(is_midpoint ?A ?B ?C), H2 : is_midpoint ?A ?B ?C |- _ ⇒ clear H2
   | H:(¬Col ?A ?B ?C), H2 : ¬Col ?A ?B ?C |- _ ⇒ clear H2
   | H:(Col ?A ?B ?C), H2 : Col ?A ?C ?B |- _ ⇒ clear H2
   | H:(Col ?A ?B ?C), H2 : Col ?A ?B ?C |- _ ⇒ clear H2
   | H:(Col ?A ?B ?C), H2 : Col ?B ?A ?C |- _ ⇒ clear H2
   | H:(Col ?A ?B ?C), H2 : Col ?B ?C ?A |- _ ⇒ clear H2
   | H:(Col ?A ?B ?C), H2 : Col ?C ?B ?A |- _ ⇒ clear H2
   | H:(Col ?A ?B ?C), H2 : Col ?C ?A ?B |- _ ⇒ clear H2
   | H:(Bet ?A ?B ?C), H2 : Bet ?C ?B ?A |- _ ⇒ clear H2
   | H:(Bet ?A ?B ?C), H2 : Bet ?A ?B ?C |- _ ⇒ clear H2
   | H:(Cong ?A ?B ?C ?D), H2 : Cong ?A ?B ?D ?C |- _ ⇒ clear H2
   | H:(Cong ?A ?B ?C ?D), H2 : Cong ?A ?B ?C ?D |- _ ⇒ clear H2
   | H:(Cong ?A ?B ?C ?D), H2 : Cong ?C ?D ?A ?B |- _ ⇒ clear H2
   | H:(Cong ?A ?B ?C ?D), H2 : Cong ?C ?D ?B ?A |- _ ⇒ clear H2
   | H:(Cong ?A ?B ?C ?D), H2 : Cong ?D ?C ?B ?A |- _ ⇒ clear H2
   | H:(Cong ?A ?B ?C ?D), H2 : Cong ?D ?C ?A ?B |- _ ⇒ clear H2
   | H:(Cong ?A ?B ?C ?D), H2 : Cong ?B ?A ?C ?D |- _ ⇒ clear H2
   | H:(Cong ?A ?B ?C ?D), H2 : Cong ?B ?A ?D ?C |- _ ⇒ clear H2
   | H:(Perp ?A ?B ?C ?D), H2 : Perp ?A ?B ?D ?C |- _ ⇒ clear H2
   | H:(Perp ?A ?B ?C ?D), H2 : Perp ?A ?B ?C ?D |- _ ⇒ clear H2
   | H:(Perp ?A ?B ?C ?D), H2 : Perp ?C ?D ?A ?B |- _ ⇒ clear H2
   | H:(Perp ?A ?B ?C ?D), H2 : Perp ?C ?D ?B ?A |- _ ⇒ clear H2
   | H:(Perp ?A ?B ?C ?D), H2 : Perp ?D ?C ?B ?A |- _ ⇒ clear H2
   | H:(Perp ?A ?B ?C ?D), H2 : Perp ?D ?C ?A ?B |- _ ⇒ clear H2
   | H:(Perp ?A ?B ?C ?D), H2 : Perp ?B ?A ?C ?D |- _ ⇒ clear H2
   | H:(Perp ?A ?B ?C ?D), H2 : Perp ?B ?A ?D ?C |- _ ⇒ clear H2
   | H:(?A<>?B), H2 : (?B<>?A) |- _ ⇒ clear H2
   | H:(?A<>?B), H2 : (?A<>?B) |- _ ⇒ clear H2
   | H:(Per ?A ?D ?C), H2 : (Per ?C ?D ?A) |- _ ⇒ clear H2
   | H:(Per ?A ?D ?C), H2 : (Per ?A ?D ?C) |- _ ⇒ clear H2
   | H:(Perp_in ?X ?A ?B ?C ?D), H2 : Perp_in ?X ?A ?B ?D ?C |- _ ⇒ clear H2
   | H:(Perp_in ?X ?A ?B ?C ?D), H2 : Perp_in ?X ?A ?B ?C ?D |- _ ⇒ clear H2
   | H:(Perp_in ?X ?A ?B ?C ?D), H2 : Perp_in ?X ?C ?D ?A ?B |- _ ⇒ clear H2
   | H:(Perp_in ?X ?A ?B ?C ?D), H2 : Perp_in ?X ?C ?D ?B ?A |- _ ⇒ clear H2
   | H:(Perp_in ?X ?A ?B ?C ?D), H2 : Perp_in ?X ?D ?C ?B ?A |- _ ⇒ clear H2
   | H:(Perp_in ?X ?A ?B ?C ?D), H2 : Perp_in ?X ?D ?C ?A ?B |- _ ⇒ clear H2
   | H:(Perp_in ?X ?A ?B ?C ?D), H2 : Perp_in ?X ?B ?A ?C ?D |- _ ⇒ clear H2
   | H:(Perp_in ?X ?A ?B ?C ?D), H2 : Perp_in ?X ?B ?A ?D ?C |- _ ⇒ clear H2
end.

Ltac assert_diffs :=
repeat
 match goal with
      | H:(¬Col ?X1 ?X2 ?X3) |- _ ⇒
      let h := fresh in
      not_exist_hyp3 X1 X2 X1 X3 X2 X3;
      assert (h := not_col_distincts X1 X2 X3 H);decompose [and] h;clear h;clean_reap_hyps

      | H:Cong ?A ?B ?C ?D, H2 : ?A ≠ ?B |-_ ⇒
      let T:= fresh in (not_exist_hyp_comm C D);
        assert (T:= cong_diff A B C D H2 H);clean_reap_hyps
      | H:Cong ?A ?B ?C ?D, H2 : ?B ≠ ?A |-_ ⇒
      let T:= fresh in (not_exist_hyp_comm C D);
        assert (T:= cong_diff_2 A B C D H2 H);clean_reap_hyps
      | H:Cong ?A ?B ?C ?D, H2 : ?C ≠ ?D |-_ ⇒
      let T:= fresh in (not_exist_hyp_comm A B);
        assert (T:= cong_diff_3 A B C D H2 H);clean_reap_hyps
      | H:Cong ?A ?B ?C ?D, H2 : ?D ≠ ?C |-_ ⇒
      let T:= fresh in (not_exist_hyp_comm A B);
        assert (T:= cong_diff_4 A B C D H2 H);clean_reap_hyps

      | H:is_midpoint ?I ?A ?B, H2 : ?A<>?B |- _ ⇒
      let T:= fresh in (not_exist_hyp2 I B I A);
       assert (T:= midpoint_distinct_1 I A B H2 H);
       decompose [and] T;clear T;clean_reap_hyps
      | H:is_midpoint ?I ?A ?B, H2 : ?B<>?A |- _ ⇒
      let T:= fresh in (not_exist_hyp2 I B I A);
       assert (T:= midpoint_distinct_1 I A B (swap_diff B A H2) H);
       decompose [and] T;clear T;clean_reap_hyps

      | H:is_midpoint ?I ?A ?B, H2 : ?I<>?A |- _ ⇒
      let T:= fresh in (not_exist_hyp2 I B A B);
       assert (T:= midpoint_distinct_2 I A B H2 H);
       decompose [and] T;clear T;clean_reap_hyps
      | H:is_midpoint ?I ?A ?B, H2 : ?A<>?I |- _ ⇒
      let T:= fresh in (not_exist_hyp2 I B A B);
       assert (T:= midpoint_distinct_2 I A B (swap_diff A I H2) H);
       decompose [and] T;clear T;clean_reap_hyps

      | H:is_midpoint ?I ?A ?B, H2 : ?I<>?B |- _ ⇒
      let T:= fresh in (not_exist_hyp2 I A A B);
       assert (T:= midpoint_distinct_3 I A B H2 H);
       decompose [and] T;clear T;clean_reap_hyps
      | H:is_midpoint ?I ?A ?B, H2 : ?B<>?I |- _ ⇒
      let T:= fresh in (not_exist_hyp2 I A A B);
       assert (T:= midpoint_distinct_3 I A B (swap_diff B I H2) H);
       decompose [and] T;clear T;clean_reap_hyps

      | H:Perp ?A ?B ?C ?D |- _ ⇒
      let T:= fresh in (not_exist_hyp2 A B C D);
       assert (T:= perp_distinct A B C D H);
       decompose [and] T;clear T;clean_reap_hyps
      | H:Perp_in ?X ?A ?B ?C ?D |- _ ⇒
      let T:= fresh in (not_exist_hyp2 A B C D);
       assert (T:= perp_in_distinct X A B C D H);
       decompose [and] T;clear T;clean_reap_hyps
      | H:out ?A ?B ?C |- _ ⇒
      let T:= fresh in (not_exist_hyp2 A B A C);
       assert (T:= out_distinct A B C H);
       decompose [and] T;clear T;clean_reap_hyps
 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
   | H:(Per ?X1 ?X2 ?X2) |- _ ⇒ clear H
   | H:(Per ?X1 ?X1 ?X2) |- _ ⇒ clear H
   | H:(is_midpoint ?X1 ?X1 ?X1) |- _ ⇒ clear H
end.

Ltac finish := match goal with
 | |- Col ?A ?B ?C ⇒ Col
 | |- ¬ Col ?A ?B ?C ⇒ Col
 | |- Perp ?A ?B ?C ?D ⇒ Perp
 | |- Cong ?A ?B ?C ?D ⇒ Cong
 | |- is_midpoint ?A ?B ?C ⇒ Midpoint
 | |- ?A<>?B ⇒ apply swap_diff;assumption
 | |- _ ⇒ try assumption
end.

Section T9.

Context `{MT:Tarski_neutral_dimensionless}.
Context `{EqDec:EqDecidability Tpoint}.

Definition two_sides := fun A B P Q ⇒
  A≠B ∧ ¬ Col P A B ∧ ¬ Col Q A B ∧ ∃ T, Col T A B ∧ Bet P T Q.

Lemma l9_2 : ∀ A B P Q, two_sides A B P Q → two_sides A B Q P.
Proof.
unfold two_sides.
intros.
spliter.
repeat split; try Col.
destruct H2 as [T [HCol1 HCol2]].
∃ T; Col; Between.
Qed.

Lemma invert_two_sides : ∀ A B P Q,
 two_sides A B P Q → two_sides B A P Q.
Proof with finish.
unfold two_sides.
intros.
spliter.
repeat split...
ex_and H2 T.
∃ T;split...
Qed.

Lemma inter_unicity : ∀ 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.
Proof.
intros.
apply l6_21 with A B X Y; Col.
Qed.

Lemma colx : ∀ 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.
Proof.
intros.
ColR.
Qed.

Lemma l9_3 : ∀ 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 with finish.

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

show_distinct A C.
intuition.

assert (T = M).
assert_bet.
assert_cols.
eapply inter_unicity with P Q A C...

subst T.

repeat split...

induction(eq_dec_points C M).
subst M.
intuition.

intro.
clear H0.

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

assert (Col P R B)
 by ColR.

assert (Col P R A).
induction (eq_dec_points P B).
subst B.
assert_cols...

apply col_permutation_2.
eapply col_transitivity_2.
apply H0.

assert_cols...

Col.

induction (eq_dec_points P R).
subst R.
apply H4.
apply col_permutation_2.
eapply (col_transitivity_1 _ B).

assert_diffs;intuition.

apply col_permutation_4.
assumption.

assert_cols...

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.
Between.
apply H4.
apply col_permutation_2.
eapply col_transitivity_1.
apply H15.
Col.
assumption.

induction H3.
spliter.
induction H10.

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

assert (∃ X, Bet M X R' ∧ Bet C X B).
eapply inner_pasch.
apply midpoint_bet.
apply H11.
apply between_symmetry.
assumption.
ex_and H14 X.
∃ X.

split.

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

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

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

show_distinct M R'.
 intuition.

assert (M ≠ R).
intro.
subst R.

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

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

eapply (col_transitivity_1).
apply H20.
apply col_trivial_2.
eapply col_transitivity_1.
apply H19.
unfold Col.
right; right.
apply midpoint_bet.
assumption.
unfold Col.
right; left.
Between.

Between.

assert (∃ X, Bet B X C ∧ Bet M X R).
eapply inner_pasch.
apply H10.
Between.

ex_and H11 X.
∃ 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.
Col.
Col.

assert (Col X P Q).
apply col_permutation_2.
eapply colx.
assumption.
apply H13.
auto.
Col.
Col.
assert_cols...
assumption.
assumption.
Qed.

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

Lemma sym_sym : ∀ A C A', is_symmetric A A' C → is_symmetric A' A C.
Proof.
unfold is_symmetric.
intros.
apply l7_2.
assumption.
Qed.

Lemma distinct : ∀ 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 : ∀ A B, ∃ C, A ≠ C ∧ B ≠ C ∧ Col A B C.
Proof.
intros.
assert (∃ C, Bet A B C ∧ B ≠ C).
apply point_construction_different.
ex_and H C.
∃ C.
split.
intro.
induction (eq_dec_points A B).
subst B.
subst C.
intuition.
subst C.
Between.
assert_cols.
auto.
Qed.

Lemma diff_bet_ex3 : ∀ A B C,
 Bet A B C →
 ∃ 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 (∃ D, Bet B C D ∧ C ≠ D).
apply point_construction_different.
ex_and H2 D.
∃ D.
repeat split.
subst C.
subst A.
assumption.
subst A.
subst C.
assumption.
assumption.
unfold Col.
left.
subst A.
subst C.
assumption.

assert (∃ D, Bet B C D ∧ C ≠ D).
apply point_construction_different.
ex_and H2 D.
∃ 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(∃ D : Tpoint, A ≠ D ∧ B ≠ D ∧ Col A B D).
intro.
ex_and H1 D.
∃ D.
repeat split.
assumption.
assumption.
assumption.
assumption.
apply diff_col_ex.

assert (∃ D, Bet B C D ∧ C ≠ D).
apply point_construction_different.
ex_and H2 D.
∃ 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 : ∀ A B C,
 Col A B C → ∃ 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 (∃ C, A ≠ C ∧ B ≠ C ∧ Col A B C).
apply (diff_col_ex).
ex_and H0 D.
∃ D.
repeat split; assumption.
apply cas2 in HH.
ex_and HH D.
∃ 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 (∃ C, A ≠ C ∧ B ≠ C ∧ Col A B C).
apply (diff_col_ex).
ex_and H0 D.
∃ D.
repeat split; assumption.
assert (HH:=H).
apply cas3 in HH.
ex_and HH D.
∃ 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_preserves_col : ∀ 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 with A B C M;auto.
assert_cols;Col.
induction H.
assert (Bet B' C' A').
eapply l7_15 with B C A M;auto.
assert_cols;Col.
assert (Bet C' A' B').
eapply l7_15 with C A B M;auto.
assert_cols;Col.
Qed.

Lemma per_mid_per : ∀ 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 midpoint_bet.
assumption.
apply midpoint_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.
∃ 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 : ∀ 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.
∃ A.
assumption.
right.
unfold Perp.
∃ 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.
Col.
Col.
assumption.
Qed.

Lemma sym_preserve_diff : ∀ 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 : ∀ 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 col3.
apply perp_distinct in H.
spliter.
apply H.
assumption.
apply col_trivial_3.
assumption.
Qed.

Lemma l9_4_1_aux : ∀ 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 →
 (∀ 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.

induction (eq_dec_points M T).
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 (symmetric_point_unicity _ _ 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 midpoint_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.

assert (Perp M T A M)
 by (eapply perp_col2 with P Q;Col).
 apply perp_perp_in in H11.
 apply perp_in_comm in H11.
 eapply perp_in_per in H11.

assert (Perp M T C M)
 by (eapply perp_col2 with P Q;Col).
 apply perp_perp_in in H12.
 apply perp_in_comm in H12.
 eapply perp_in_per in H12.

assert (M = T).
 apply (l8_6 C M T A).
 3:Between.
 apply l8_2;auto.
 apply l8_2;auto.

subst T.
split.
intro.
unfold out in ×.
spliter.
repeat split.
intro.
subst C.
apply perp_distinct in H4.
spliter.
absurde.
intro.
subst C'.
intuition.
intuition.
intuition.


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(∃ 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 col3.
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.

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.

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

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 : ∀ 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_bet.
assert_cols.
assert (Col A C C') by ColR.
assert (C = C' ∨ is_midpoint A C C')
 by (eapply l7_20;Col).
induction H7.
treat_equalities.
intuition.
eapply l7_17;eauto.
Qed.

Lemma l9_4_1 : ∀ 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 →
 (∀ U C',is_midpoint M U C' → (out R U A ↔ out S C C')).
Proof.
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 : ∀ 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.
Proof.
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.
∃ M.
unfold is_midpoint in ×.
spliter.
split.
unfold Col.
right; right.
apply between_symmetry.
assumption.
assumption.
Qed.

Lemma col_preserves_two_sides : ∀ 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.
Proof.
intros.
unfold two_sides in ×.
spliter.
repeat split.
assumption.
intro.
apply H4.
apply col_permutation_1.

eapply col3.
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 col3.
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.
∃ T.
split.

eapply col3.
apply H3.
apply col_permutation_1.
assumption.
assumption.
assumption.
assumption.
Qed.

Lemma out_out_two_sides : ∀ 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.
Proof.
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.
∃ 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 l9_4_2_aux : ∀ 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.
Proof.
intros.

induction (eq_dec_points R S).
subst S.

assert (TT:= H0).
unfold two_sides in H0.
spliter.
ex_and H9 T.

induction (eq_dec_points R T).
subst T.
clear H9 H3.

apply (out_out_two_sides P Q A C U V R); auto using l6_6, bet_col with col.

assert (Perp R T A R)
 by (eapply perp_col2 with P Q;Col).
 apply perp_perp_in in H12.
 apply perp_in_comm in H12.
 eapply perp_in_per in H12.

assert (Perp R T C R)
 by (eapply perp_col2 with P Q;Col).
 apply perp_perp_in in H13.
 apply perp_in_comm in H13.
 eapply perp_in_per in H13.

assert (R = T).
 apply (l8_6 C R T A).
 3:Between.
 apply l8_2;auto.
 apply l8_2;auto.
subst.
intuition.


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 col_transitivity_1.
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 (∃ 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 midpoint_bet.
apply H18.
apply l7_2.
assumption.
apply col_trivial_3.

assert (∀ 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 : ∀ 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.
Proof.
intros.
assert(le S C R A ∨ le R A S C)
 by (apply le_cases).
induction H6.
eapply l9_4_2_aux with A C R S;assumption.
apply l9_2.
apply l9_2 in H.
eapply l9_4_2_aux with C A S R;auto.
Qed.

Lemma l9_5 : ∀ 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.
Proof.
intros.

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

assert(∃ 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(∃ 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(∃ 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 col_transitivity_1.
apply H.
assumption.
apply col_permutation_1.
assumption.

assert (R ≠ B).
intro.
subst B.
absurde.

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

apply H8.
eapply col_permutation_2.
eapply col_transitivity_1.

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 (∃ 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 symmetric_point_unicity in H10.
apply H15.
apply sym_equal.
apply H10.

apply l7_3_2.
assumption.
assumption.
unfold Col.
right;left.
apply midpoint_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.