Library Ch10_line_reflexivity

Require Export Ch09_plane.

Section T10.

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

Definition is_image_spec P' P A B :=
  (∃ X, is_midpoint X P P' ∧ Col A B X) ∧
  (Perp A B P P' ∨ P=P').

Definition is_image P' P A B :=
 (A≠B ∧ is_image_spec P' P A B) ∨ (A=B ∧ is_midpoint A P P').

Lemma ex_sym : ∀ A B X, ∃ Y, (Perp A B X Y ∨ X = Y) ∧
   (∃ M, Col A B M ∧ is_midpoint M X Y).
Proof.
intros.
induction (Col_dec A B X).
∃ X.
split.
right.
reflexivity.
∃ X.
split.
assumption.
apply l7_3_2.
assert (∃ M, Col A B M ∧ Perp A B X M).
apply l8_18_existence.
assumption.
ex_and H0 M.
double X M Z.
∃ Z.
split.
left.
apply perp_sym.
eapply perp_col.
intro.
subst Z.
apply l7_3 in H2.
subst X.
apply perp_distinct in H1.
spliter.
absurde.
apply perp_sym.
apply H1.
unfold Col.
left.
apply midpoint_bet.
assumption.
∃ M.
split.
assumption.
assumption.
Qed.

Lemma is_image_is_image_spec : ∀ P P' A B, A≠B → (is_image P' P A B ↔ is_image_spec P' P A B).
Proof.
intros.
unfold is_image.
tauto.
Qed.

Require Import Setoid.

Lemma ex_sym1 : ∀ A B X, A≠B → ∃ Y, (Perp A B X Y ∨ X = Y) ∧
 (∃ M, Col A B M ∧ is_midpoint M X Y ∧ is_image X Y A B).
Proof.
intros.
induction (Col_dec A B X).
∃ X.
split.
right.
reflexivity.
∃ X.
rewrite → (is_image_is_image_spec) by apply H.
split.
assumption.
split.
apply l7_3_2.
unfold is_image_spec.
split.
∃ X.
split.
apply l7_3_2.
assumption.
right.
reflexivity.
assert (∃ M, Col A B M ∧ Perp A B X M).
apply l8_18_existence.
assumption.
ex_and H1 M.
double X M Z.
∃ Z.
split.
left.
apply perp_sym.
eapply perp_col.
intro.
subst Z.
apply l7_3 in H3.
subst X.
apply perp_distinct in H2.
spliter.
absurde.
apply perp_sym.
apply H2.
unfold Col.
left.
apply midpoint_bet.
assumption.
∃ M.
split.
assumption.
split.
assumption.
rewrite → (is_image_is_image_spec) by apply H.
unfold is_image_spec.
split.
∃ M.
split.
apply l7_2.
assumption.
assumption.
left.
apply perp_sym.
apply perp_left_comm.
eapply perp_col.
intro.
subst X.
apply l7_3 in H3.
subst Z.
apply perp_distinct in H2.
spliter.
absurde.
apply perp_sym.
apply H2.
unfold Col.
left.
apply midpoint_bet.
assumption.
Qed.

Lemma l10_2_unicity : ∀ A B P P1 P2,
 is_image P1 P A B → is_image P2 P A B → P1=P2.
Proof.
intros.

induction (eq_dec_points A B).
subst.
unfold is_image in ×.
induction H.
intuition.
induction H0.
intuition.
spliter.
eapply symmetric_point_unicity with P B;auto.

rewrite → (is_image_is_image_spec) in × by apply H1.
unfold is_image_spec in ×.
spliter.
ex_and H X.
ex_and H0 Y.
induction H2; induction H3.

assert (P ≠ X).
intro.
subst X.
apply is_midpoint_id in H.
subst P1.
apply perp_distinct in H3.
spliter.
absurde.

assert (P ≠ Y).
intro.
subst Y.
apply is_midpoint_id in H0.
subst P2.
apply perp_distinct in H2.
spliter.
absurde.

assert (Perp P X A B).
eapply perp_col.
assumption.
apply perp_sym.
apply H3.
unfold Col.
right; left.
apply midpoint_bet.
apply l7_2.
assumption.

assert (Perp P Y A B).
eapply perp_col.
assumption.
apply perp_sym.
apply H2.
unfold Col.
right; left.
apply midpoint_bet.
apply l7_2.
assumption.

induction (eq_dec_points X A).
subst X.

assert (¬ Col A B P ∧ Per P A B).
eapply l8_16_1.
assumption.
apply col_trivial_3.
apply col_trivial_2.
auto.
apply perp_sym.
assumption.
spliter.

assert (Y = A).
eapply l8_18_unicity.
apply H10.
assumption.
apply perp_sym.
assumption.
apply col_trivial_3.
apply perp_sym.
assumption.
subst Y.
eapply symmetric_point_unicity.
apply H.
apply H0.

assert (¬ Col A B P ∧ Per P X A).
eapply l8_16_1.
assumption.
assumption.
apply col_trivial_3.
auto.
apply perp_sym.
assumption.
spliter.

assert (Y = X).
eapply l8_18_unicity.
apply H11.
assumption.
apply perp_sym.
assumption.
assumption.
apply perp_sym.
assumption.
subst Y.

eapply symmetric_point_unicity.
apply H.
apply H0.

subst P1.
assert (P ≠ Y).
intro.
subst Y.
apply l7_3 in H.
subst X.
apply is_midpoint_id in H0.
subst P2.
eapply perp_distinct in H2.
spliter.
absurde.

assert (Perp P Y A B).
eapply perp_col.
assumption.
apply perp_sym.
apply H2.
unfold Col.
right; left.
apply midpoint_bet.
apply l7_2.
assumption.

apply l7_3 in H.
subst X.

induction (eq_dec_points Y A).
subst Y.

assert (¬ Col A B P ∧ Per P A B).
eapply l8_16_1.
assumption.
assumption.
apply col_trivial_2.
auto;
auto.
apply perp_sym.
assumption.
spliter.
contradiction.

assert (¬ Col A B P ∧ Per P Y A).
eapply l8_16_1.
assumption.
assumption.
apply col_trivial_3.
auto.
apply perp_sym.
assumption.
spliter.
contradiction.

subst P2.
assert (P ≠ X).
intro.
subst X.
apply l7_3 in H0.
subst Y.
apply is_midpoint_id in H.
subst P1.
eapply perp_distinct in H3.
spliter.
absurde.

assert (Perp P X A B).
eapply perp_col.
assumption.
apply perp_sym.
apply H3.
unfold Col.
right; left.
apply midpoint_bet.
apply l7_2.
assumption.

apply l7_3 in H0.
subst Y.

induction (eq_dec_points X A).
subst X.

assert (¬ Col A B P ∧ Per P A B).
eapply l8_16_1.
assumption.
assumption.
apply col_trivial_2.
auto.
apply perp_sym.
assumption.
spliter.
contradiction.

assert (¬ Col A B P ∧ Per P X A).
eapply l8_16_1.
assumption.
assumption.
apply col_trivial_3.
auto.
apply perp_sym.
assumption.
spliter.
contradiction.

subst P1.
subst P2.
reflexivity.
Qed.

Lemma l10_2_existence_spec : ∀ A B P,
 ∃ P', is_image_spec P' P A B.
Proof.
intros.
induction (Col_dec A B P).
unfold is_image_spec.
∃ P.
split.
∃ P.
split.
apply l7_3_2.
assumption.
right.
reflexivity.

assert (∃ X, Col A B X ∧ Perp A B P X).
eapply l8_18_existence.
assumption.
ex_and H0 X.
double P X P'.
∃ P'.
unfold is_image_spec.
split.
∃ X.
split; assumption.
left.
apply perp_sym.
eapply perp_col.
intro.
subst P'.
apply l7_3 in H2.
subst X.
apply perp_distinct in H1.
spliter.
absurde.
apply perp_sym.
apply H1.
unfold Col.
left.
apply midpoint_bet.
assumption.
Qed.

Lemma l10_2_existence : ∀ A B P,
 ∃ P', is_image P' P A B.
Proof.
intros.

induction (eq_dec_points A B).
subst B.
unfold is_image.
elim (symmetric_point_construction P A).
intros P'.
∃ P'.
tauto.

elim (l10_2_existence_spec A B P).
intros P'; intros.
∃ P'.
unfold is_image.
tauto.
Qed.

Lemma l10_4_spec : ∀ A B P P',
 is_image_spec P P' A B →
 is_image_spec P' P A B.
Proof.
intros.
unfold is_image_spec in ×.
spliter.
ex_and H X.
split.
∃ X.
split.
apply l7_2.
assumption.
assumption.
induction H0.
left.
apply perp_right_comm.
assumption.
auto.
Qed.

Lemma l10_4 : ∀ A B P P', is_image P P' A B → is_image P' P A B.
Proof.
intros.
induction (eq_dec_points A B).
subst B.
unfold is_image in ×.
elim H;intros.
intuition.
right.
spliter.
split.
assumption.
apply l7_2.
assumption.

rewrite → (is_image_is_image_spec) in × by apply H0.
apply l10_4_spec;auto.
Qed.

Lemma l10_5 : ∀ A B P P' P'',
 is_image P' P A B →
 is_image P'' P' A B → P=P''.
Proof.
intros.

induction (eq_dec_points A B).
unfold is_image in ×.
subst.
induction H.
intuition.
induction H0.
intuition.
spliter.
apply symmetric_point_unicity with P' B.
apply l7_2.
assumption.
assumption.

rewrite → (is_image_is_image_spec) in × by apply H1.
eapply l10_2_unicity.
eapply l10_4.
apply is_image_is_image_spec.
apply H1.
apply H.
apply is_image_is_image_spec.
assumption.
assumption.
Qed.

Lemma l10_6_unicity : ∀ A B P P1 P2, is_image P P1 A B → is_image P P2 A B → P1 = P2.
Proof.
intros.
induction (eq_dec_points A B).
subst.
unfold is_image in ×.
induction H.
intuition.
induction H0.
intuition.
spliter.
apply symmetric_point_unicity with P B.
apply l7_2.
assumption.
apply l7_2.
assumption.

eapply l10_2_unicity.
apply l10_4.
apply H.
apply l10_4.
assumption.
Qed.

Lemma l10_6_existence_spec : ∀ A B P', A≠B → ∃ P, is_image_spec P' P A B.
Proof.
intros.
assert (∃ P, is_image_spec P P' A B).
eapply l10_2_existence_spec.
ex_and H0 P.
∃ P.
apply l10_4_spec.
assumption.
Qed.

Lemma l10_6_existence : ∀ A B P', ∃ P, is_image P' P A B.
Proof.
intros.
assert (∃ P, is_image P P' A B).
eapply l10_2_existence.
ex_and H P.
∃ P.
apply l10_4.
assumption.
Qed.

Lemma l10_7 : ∀ A B P P' Q Q',
 is_image P' P A B → is_image Q' Q A B →
  P'=Q' → P = Q.
Proof.
intros.
subst Q'.
eapply l10_2_unicity.
apply l10_4.
apply H.
apply l10_4.
assumption.
Qed.

Lemma l10_8 : ∀ A B P, is_image P P A B → Col P A B.
Proof.
intros.
induction (eq_dec_points A B).
subst;Col.
unfold is_image in H.
unfold is_image_spec in H.
induction H.
spliter.
ex_and H1 X.
apply l7_3 in H1.
subst X.
Col.
spliter. subst. Col.
Qed.

Lemma is_image_col_cong : ∀ A B P P' X, A≠B →
 is_image P P' A B → Col A B X → Cong P X P' X.
Proof.
intros.
rewrite is_image_is_image_spec in H0 by apply H.

unfold is_image_spec in ×.
spliter.
ex_and H0 M.
induction H2.

assert (HH:= H2).
apply perp_distinct in HH.
spliter.

induction (eq_dec_points M X).
subst X.
unfold is_midpoint in ×.
spliter.
Cong.

assert (Perp M X P' P).
eapply perp_col2;eauto.

assert(¬ Col A B P ∧ Per P M X).
eapply l8_16_1.
assumption.
assumption.
assumption.
auto.
apply perp_sym.
eapply perp_col.
intro.
subst P.
apply l7_2 in H0.
apply is_midpoint_id in H0.
subst P'.
absurde.
apply perp_left_comm.
apply perp_sym.
apply H2;
eapply perp_left_comm.
unfold Col.
right; left.
apply midpoint_bet.
assumption.
spliter.
eapply l8_2 in H9.
unfold Per in H9.
ex_and H9 P0.
assert (P0 = P').
eapply symmetric_point_unicity.
apply H9.
apply l7_2.
assumption.
subst P0.
apply cong_commutativity.
assumption.
subst P'.
apply cong_reflexivity.
Qed.

Lemma is_image_spec_col_cong : ∀ A B P P' X,
 is_image_spec P P' A B → Col A B X → Cong P X P' X.
Proof.
intros.
unfold is_image_spec in ×.
spliter.
ex_and H M.
induction H1.

assert (HH:= H1).
apply perp_distinct in HH.
spliter.

induction (eq_dec_points M X).
subst X.
unfold is_midpoint in ×.
spliter.
Cong.

assert (Perp M X P' P)
 by (eauto using perp_col2).

assert(¬ Col A B P ∧ Per P M X).
eapply l8_16_1.
assumption.
assumption.
assumption.
auto.
apply perp_sym.
eapply perp_col.
intro.
subst P.
apply l7_2 in H.
apply is_midpoint_id in H.
subst P'.
absurde.
apply perp_left_comm.
apply perp_sym.
apply H1;
eapply perp_left_comm.
unfold Col.
right; left.
apply midpoint_bet.
assumption.
spliter.
eapply l8_2 in H8.
unfold Per in H8.
ex_and H8 P0.
assert (P0 = P').
eapply symmetric_point_unicity.
apply H8.
apply l7_2.
assumption.
subst P0.
Cong.
subst.
Cong.
Qed.

Lemma perp_not_col : ∀ A B P, Perp A B P A → ¬ Col A B P.
Proof.
intros.
assert (Perp_in A A B P A).
apply perp_perp_in.
assumption.

assert (Per P A B).
apply perp_in_per.
apply perp_in_sym.
assumption.
apply perp_in_left_comm in H0.

assert (¬ Col B A P → ¬ Col A B P).
intro.
intro.
apply H2.
apply col_permutation_4.
assumption.
apply H2.
apply perp_distinct in H.
spliter.
apply per_not_col.

auto.
auto.
apply perp_in_per.
apply perp_in_right_comm.
assumption.
Qed.

Lemma image_id : ∀ A B T T',
  A≠B →
  Col A B T →
  is_image T T' A B →
  T = T'.
Proof.
intros.
rewrite is_image_is_image_spec in H1 by apply H.
unfold is_image_spec in H1.
spliter.
ex_and H1 X.
induction H2.
assert (A ≠ B ∧ T' ≠ T).
apply perp_distinct in H2.
spliter.
split;
assumption.
spliter.

induction (eq_dec_points A X).
subst X.
assert (Perp A B T' A).
apply perp_sym.
eapply perp_col.
intro.
subst T'.
apply is_midpoint_id in H1.
subst A.
absurde.
apply perp_sym.
apply H2.
unfold Col.
right; left.
apply midpoint_bet.
apply l7_2.
assumption.
assert (¬ Col A T' B).
apply perp_not_col.
apply perp_comm.
apply perp_sym.
assumption.
assert (A = T).
eapply inter_unicity.
5: apply H7.
apply col_trivial_3.
unfold Col.
right; left.
apply midpoint_bet.
apply l7_2.
apply H1.
assumption.
apply col_trivial_2.
assumption.
subst A.
apply l7_2 in H1.
apply is_midpoint_id in H1.
subst T'.
absurde.

induction (eq_dec_points B X).
subst X.
assert (Perp A B T' B).
apply perp_sym.
eapply perp_col.
intro.
subst T'.

apply is_midpoint_id in H1.
subst B.
absurde.
apply perp_sym.
apply H2.
unfold Col.
right; left.
apply midpoint_bet.
apply l7_2.
assumption.
assert (¬ Col B T' A).
apply perp_not_col.
apply perp_left_comm.
apply perp_sym.
assumption.
assert (B = T).
eapply inter_unicity.
5: apply H8.
apply col_trivial_3.
unfold Col.
right; left.
apply midpoint_bet.
apply l7_2.
apply H1.
apply col_permutation_4.
assumption.
apply col_trivial_2.
assumption.
subst B.
apply l7_2 in H1.
apply is_midpoint_id in H1.
subst T'.
absurde.

assert (Col A X T) by ColR.

assert (Perp A B T' X).
apply perp_sym.
eapply perp_col.
intro.
subst T'.
apply is_midpoint_id in H1.
subst X.
absurde.
apply perp_sym.
apply H2.
assert_cols.
Col.

assert (¬ Col X T' A).
apply perp_not_col.
apply perp_left_comm.
apply perp_sym.
eapply perp_col.
assumption.
apply H9.
assumption.

assert (X = T).
eapply inter_unicity.
5: apply H10.
apply col_trivial_3.
unfold Col.
right; left.
apply midpoint_bet.
apply l7_2.
apply H1.
apply col_permutation_4.
assumption.
apply col_trivial_2.
assumption.
subst X.
apply l7_2 in H1.
apply is_midpoint_id in H1.
subst T'.
absurde.

subst T'.
reflexivity.
Qed.

Lemma osym_not_col : ∀ A B P P',
 is_image P P' A B →
 ¬ Col A B P → ¬ Col A B P'.
Proof.
intros.

unfold is_image in ×.
induction H.
spliter.

assert ( HH:= H1).
unfold is_image_spec in HH.
spliter.
ex_and H2 T.
intro.
induction H3.
assert (P'=P).
eapply image_id.
apply H.
assumption.

apply l10_4.
apply is_image_is_image_spec.
assumption.
assumption.
subst P'.
apply perp_distinct in H3.
spliter.
absurde.
apply H0.
subst P'.
assumption.
spliter. subst. Col5.
Qed.

Definition coplanar A B C D :=
  ∃ X, (Col A B X ∧ Col C D X) ∨ (Col A C X ∧ Col B D X) ∨ (Col A D X ∧ Col B C X).

Lemma coplanar_perm_1 : ∀ A B C D,
 coplanar A B C D → coplanar A B D C.
Proof.
intros.
unfold coplanar in ×.
decompose [ex and or] H;clear H;
∃ x;Col5.
Qed.

Lemma coplanar_perm_2 : ∀ A B C D,
 coplanar A B C D → coplanar A C B D.
Proof.
intros.
unfold coplanar in ×.
decompose [ex and or] H;clear H;
∃ x;Col5.
Qed.

Lemma coplanar_perm_3 : ∀ A B C D,
 coplanar A B C D → coplanar A C D B.
Proof.
intros.
unfold coplanar in ×.
decompose [ex and or] H;clear H;
∃ x;Col5.
Qed.

Lemma coplanar_perm_4 : ∀ A B C D,
 coplanar A B C D → coplanar A D B C.
Proof.
intros.
unfold coplanar in ×.
decompose [ex and or] H;clear H;
∃ x;Col5.
Qed.

Lemma coplanar_perm_5 : ∀ A B C D,
 coplanar A B C D → coplanar A D C B.
Proof.
intros.
unfold coplanar in ×.
decompose [ex and or] H;clear H;
∃ x;Col5.
Qed.

Lemma coplanar_perm_6 : ∀ A B C D,
 coplanar A B C D → coplanar B A C D.
Proof.
intros.
unfold coplanar in ×.
decompose [ex and or] H;clear H;
∃ x;Col5.
Qed.

Lemma coplanar_perm_7 : ∀ A B C D,
 coplanar A B C D → coplanar B A D C.
Proof.
intros.
unfold coplanar in ×.
decompose [ex and or] H;clear H;
∃ x;Col5.
Qed.

Lemma coplanar_perm_8 : ∀ A B C D,
 coplanar A B C D → coplanar B C A D.
Proof.
intros.
unfold coplanar in ×.
decompose [ex and or] H;clear H;
∃ x;Col5.
Qed.

Lemma coplanar_perm_9 : ∀ A B C D,
 coplanar A B C D → coplanar B C D A.
Proof.
intros.
unfold coplanar in ×.
decompose [ex and or] H;clear H;
∃ x;Col5.
Qed.

Lemma coplanar_perm_10 : ∀ A B C D,
 coplanar A B C D → coplanar B D A C.
Proof.
intros.
unfold coplanar in ×.
decompose [ex and or] H;clear H;
∃ x;Col5.
Qed.

Lemma coplanar_perm_11 : ∀ A B C D,
 coplanar A B C D → coplanar B D C A.
Proof.
intros.
unfold coplanar in ×.
decompose [ex and or] H;clear H;
∃ x;Col5.
Qed.


Lemma per_per_col : ∀ A B C X, Per A X C → X ≠ C → Per B X C → Col A B X.
Proof.
intros.
unfold Per in ×.
ex_and H C'.
ex_and H1 C''.
assert (C' = C'').
eapply symmetric_point_unicity.
apply H.
apply H1.
subst C''.
eapply upper_dim.
2:apply H2.
intro.
subst C'.
apply l7_3 in H1.
apply H0.
assumption.
assumption.
unfold is_midpoint in H.
spliter.
Cong.
Qed.

Lemma per_per_perp : ∀ A B X Y,
 A ≠ B → X ≠ Y →
 (B ≠ X ∨ B ≠ Y) → Per A B X → Per A B Y →
 Perp A B X Y.
Proof.
intros.
induction H1.

assert(HH:=H2).
apply per_perp_in in H2; auto.
apply perp_in_perp in H2.
induction H2.
apply perp_not_eq_1 in H2.
tauto.
apply perp_sym.
apply (perp_col _ B); auto.
Perp.
apply col_permutation_5.
eapply (per_per_col _ _ A); Perp.

assert(HH:=H3).
apply per_perp_in in H3; auto.
apply perp_in_perp in H3.
induction H3.
apply perp_not_eq_1 in H3.
tauto.
apply perp_sym.
apply perp_left_comm.
apply (perp_col _ B); auto.
Perp.
apply col_permutation_5.
eapply (per_per_col _ _ A); Perp.
Qed.

Lemma midpoint_preserves_image : ∀ A B P P' Q Q' M,
 A ≠ B → Col A B M → is_image P P' A B →
 is_midpoint M P Q → is_midpoint M P' Q' → is_image Q Q' A B.
Proof.
intros.
rewrite is_image_is_image_spec in × by apply H.

assert (HH1:=H1).
unfold is_image_spec in H1.
spliter.
ex_and H1 X.
induction H4.

double X M Y.

assert (is_midpoint Y Q Q').
eapply symmetry_preserves_midpoint.
apply H2.
apply H6.
apply H3.
apply l7_2.
apply H1.

assert (P ≠ P').
intro.
subst P'.
apply perp_distinct in H4.
spliter.
absurde.

assert (Q ≠ Q').
intro.
subst Q'.
apply l7_3 in H7.
subst Q.
assert (P=P').
eapply l7_9.
apply H2.
apply H3.
subst P'.
apply perp_distinct in H4.
spliter.
absurde.

split.
∃ Y.
split.
apply l7_2.
apply H7.
induction (eq_dec_points X Y).
subst Y.
assumption.

eapply (colx _ _ M X).
assumption.
intro.
subst X.
apply is_midpoint_id in H6.
subst Y.
absurde.
intro.
subst Y.
apply l7_2 in H6.
apply is_midpoint_id in H6.
subst X.
absurde.
assumption.
assumption.
unfold Col.
right; right.
apply midpoint_bet.
apply l7_2.
assumption.

left.

assert(Per M Y Q).
unfold Per.
∃ Q'.
split.
assumption.
unfold is_midpoint in ×.
spliter.
eapply cong_transitivity.
apply cong_symmetry.
apply H14.
apply cong_symmetry.
eapply cong_transitivity.
apply cong_symmetry.
apply H13.
eapply is_image_col_cong.
apply H.
apply l10_4.
apply is_image_is_image_spec.
assumption.
apply HH1.
assumption.

induction (eq_dec_points X Y).
subst Y.
apply l7_3 in H6.
subst X.

apply perp_sym.
eapply perp_col.
auto.
apply perp_left_comm.
eapply perp_col.
2:apply perp_sym.
2:apply H4.
intro.
subst Q'.
apply l7_3 in H3.
subst P'.
apply is_midpoint_id in H1.
subst P.
absurde.
eapply (col_transitivity_2 M).
intro.
subst P'.
apply is_midpoint_id in H1.
subst P.
absurde.
unfold Col.
right; right.
apply midpoint_bet.
apply l7_2.
assumption.
unfold Col.
right; right.
apply midpoint_bet.
apply l7_2.
assumption.

eapply (col_transitivity_2 M).
intro.
subst Q'.
apply l7_2 in H7.
apply is_midpoint_id in H7.
subst Q.
absurde.
unfold Col.
right; right.
apply midpoint_bet.
assumption.
unfold Col.
right; right.
apply midpoint_bet.
assumption.

apply per_perp_in in H10.
apply perp_in_perp in H10.
induction H10.
apply perp_distinct in H10.
spliter.
absurde.
apply perp_comm.
apply perp_sym.
eapply perp_col.

assumption.
apply perp_comm.

eapply (perp_col Y Q).
intro.
subst Q.
apply perp_distinct in H10.
spliter.
absurde.
apply perp_sym.

induction (eq_dec_points A M).
subst A.
apply perp_left_comm.

eapply (perp_col _ M).
auto.
apply perp_left_comm.
eapply (perp_col _ Y).
assumption.
assumption.
induction (eq_dec_points M X).
subst X.

apply is_midpoint_id in H6.
subst M.
apply col_trivial_1.
eapply (col_transitivity_1 _ X).
assumption.
unfold Col.
right; right.
apply midpoint_bet.
apply l7_2.
assumption.
apply col_permutation_5.
assumption.
apply col_trivial_2.

induction (eq_dec_points B M).
subst M.
apply perp_left_comm.

apply (perp_col _ Y).
auto.
assumption.
induction (eq_dec_points B X).
subst X.
apply is_midpoint_id in H6.
subst Y.
absurde.
eapply col_transitivity_1.
apply H13.
unfold Col.
right; right.
apply midpoint_bet.
apply l7_2.
assumption.
apply col_permutation_1.
assumption.
eapply perp_col.
assumption.
apply perp_left_comm.
eapply (perp_col M Y).
auto.
assumption.

assert(Col B X M).
eapply col_transitivity_2.
apply H.
assumption.
assumption.
induction (eq_dec_points M X).
subst X.
apply is_midpoint_id in H6.
contradiction.
assert(Col B Y M).
apply col_permutation_1.
eapply (col_transitivity_2 X).
auto.
apply col_permutation_1.
assumption.
unfold Col.
left.
apply midpoint_bet.
assumption.
eapply (col_transitivity_1 _ B).
auto.
apply col_permutation_2.
assumption.
apply col_permutation_3.
apply H0.
apply col_permutation_5.
apply H0.
apply col_trivial_2.
unfold Col.
left.
apply midpoint_bet.
apply H7.
intro.
subst Y.
apply l7_2 in H6.
apply is_midpoint_id in H6.
subst X.
absurde.
intro.
subst Q.
apply is_midpoint_id in H7.
subst Q'.
absurde.

subst P'.
apply l7_3 in H1.
subst P.
assert(Q = Q').
eapply l7_9.
apply l7_2.
apply H2.
apply l7_2.
apply H3.
subst Q'.

split.
∃ Q.
split.
apply l7_3_2.
induction (eq_dec_points M X).
subst X.
assert(M=Q).
apply is_midpoint_id.
assumption.
subst Q.
assumption.
eapply colx.
assumption.
apply H1.
intro.
subst Q.
apply l7_3 in H2.
contradiction.
assumption.
assumption.
unfold Col.
left.
apply midpoint_bet.
apply H3.
right.
reflexivity.

Qed.

Definition is_image_spec_in M P' P A B :=
  (is_midpoint M P P' ∧ Col A B M) ∧ (Perp A B P P' ∨ P=P').

Definition is_image_spec_in_gen M P' P A B :=
 (A ≠ B ∧ is_image_spec_in M P' P A B) ∨ (A=B ∧ A=M ∧ is_midpoint M P P').

Lemma image_in_is_image_spec :
 ∀ M A B P P',
  is_image_spec_in M P P' A B → is_image_spec P P' A B.
Proof.
intros.
unfold is_image_spec_in in H.
spliter.
unfold is_image_spec.
split.
∃ M.
split;
assumption.
assumption.
Qed.

Lemma image_in_gen_is_image : ∀ M A B P P',
 is_image_spec_in_gen M P P' A B → is_image P P' A B.
Proof.
intros.
unfold is_image_spec_in_gen in H.
induction H.
spliter.
apply image_in_is_image_spec in H0.
unfold is_image.
tauto.
spliter.
subst.
subst.
unfold is_image.
right.
auto.
Qed.

Lemma image_image_in : ∀ A B P P' M,
 P ≠ P'→ is_image_spec P P' A B → Col A B M → Col P M P' →
 is_image_spec_in M P P' A B.
Proof.
intros.
unfold is_image_spec_in.
split.
split.

assert(HH:=H0).
unfold is_image_spec in H0.
spliter.
ex_and H0 M'.

induction H3.

assert (Perp P M' A B).
eapply perp_col.
intro.
subst P.
apply l7_2 in H0.
apply is_midpoint_id in H0.
subst P'.
apply perp_distinct in H3.
spliter.
absurde.
apply perp_sym.
apply perp_right_comm.
apply H3.
unfold Col.
right; left.
apply midpoint_bet.
assumption.

assert (M'=M).

eapply inter_unicity.
apply H4.
unfold Col.
right; left.
apply midpoint_bet.
apply H0.
assumption.
apply col_permutation_5.
assumption.

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

assert (¬ Col A B P ∧ Per P A B).
eapply l8_16_1.
apply perp_distinct in H3.
spliter.
assumption.
apply col_trivial_3.
apply col_trivial_2.
apply perp_distinct in H3.
spliter.
auto.
apply perp_sym.
assumption.
spliter.
intro.
apply H6.
apply col_permutation_5.
assumption.

assert (¬ Col A B P ∧ Per P M' A).
eapply l8_16_1.
apply perp_distinct in H3.
spliter.
assumption.
assumption.
apply col_trivial_3.
assumption.
apply perp_sym.
assumption.
spliter.
intro.
apply H7.
apply col_permutation_5.
assumption.
apply perp_distinct in H3.
spliter.
auto.
subst M'.
assumption.

subst P'.
absurde.
assumption.

assert (HH:=H0).
unfold is_image_spec in H0.
spliter.
induction H3.
left.
assumption.
right.
assumption.
Qed.

Lemma image_in_col : ∀ A B P P' Q Q' M,
 is_image_spec_in M P P' A B → is_image_spec_in M Q Q' A B →
 Col M P Q.
Proof.
intros.

assert(is_image_spec P P' A B).
eapply (image_in_is_image_spec M).
assumption.
assert(is_image_spec Q Q' A B).
eapply (image_in_is_image_spec M).
assumption.
unfold is_image_spec_in in ×.
spliter.
induction H3.
induction H5.

induction (eq_dec_points A M).
subst M.

assert (Per B A P).
 unfold Per.
 ∃ P'.
 split.
 apply l7_2.
 assumption.
 apply cong_commutativity.
 eapply is_image_spec_col_cong with A B;Col.

assert (Per B A Q).
 unfold Per.
 ∃ Q'.
 split.
 apply l7_2.
 assumption.
 apply cong_commutativity.
 eapply is_image_spec_col_cong with A B;Col.

apply col_permutation_2.
eapply per_per_col.
apply l8_2.
apply H7.
apply perp_distinct in H3.
spliter.
assumption.
apply l8_2.
assumption.

assert (Per A M P).
 unfold Per.
 ∃ P'.
 split.
 apply l7_2.
 assumption.
 apply cong_commutativity.
 eapply is_image_spec_col_cong.
 apply H1.
 Col.

assert (Per A M Q).
 unfold Per.
 ∃ Q'.
 split.
 apply l7_2.
 assumption.
 apply cong_commutativity.
 eapply is_image_spec_col_cong.
 apply H2.
 apply col_trivial_3.

apply col_permutation_2.
eapply per_per_col.
apply l8_2.
apply H8.
auto.
apply l8_2.
assumption.

subst P'.
apply l7_3 in H.
subst P.
Col.
subst Q'.
apply l7_3 in H0.
subst Q.
Col.
Qed.

Lemma image_in_col0 : ∀ A B P P' Y : Tpoint,
 is_image_spec_in Y P P' A B → Col P P' Y.
Proof.
intros.
unfold is_image_spec_in in ×.
spliter.
assert_cols.
Col.
Qed.

Lemma l10_10_spec : ∀ A B P Q P' Q',
 A≠B → is_image_spec P' P A B → is_image_spec Q' Q A B →
 Cong P Q P' Q'.
Proof.
intros.
assert(HH0 := H0).
assert(HH1 := H1 ).
unfold is_image_spec in H0.
unfold is_image_spec in H1.
spliter.
ex_and H0 X.
ex_and H1 Y.
assert (∃ M, is_midpoint M X Y).
   apply midpoint_existence.
ex_elim H6 M.
double P M P''.
double Q M Q''.
double P' M P'''.
apply cong_commutativity.
induction H3.

induction H2.

assert (is_image_spec P'' P''' A B).
 apply is_image_is_image_spec .
 assumption.
 eapply (midpoint_preserves_image ) with P P' M.
 assumption.

 induction (eq_dec_points X Y).
 subst Y.
 apply l7_3 in H7.
 subst X.
 assumption.
 assert_cols.
 ColR.

 apply l10_4.
 apply is_image_is_image_spec;auto.
 assumption.
 assumption.

assert(P'' ≠ P''').
 intro.
 subst P'''.
 assert( P' = P).
 eapply l7_9.
 apply H9.
 assumption.
 subst P'.
 apply perp_distinct in H3.
 spliter.
 absurde.

assert (is_midpoint Y P'' P''')
 by (eauto using symmetry_preserves_midpoint).

assert (Cong P'' Y P''' Y)
 by (unfold is_midpoint in *; spliter; Cong).

assert (Cong Q Y Q' Y)
 by (unfold is_midpoint in *;spliter; Cong).

assert (Col P'' Y Q).
 apply col_permutation_2.
 eapply image_in_col.
 eapply image_image_in.
 apply perp_distinct in H2.
 spliter.
 apply H15.
 apply l10_4_spec.
 apply HH1.
 assumption.
 unfold Col.
 left.
 apply midpoint_bet.
 assumption.
 eapply (image_image_in _ _ _ P''').
 assumption.
 assumption.
 assumption.
 unfold Col.
 left.
 apply midpoint_bet.
 assumption.

eapply (l4_16 P'' Y Q P P''' Y Q' P').

repeat split.

assumption.
assumption.

unfold Col in H15.
induction H15.
assert(Bet P''' Y Q').
eapply (l7_15).
apply H12.
apply l7_3_2.
apply H1.
assumption.

eapply l2_11.
apply H15.
apply H16.
assumption.
apply cong_commutativity.
assumption.
induction H15.

assert (Bet Y Q' P''').
eapply (l7_15).
apply l7_3_2.
apply H1.
apply H12.
assumption.

eapply l4_3.
apply between_symmetry.
apply H15.
apply between_symmetry.
apply H16.
assumption.
assumption.

apply between_symmetry in H15.

assert (Bet Y P''' Q').
eapply (l7_15).
apply l7_3_2.
apply H12.
apply H1.
assumption.
apply cong_commutativity.

eapply l4_3.
apply between_symmetry.
apply H15.
apply between_symmetry.
apply H16.
assumption.
assumption.
apply cong_commutativity.
assumption.

assert (Cong P Y P' Y).
   eapply is_image_spec_col_cong.
   eapply l10_4_spec.
   apply HH0.
   assumption.
assert (Cong P P'' P' P''').
   induction(eq_dec_points X Y).
      subst Y.
      eapply l2_11.
apply midpoint_bet.
         apply H6.
         apply H9.
         apply l7_3 in H7.
         subst X.
         assumption.
         apply l7_3 in H7.
         subst X.
         eapply cong_transitivity.
            unfold is_midpoint in H6.
            spliter.
            apply cong_symmetry.
            apply H7.
            eapply cong_transitivity.
               apply H16.
               unfold is_midpoint in H9.
               spliter.
               assumption.

eapply l2_11.
         apply H6.
         apply H9.
         eapply is_image_spec_col_cong.
            apply l10_4_spec.
            apply HH0.
            unfold is_midpoint in H7.
            spliter.
            eapply colx.
            assumption.
            3:apply H4.
            3:apply H5.
            auto.
            intro.
            subst X.
            apply cong_symmetry in H18.
            apply cong_identity in H18.
subst Y.
absurde.
unfold Col.
right; left.
apply between_symmetry.
assumption.
apply cong_commutativity.
eapply is_image_spec_col_cong.
apply H10.

eapply colx.
                     4:apply H4.
                     4:apply H5.
                     assumption.
                     auto.
                     intro.
                     subst X.
                     apply is_midpoint_id in H7.
                     contradiction.
unfold Col.
right; left.
apply midpoint_bet.
apply l7_2.
assumption.
apply cong_commutativity.

assumption.
apply cong_commutativity.
eapply is_image_spec_col_cong.
apply l10_4_spec.
apply HH0.
assumption.
intro.
subst P''.
apply cong_symmetry in H13.
apply cong_identity in H13.
subst P'''.
absurde.

subst Q'.
apply l7_3 in H1.
subst Q.
apply cong_commutativity.
eapply is_image_spec_col_cong.
apply l10_4_spec.
apply HH0.
assumption.

subst P'.
apply l7_3 in H0.
subst P.
eapply is_image_spec_col_cong.

apply l10_4_spec.
apply HH1.
assumption.
Qed.

Lemma l10_10 : ∀ A B P Q P' Q',
  is_image P' P A B → is_image Q' Q A B →
 Cong P Q P' Q'.
Proof.
intros.
induction (eq_dec_points A B).
subst.
unfold is_image in ×.
induction H.
intuition.
induction H0.
intuition.
spliter.
apply l7_13 with B;
apply l7_2;auto.

rewrite is_image_is_image_spec in × by apply H1.
apply l10_10_spec with A B;auto.
Qed.

Lemma is_image_spec_rev : ∀ P P' A B, is_image_spec P P' A B → is_image_spec P P' B A.
Proof.
unfold is_image_spec.
intros.
spliter.
split.
ex_and H M.
∃ M.
split.
assumption.
apply col_permutation_4.
assumption.
induction H0.
left.
apply perp_left_comm.
assumption.
right.
assumption.
Qed.

Lemma is_image_rev : ∀ P P' A B,
 is_image P P' A B → is_image P P' B A.
Proof.
intros.
unfold is_image in ×.
induction H.
spliter.
left.
split.
auto.
apply is_image_spec_rev.
assumption.
right.
spliter. subst. tauto.
Qed.

Lemma per_double_cong : ∀ A B C C',
 Per A B C → is_midpoint B C C' → Cong A C A C'.
Proof.
intros.
unfold Per in H.
ex_and H C''.
assert (C' = C'').
eapply l7_9.
apply l7_2.
apply H0.
apply l7_2.
assumption.
subst C''.
assumption.
Qed.

Lemma midpoint_preserves_per : ∀ A B C A1 B1 C1 M,
 Per A B C →
 is_midpoint M A A1 →
 is_midpoint M B B1 →
 is_midpoint M C C1 →
 Per A1 B1 C1.
Proof.
intros.
unfold Per in ×.
ex_and H C'.
double C' M C1'.
∃ C1'.
split.
eapply symmetry_preserves_midpoint.
apply H2.
apply H1.
apply H4.
assumption.
eapply l7_16.
apply H0.
apply H2.
apply H0.
apply H4.
assumption.
Qed.

Lemma image_preserves_bet : ∀ A B C A' B' C' X Y,
   X ≠ Y →
  is_image_spec A A' X Y → is_image_spec B B' X Y → is_image_spec C C' X Y →
  Bet A B C →
  Bet A' B' C'.
Proof.
intros.
eapply l4_6.
apply H3.
unfold Cong_3.

repeat split;
eapply l10_10_spec.
apply H.
apply l10_4_spec.
assumption.
apply l10_4_spec;
assumption.

apply H.
apply l10_4_spec.
assumption.
apply l10_4_spec.
assumption.

apply H.
apply l10_4_spec.
assumption.
apply l10_4_spec.
assumption.
Qed.

Lemma image_gen_preserves_bet : ∀ A B C A' B' C' X Y,
   X ≠ Y →
  is_image A A' X Y →
  is_image B B' X Y →
  is_image C C' X Y →
  Bet A B C →
  Bet A' B' C'.
Proof.
intros.
rewrite is_image_is_image_spec in × by apply H.
eapply image_preserves_bet;eauto.
Qed.

Lemma image_preserves_midpoint :
 ∀ A B C A' B' C' X Y, X ≠ Y →
 is_image_spec A A' X Y → is_image_spec B B' X Y → is_image_spec C C' X Y →
 is_midpoint A B C →
 is_midpoint A' B' C'.
Proof.
intros.
unfold is_midpoint in ×.
spliter.
repeat split.
eapply image_preserves_bet.
apply H.
apply H1.
apply H0.
apply H2.
assumption.
eapply cong_transitivity.
eapply l10_10_spec.
apply H.
apply H1.
apply H0.
eapply cong_transitivity.
apply H4.
eapply l10_10_spec.
apply H.
apply l10_4_spec.
apply H0.
apply l10_4_spec.
apply H2.
Qed.

Lemma image_preserves_per : ∀ A B C A' B' C' X Y,
  X ≠ Y →
 is_image_spec A A' X Y → is_image_spec B B' X Y → is_image_spec C C' X Y →
 Per A B C →
 Per A' B' C'.
Proof.
intros.
double C B C1.
assert (∃ C1', is_image_spec C1 C1' X Y).
apply l10_6_existence_spec.
assumption.
ex_and H5 C1'.
unfold Per.
∃ C1'.
split.
eapply image_preserves_midpoint.
apply H.
apply H1.
apply H2.
apply H6.
assumption.
eapply cong_transitivity.
eapply l10_10_spec.
apply H.
apply H0.
apply H2.
eapply cong_transitivity.
unfold Per in H3.
ex_and H3 C2.
assert (C2=C1).
eapply symmetric_point_unicity.
apply H3.
assumption.
subst C2.
apply H5.
eapply l10_10_spec.
apply H.
apply l10_4_spec.
assumption.
apply l10_4_spec.
assumption.
Qed.

Lemma col_per_perp : ∀ A B C D,
 A ≠ B → B ≠ C → D ≠ B → D ≠ C →
 Col B C D → Per A B C → Perp C D A B.
Proof.
intros.
apply per_perp_in in H4.
apply perp_in_perp in H4.
induction H4.
apply perp_distinct in H4.
spliter.
absurde.
eapply (perp_col _ B).
auto.
apply perp_sym.
apply perp_right_comm.
assumption.
apply col_permutation_4.
assumption.
assumption.
assumption.
Qed.

Lemma image_col : ∀ A B X, Col A B X → is_image_spec X X A B.
Proof.
intros.
unfold is_image_spec.
split.
∃ X.
split.
apply l7_3_2.
assumption.
right.
reflexivity.
Qed.

Lemma is_image_spec_triv : ∀ A B, is_image_spec A A B B.
Proof.
intros.
apply image_col.
Col.
Qed.

Lemma is_image_spec_dec :
  ∀ A B C D, is_image_spec A B C D ∨ ¬ is_image_spec A B C D.
Proof.
intros.
elim (eq_dec_points C D); intro HCD.

  subst.
  elim (eq_dec_points A B); intro HAB.

    subst.
    left.
    apply is_image_spec_triv.

    right.
    intro H.
    unfold is_image_spec in ×.
    destruct H as [H HFalse].
    elim HFalse; clear HFalse; intro HFalse.

      apply perp_distinct in HFalse.
      intuition.

      intuition.

  elim (l10_6_existence_spec C D A HCD); intros B' HB'.
  elim (eq_dec_points B B'); intro HBB'.

    subst.
    tauto.

    right.
    intro H.
    apply HBB'.
    apply l10_6_unicity with C D A.

      unfold is_image.
      tauto.

      unfold is_image.
      tauto.
Qed.

Lemma l10_12 : ∀ A B C A' B' C',
 Per A B C → Per A' B' C' →
 Cong A B A' B' → Cong B C B' C' →
 Cong A C A' C'.
Proof.
intros.

induction (eq_dec_points B C).
   subst B.
   apply cong_symmetry in H2.
   apply cong_identity in H2.
   subst B'.
   assumption.

induction (eq_dec_points A B).
   subst B.
   apply cong_symmetry in H1.
   apply cong_identity in H1.
   subst B'.
   assumption.

assert (∃ X, is_midpoint X B B').
   apply midpoint_existence.

ex_and H5 X.
double A' X A1.
double C' X C1.

assert(Cong_3 A' B' C' A1 B C1).
   repeat split.
      eapply l7_13.
            apply l7_2.
            apply H5.
            assumption.
      eapply l7_13.
            apply l7_2.
            apply H5.
            apply l7_2.
            assumption.
      eapply l7_13.
         apply H6.
         apply l7_2.
         assumption.

assert (Per A1 B C1).
   eapply l8_10.
      apply H0.
      apply H8.

unfold Cong_3 in H8.
spliter.

assert(Cong A B A1 B).
   eapply cong_transitivity.
   apply H1.
   assumption.

assert(Cong B C B C1).
   eapply cong_transitivity.
   apply H2.
   assumption.

assert(∃ Y, is_midpoint Y C C1).
   apply midpoint_existence.
ex_and H14 Y.

apply cong_symmetry.
eapply cong_transitivity.
   apply H10.

induction (eq_dec_points B Y).
subst Y.

induction (eq_dec_points A A1).
subst A1.
unfold Per in H9.
ex_and H9 C2.
assert (C=C2).

eapply l7_9.
apply H15.
apply l7_2.
assumption.
subst C2.
assumption.

assert(C1 ≠ B).
intro.
subst C1.
apply l7_2 in H15.
apply is_midpoint_id in H15.
contradiction.

assert (Per C B A1).
eapply (l8_3 C1 B A1 C).

apply l8_2.
apply H9.
assumption.
apply midpoint_col.
apply l7_2.
assumption.

assert(Col A A1 B).
eapply per_per_col.
apply H.
assumption.
apply l8_2.
assumption.

assert (A= A1 ∨ is_midpoint B A A1).
eapply l7_20.
apply col_permutation_5.
assumption.
apply cong_commutativity.
assumption.
induction H19.
contradiction.
eapply l7_13.
apply H19.
assumption.

assert(is_image_spec C1 C B Y).
unfold is_image_spec.
split.
∃ Y.
split.
assumption.
apply col_trivial_2.
induction(eq_dec_points C C1).
right.
assumption.
left.
apply perp_sym.
assert(Y≠C ∧ Y ≠ C1).
eapply midpoint_distinct_1.
assumption.
assumption.
spliter.

eapply col_per_perp.
assumption.
auto.
intuition.
auto.
apply midpoint_col.
assumption.

unfold Per.
∃ C1.
split.
assumption.
assumption.

induction (is_image_spec_dec A A1 B Y).

eapply l10_10_spec.

2:apply H17.
assumption.
apply l10_4_spec.
assumption.


assert(∃ A2, is_image_spec A1 A2 B Y).

apply l10_6_existence_spec.
assumption.
ex_elim H18 A2.

assert (Cong C A2 C1 A1).
eapply l10_10_spec.
2:apply H16.
assumption.
assumption.

assert (Per A2 B C).
eapply (image_preserves_per A1 B C1 A2 B C).
2:apply H19.
assumption.
apply image_col.
apply col_trivial_3.
assumption.
assumption.

assert (Cong A1 B A2 B).
eapply is_image_spec_col_cong.
apply H19.
apply col_trivial_3.

assert (A = A2 ∨ is_midpoint B A A2).
eapply l7_20.
apply col_permutation_1.
eapply per_per_col.
apply H20.
assumption.
assumption.
eapply cong_transitivity.
apply cong_commutativity.
apply H12.
apply cong_commutativity.
assumption.

induction H22.
subst A2.
apply cong_symmetry.
apply cong_commutativity.
assumption.

assert(Cong A C A2 C).
apply l8_2 in H.
unfold Per in H.
ex_and H A3.
assert(A2=A3).
eapply symmetric_point_unicity.
apply H22.
apply H.
subst A3.
apply cong_commutativity.
assumption.

eapply cong_transitivity.
apply cong_symmetry.
apply cong_commutativity.
apply H18.
apply cong_symmetry.
assumption.
Qed.

Lemma l10_14 : ∀ P P' A B, P ≠ P' → A ≠ B →
 is_image P P' A B → two_sides A B P P'.
Proof.
intros.

rewrite is_image_is_image_spec in H1 by apply H0.

unfold is_image_spec in H1.
spliter.
ex_and H1 M.
induction H2.

assert (P ≠ M).
intro.
subst P.
apply l7_2 in H1.
apply is_midpoint_id in H1.
subst P'.
absurde.

induction (eq_dec_points A M).
subst A.
assert (Perp M B P M).
apply perp_sym.
eapply (perp_col _ P').
assumption.

apply perp_sym.
apply perp_right_comm.
apply H2.
unfold Col.
right; left.
apply midpoint_bet.
assumption.

assert (Perp_in M M B P M).
eapply perp_perp_in.
assumption.
assert(Per B M P).
eapply perp_in_per.
apply perp_in_comm.
assumption.

assert (B ≠ M).
intro.
repeat split.
subst B.
apply perp_distinct in H2.
spliter.
absurde.

assert (¬Col B M P).
eapply per_not_col.
assumption.
auto.
assumption.
repeat split.
auto.
intro.
apply H9.
Col.
intro.
apply H9.
apply col_permutation_2.
eapply (col_transitivity_1 _ P').
intro.
subst P'.
apply is_midpoint_id in H1.
subst P.
absurde.

unfold Col.
right; right.
apply midpoint_bet.
apply l7_2.
assumption.
apply col_permutation_4.
assumption.
∃ M.
split.
apply col_trivial_1.
apply midpoint_bet.
apply l7_2.
assumption.

induction (eq_dec_points B M).
subst B.
assert (Perp M A P M).
apply perp_sym.
eapply (perp_col _ P').
assumption.

apply perp_sym.
apply perp_comm.
apply H2.
unfold Col.
right; left.
apply midpoint_bet.
assumption.

assert (Perp_in M M A P M).
eapply perp_perp_in.
assumption.
assert(Per A M P).
eapply perp_in_per.
apply perp_in_comm.
assumption.

repeat split.
assumption.

assert (¬Col A M P).
eapply per_not_col.
assumption.
auto.
assumption.
intro.
apply H9.
apply col_permutation_1.
assumption.
intro.

assert (Col M A P).
eapply (col_transitivity_1 _ P').
intro.
subst P'.
apply is_midpoint_id in H1.
subst P.
absurde.
apply col_permutation_2.
assumption.
unfold Col.
right; right.
apply midpoint_bet.
apply l7_2.
assumption.

eapply (per_not_col ).
3: apply H8.
assumption.
auto.
apply col_permutation_4.
assumption.
∃ M.
split.
apply col_trivial_3.
apply midpoint_bet.
apply l7_2.
assumption.

repeat split.
apply perp_distinct in H2.
spliter.
assumption.

assert(Perp P M A B).
eapply perp_col.
assumption.
apply perp_sym.
apply perp_right_comm.
apply H2.
unfold Col.
right; left.
apply midpoint_bet.
assumption.
assert (¬ Col M P A).

apply perp_not_col.
apply perp_sym.
eapply perp_col.
assumption.
apply perp_sym.
apply perp_left_comm.
apply H7.
assumption.
intro.
apply H8.
apply col_permutation_1.
eapply col_transitivity_1.
apply perp_distinct in H2.
spliter.
apply H2.
assumption.
apply col_permutation_1.
assumption.

assert(Perp P' M A B).
eapply perp_col.
intro.
subst P'.
apply is_midpoint_id in H1.
subst P.
absurde.
apply perp_sym.
apply H2.
unfold Col.
right; left.
apply midpoint_bet.
apply l7_2.
assumption.

assert (¬ Col M P' A).

apply perp_not_col.
apply perp_sym.
eapply perp_col.
assumption.
apply perp_sym.
apply perp_left_comm.
apply H7.
assumption.
intro.
apply H8.
apply col_permutation_1.
eapply col_transitivity_1.
apply perp_distinct in H2.
spliter.
apply H2.
assumption.
apply col_permutation_1.
assumption.

∃ M.
split.
apply col_permutation_2.
assumption.
apply midpoint_bet.
apply l7_2.
assumption.

subst P'.
absurde.
Qed.

Lemma l10_15 : ∀ A B C P,
 Col A B C → ¬ Col A B P →
 ∃ Q, Perp A B Q C ∧ one_side A B P Q.
Proof.
intros.
assert (A≠B).
 intro;subst.
 Col.

assert (∃ X , two_sides A B P X).

apply l9_10.
assumption.
intro.
apply H0.
apply col_permutation_1.
assumption.

ex_elim H2 X.

induction (eq_dec_points A C).

subst C.

assert (∃ Q, ∃ T, Perp A B Q A ∧ Col A B T ∧ Bet X T Q).
apply l8_21.
assumption.

ex_elim H2 Q.
ex_and H4 T.
∃ Q.
split.
assumption.
eapply l9_8_1.
apply H3.
unfold two_sides.
repeat split.
assumption.
apply perp_not_col in H2.
intro.
apply H2.
apply col_permutation_1.
assumption.
unfold two_sides in H3.
spliter.
assumption.
∃ T.
split.
apply col_permutation_2.
assumption.
apply between_symmetry.
assumption.

assert (∃ Q, ∃ T, Perp C A Q C ∧ Col C A T ∧ Bet X T Q).
apply l8_21.
auto.
ex_elim H4 Q.
ex_and H5 T.
∃ Q.
split.

eapply perp_col.
assumption.
apply perp_left_comm.
apply H4.
apply col_permutation_5.
assumption.
eapply l9_8_1.
apply H3.

unfold two_sides.
repeat split.
assumption.
eapply perp_not_col in H4.
intro.
apply H4.
apply col_permutation_2.
eapply col_transitivity_1.
apply H1.
apply col_permutation_1.
assumption.
assumption.
unfold two_sides in H3.
spliter.
assumption.
∃ T.
split.
apply col_permutation_2.
eapply col_transitivity_1.
apply H2.
apply col_permutation_5.
assumption.
apply col_permutation_4.
assumption.
apply between_symmetry.
assumption.
Qed.

Lemma l10_16 : ∀ A B C A' B' P,
 ¬ Col A B C → ¬ Col A' B' P → Cong A B A' B' →
 ∃ C', Cong_3 A B C A' B' C' ∧ one_side A' B' P C' .
Proof.
intros.

induction (eq_dec_points A B).
subst B.
apply cong_symmetry in H1.
apply False_ind.
apply H.
apply col_trivial_1.

assert(∃ X, Col A B X ∧ Perp A B C X).
apply l8_18_existence.
assumption.
ex_and H3 X.
assert (∃ X', Cong_3 A B X A' B' X').
eapply l4_14.
assumption.
assumption.
ex_elim H5 X'.

assert (∃ Q, Perp A' B' Q X' ∧ one_side A' B' P Q).
apply l10_15.

eapply l4_13.
apply H3.
assumption.
assumption.
ex_and H5 Q.

assert (∃ C', out X' C' Q ∧ Cong X' C' X C).
eapply l6_11_existence.
apply perp_distinct in H5.
spliter.
assumption.
intro.
subst C.
apply perp_distinct in H4.
spliter.
absurde.

ex_and H8 C'.
∃ C'.

unfold Cong_3 in ×.
spliter.

assert (Cong A C A' C').

induction(eq_dec_points A X).
subst X.
apply cong_symmetry in H10.
apply cong_identity in H10.
subst X'.
apply cong_symmetry.
assumption.

eapply l10_12.
3: apply H10.
apply perp_in_per.
eapply l8_14_2_1b_bis.
eapply perp_col.
assumption.
apply perp_right_comm.
apply H4.
assumption.
apply col_trivial_3.
apply col_trivial_1.
apply perp_in_per.
eapply l8_14_2_1b_bis.
eapply perp_col.
intro
assumption.
subst X'.
apply cong_identity in H10.
contradiction.
apply perp_sym.
eapply perp_col.
intro.
subst X'.
apply cong_symmetry in H9.
apply cong_identity in H9.
subst X.
apply perp_distinct in H4.
spliter.
absurde.
apply perp_sym.
apply perp_right_comm.
apply H5.
apply col_permutation_5.
eapply out_col.
assumption.
eapply l4_13.
apply H3.
unfold Cong_3.
repeat split;assumption.
apply col_trivial_3.
apply col_trivial_1.
apply cong_symmetry.
assumption.

assert (Cong B C B' C').

induction(eq_dec_points B X).
subst X.
apply cong_symmetry in H11.
apply cong_identity in H11.
subst X'.
apply cong_symmetry.
assumption.

eapply l10_12.
3: apply H11.
apply perp_in_per.
eapply l8_14_2_1b_bis.
eapply perp_col.
assumption.
apply perp_comm.
apply H4.
apply col_permutation_4.
assumption.
apply col_trivial_3.
apply col_trivial_1.
apply perp_in_per.
eapply l8_14_2_1b_bis.
eapply perp_col.
intro
assumption.
subst X'.
apply cong_identity in H11.
contradiction.
apply perp_sym.
eapply perp_col.
intro.
subst X'.
apply cong_symmetry in H9.
apply cong_identity in H9.
subst X.
apply perp_distinct in H4.
spliter.
absurde.
apply perp_sym.
apply perp_comm.
apply H5.
apply col_permutation_5.
eapply out_col.
assumption.
apply col_permutation_4.
eapply l4_13.
apply H3.
unfold Cong_3.
repeat split;
assumption.

apply col_trivial_3.
apply col_trivial_1.
apply cong_symmetry.
assumption.
repeat split.
assumption.
assumption.
assumption.

assert (T19 := (l9_19 A' B' C' Q X')).
assert (one_side A' B' C' Q ↔ out X' C' Q ∧ ¬ Col A' B' C').
apply T19.
intro.
subst B'.
apply cong_identity in H1.
contradiction.
eapply l4_13.
apply H3.
unfold Cong_3.
repeat split;
assumption.
apply col_permutation_1.
apply out_col.
assumption.
apply cong_symmetry in H1.
destruct H14.
spliter.
assert (one_side A' B' C' Q).
apply H15.
split.
assumption.
intro.
apply H.
eapply l4_13.
apply H16.
unfold Cong_3.
repeat split.
assumption.
apply cong_symmetry.
assumption.
apply cong_symmetry.
assumption.
eapply one_side_transitivity.
apply H7.
apply one_side_symmetry.
assumption.
Qed.

Lemma not_col_exists : ∀ A B, A ≠ B → ∃ P, ¬Col A B P.
intros.
assert(HH:= ex_col2 A B).
ex_and HH C.
assert(HH:=l8_21 A B C H).

ex_and HH P.
ex_and H3 T.
apply perp_not_col in H3.
∃ P.
assumption.
Qed.

Lemma perp_exists : ∀ O A B, A ≠ B → ∃ X, Perp O X A B.
Proof.
intros.
assert(HH:=not_col_exists A B H).
ex_and HH Q.
induction(Col_dec O A B).
assert(∃ P, Perp A B P O ∧ one_side A B Q P).

apply(l10_15 A B O Q ).
Col.
auto.
ex_and H2 P.
∃ P.
apply perp_sym.
apply perp_right_comm.
auto.
assert(∃ P : Tpoint, Col A B P ∧ Perp A B O P).
apply (l8_18_existence A B O).
intro.
apply H1.
Col.
ex_and H2 P.
∃ P.
apply perp_sym.
auto.
Qed.

End T10.