Library GeoCoq.Tarski_dev.Ch13_1


Require Export GeoCoq.Tarski_dev.Ch12_parallel.

Section L13_1.

Context `{T2D:Tarski_2D}.

Pappus Desargues

Lemma per2_col_eq : A P P' B, A P A P' Per A P B Per A P' B Col P A P' P = P'.
Proof.
intros.
induction(eq_dec_points P B).
subst B.
assert( A = P' P = P').
apply(l8_9 A P' P H2); Col.
induction H4.
contradiction.
assumption.
induction(eq_dec_points P' B).
subst B.
assert(A = P P' = P).
apply(l8_9 A P P' H1); Col.
induction H5; auto.
contradiction.

apply per_perp_in in H1; auto.
apply per_perp_in in H2; auto.

apply perp_in_comm in H1.
apply perp_in_comm in H2.
apply perp_in_perp_bis in H1.
apply perp_in_perp_bis in H2.
induction H1; induction H2.
apply(l8_18_uniqueness P A B P P'); Col.
apply perp_not_col; auto.
apply perp_left_comm.
apply(perp_col A P' B P' P); Perp.
Col.
apply perp_distinct in H2.
tauto.
apply perp_distinct in H1.
tauto.
apply perp_distinct in H1.
tauto.
Qed.

Lemma per_distinct : A B C, Per A B C A B A C.
Proof.
intros.
intro.
subst C.
apply H0.
apply (l8_8).
assumption.
Qed.

Lemma per2_preserves_diff : O A B A' B', O A' O B' Col O A' B' Per O A' A Per O B' B A' B' A B.

Proof.
intros.
intro.
subst B.
apply H4.
apply(per2_col_eq O A' B' A);Col.
Qed.

Lemma per23_preserves_bet : A B C B' C', Bet A B C A B' A C' Col A B' C' Per A B' B Per A C' C Bet A B' C'.
Proof.
intros.
assert(HC:Col A B C).
apply bet_col in H; Col.

induction(eq_dec_points B B').
subst B'.

assert(Col A C' C).
ColR.

assert(A = C' C = C').
apply l8_9; auto.
induction H6.
contradiction.
subst C'.
assumption.

assert(A C).
intro.
subst C.
apply l8_8 in H4.
contradiction.

assert(C C').
intro.
subst C'.

assert(Col A B' B).
ColR.

assert(A = B' B = B').
apply l8_9; auto.
induction H8; contradiction.

assert(Perp A B' B' B).
apply per_perp_in in H3; auto.
apply perp_in_comm in H3.
apply perp_in_perp_bis in H3.
induction H3; Perp.
apply perp_distinct in H3.
tauto.

assert(Perp A C' C' C).
apply per_perp_in in H4; auto.
apply perp_in_comm in H4.
apply perp_in_perp_bis in H4.
induction H4; Perp.
apply perp_distinct in H4.
tauto.

assert(Par B B' C C').
apply(l12_9 B B' C C' A B');Perp.
apply perp_sym.
apply(perp_col _ C'); Perp.
ColR.

induction(eq_dec_points B C).
subst C.
assert(B' = C').
apply(per2_col_eq A B' C' B); Perp.
Col.
subst C'.
Between.

assert(¬Col A B' B).
apply per_not_col in H3; auto.

assert(¬Col A C' C).
apply per_not_col in H4; auto.

assert(B' C').
intro.
subst C'.
clean_trivial_hyps.

assert(Col B C B').
apply(per_per_col B C A B'); Perp.
apply H13; ColR.

induction H10.
apply l12_6 in H10.

assert(TS B B' A C).
repeat split;auto.
intro.
assert(A = B' B = B').
apply l8_9; Col.
induction H12; tauto.
intro.
apply H13; ColR.
B.
split; Col.

assert(TS B B' A C').
apply l9_2.
apply(l9_8_2 B B' C C' A); auto.
apply l9_2.
assumption.
unfold TS in H16.
spliter.
ex_and H18 T.
assert(T = B').
apply bet_col in H19.
apply (l6_21 B B' A B'); Col.
ColR.
subst T.
assumption.
spliter.
apply False_ind.
apply H12.
ColR.
Qed.

Lemma per23_preserves_bet_inv : A B C B' C', Bet A B' C' A B' Col A B C Per A B' B Per A C' C Bet A B C.
Proof.
intros.

induction(eq_dec_points B B').
subst B'.
assert(Col A C' C).
apply bet_col in H.
ColR.
assert(A = C' C = C').
apply(l8_9 A C' C); auto.
induction H5.
subst C'.
apply between_identity in H.
contradiction.
subst C'.
assumption.

assert(Perp A B' B' B).
apply per_perp_in in H2.
apply perp_in_comm in H2.
apply perp_in_perp_bis in H2.
induction H2.
Perp.
apply perp_distinct in H2.
tauto.
auto.
auto.

assert(Perp A C' C' C).
apply per_perp_in in H3.
apply perp_in_comm in H3.
apply perp_in_perp_bis in H3.
induction H3.
Perp.
apply perp_distinct in H3.
tauto.
intro.
subst C'.
apply between_identity in H.
contradiction.
intro.
subst C'.
induction(eq_dec_points A C).
subst C.
apply between_identity in H.
contradiction.
assert(Col A B' B).
apply bet_col in H.
ColR.
assert(A = B' B = B').
apply(l8_9 A B' B); auto.
induction H8;contradiction.

assert(Perp A B' C' C).
apply bet_col in H.
apply(perp_col _ C'); Col.

assert( Par B' B C' C).
apply(l12_9 B' B C' C A B').
Perp.
Perp.

induction(eq_dec_points B C).
subst C.
Between.

induction H8.
assert(B' C').
intro.
subst C'.
apply H8.
B'.
split; Col.

assert(HH:=l12_6 B' B C' C H8).

assert(TS B' B A C').
repeat split; auto.
intro.
assert(A = B' B = B').
apply(l8_9 A B' B); auto.
induction H12;contradiction.
intro.
assert(Col A B' B).
assert_cols.
ColR.
assert(A = B' B = B').
apply(l8_9 A B' B); auto.
induction H13;contradiction.
B'.
split; Col.

assert(TS B' B C A).
apply(l9_8_2 B' B C' C A); auto.
apply l9_2.
assumption.
unfold TS in H12.
spliter.
ex_and H14 T.

assert(A C).
intro.
subst C.
apply between_identity in H15.
subst T.
contradiction.

assert (T = B).
assert_cols.
apply (l6_21 A C B' B); Col.
intro.
assert(Col A B' B).
ColR.
assert(A = B' B = B').
apply(l8_9 A B' B); auto.
induction H21;contradiction.
subst T.
Between.

spliter.
assert_cols.
assert(Col A B' B).
ColR.
assert(A = B' B = B').
apply(l8_9 A B' B); auto.
induction H15;contradiction.
Qed.

Lemma per13_preserves_bet : A B C A' C', Bet A B C B A' B C' Col A' B C' Per B A' A Per B C' C Bet A' B C'.
Proof.
intros.
assert(Col A B C).
apply bet_col in H.
Col.

induction(eq_dec_points A A').
subst A'.
assert(Col B C' C).
ColR.

assert(B = C' C = C').
apply l8_9; auto.
induction H7.
contradiction.
subst C'.
assumption.

assert(C C').
intro.
subst C'.
assert(Col A A' B).
ColR.
assert(B = A' A = A').
apply l8_9; Col.
induction H8; tauto.

assert(Perp B A' A' A).
apply per_perp_in in H3; auto.
apply perp_in_comm in H3.
apply perp_in_perp_bis in H3.
induction H3.
Perp.
apply perp_distinct in H3.
tauto.

assert(Perp B C' C' C).
apply per_perp_in in H4; auto.
apply perp_in_comm in H4.
apply perp_in_perp_bis in H4.
induction H4.
Perp.
apply perp_distinct in H4.
tauto.

assert(Par A A' C C').
apply(l12_9 A A' C C' B A');Perp.
apply perp_sym.
apply(perp_col _ C'); Perp.
ColR.

induction H10.
assert(HH:=par_strict_symmetry A A' C C' H10).
apply l12_6 in H10.
apply l12_6 in HH.

assert(¬Col A A' B).
apply per_not_col in H3; auto.
intro.
apply H3.
Col.

assert(¬Col C C' B).
apply per_not_col in H4; auto.
intro.
apply H4.
Col.

assert(OS A A' B C).
apply out_one_side.
left; auto.
repeat split.
intro.
subst A.
unfold OS in H10.
ex_and H10 X.
unfold TS in H13.
spliter.
apply H13.
Col.
intro.
subst C.
unfold OS in H10.
ex_and H10 X.
unfold TS in H10.
spliter.
apply H10.
Col.
left.
assumption.

assert(OS C C' B A).
apply out_one_side.
left; auto.
repeat split.
intro.
subst C.
apply H12.
Col.
intro.
subst C.
unfold OS in H10.
ex_and H10 X.
unfold TS in H10.
spliter.
apply H10.
Col.
left.
Between.

assert(OS A A' B C').
apply(one_side_transitivity _ _ _ C); auto.
assert(OS C C' B A').
apply(one_side_transitivity _ _ _ A); auto.

apply invert_one_side in H15.
apply invert_one_side in H16.
assert(HP:= col_one_side_out A' A B C' H2 H15).
assert(Out C' B A').
apply(col_one_side_out C' C B A'); Col.

unfold Out in ×.
spliter.

induction H19.
Between.
induction H22.
Between.
apply False_ind.
apply H18.
apply (between_equality _ _ B); Between.
spliter.

induction(eq_dec_points A C).
subst C.
apply between_identity in H.
subst B.
clean_duplicated_hyps.
clean_trivial_hyps.
apply l8_8 in H4.
contradiction.
assert(Col B C' C).
ColR.
apply per_not_col in H4; auto.
contradiction.
Qed.

Lemma per13_preserves_bet_inv : A B C A' C', Bet A' B C' B A' B C' Col A B C Per B A' A Per B C' C Bet A B C.
Proof.
intros.
assert(Col A' B C').
apply bet_col in H.
Col.

induction(eq_dec_points A A').
subst A'.
assert(Col B C' C).
ColR.
assert(HH:=l8_9 B C' C H4 H6 ).
induction HH.
contradiction.
subst C'.
assumption.

assert(C C').
intro.
subst C'.
assert(Col B A' A).
ColR.
assert(HH:=l8_9 B A' A H3 H7).
induction HH;
contradiction.

assert(Perp B A' A' A).
apply per_perp_in in H3; auto.
apply perp_in_comm in H3.
apply perp_in_perp_bis in H3.
induction H3.
Perp.
apply perp_distinct in H3.
tauto.

assert(Perp B C' C' C).
apply per_perp_in in H4; auto.
apply perp_in_comm in H4.
apply perp_in_perp_bis in H4.
induction H4.
Perp.
apply perp_distinct in H4.
tauto.

assert(Par A A' C C').
apply(l12_9 A A' C C' B A');Perp.
apply perp_sym.
apply(perp_col _ C'); Perp.
ColR.

induction H10.
assert(HH:=par_strict_symmetry A A' C C' H10).
apply l12_6 in H10.
apply l12_6 in HH.

assert(¬Col A' A B).
apply per_not_col in H3; auto.
intro.
apply H3.
Col.

assert(¬Col C' C B).
apply per_not_col in H4; auto.
intro.
apply H4.
Col.

assert(OS A' A B C').
apply out_one_side.
left; auto.
repeat split.
intro.
subst A'.
apply H11.
Col.
intro.
subst C'.
apply one_side_symmetry in H10.
unfold OS in H10.
ex_and H10 X.
unfold TS in H10.
spliter.
apply H10.
Col.
left.
assumption.

assert(OS C' C B A').
apply out_one_side.
left; auto.
repeat split.
intro.
subst C'.
apply H12.
Col.
intro.
subst C'.
apply one_side_symmetry in H10.
unfold OS in H10.
ex_and H10 X.
unfold TS in H10.
spliter.
apply H10.
Col.
left.
Between.

assert(OS A' A B C).
apply(one_side_transitivity _ _ _ C'); auto.
apply invert_one_side.
apply one_side_symmetry.
assumption.

assert(OS C C' B A).
apply(one_side_transitivity _ _ _ A'); auto.
apply invert_one_side.
assumption.
apply one_side_symmetry.
assumption.

apply invert_one_side in H15.

assert(HP:= col_one_side_out A A' B C H2 H15).

assert(Out C B A).
apply(col_one_side_out C C' B A); Col.

unfold Out in ×.
spliter.

induction H19.
Between.
induction H22.
Between.
apply False_ind.
apply H18.
apply (between_equality _ _ B); Between.


spliter.
assert(Perp A' C' A A').
apply (perp_col _ B); Perp.
intro.
subst C'.
apply between_identity in H.
subst A'.
apply perp_distinct in H9.
tauto.
apply perp_not_col in H14.

apply False_ind.
apply H14.
ColR.
Qed.

Lemma per3_preserves_bet1 : O A B C A' B' C', Col O A B Bet A B C O A' O B' O C'
                                                     Per O A' A Per O B' B Per O C' C
                                                     Col A' B' C' Col O A' B' Bet A' B' C'.

Proof.
intros O A B C A' B' C'.
intro HC.
intros.

induction(eq_dec_points A B).
subst B.
assert(A' = B').
apply(per2_col_eq O A' B' A H0 H1 H3 H4); Col.
subst B'.
Between.

induction (eq_dec_points A A').
subst A'.
induction(eq_dec_points B B').
subst B'.
assert(Col O C C').
apply bet_col in H.
ColR.

assert(C = C').
apply bet_col in H.
assert(O = C' C = C').
apply(l8_9 O C' C H5); Col.
induction H10.
contradiction.
assumption.
subst C'.
assumption.

induction(eq_dec_points A B').
subst B'.
Between.

assert(A C).
intro.
subst C.
apply between_identity in H.
contradiction.

assert( ¬ Col O B' B).
apply(per_not_col O B' B H1); auto.

assert(C C').
intro.
subst C'.
clean_trivial_hyps.
apply H12.
apply bet_col in H.
ColR.

assert(Perp B B' O A).

apply per_perp_in in H4; auto.
apply perp_in_perp_bis in H4.
induction H4.
apply perp_distinct in H4.
tauto.
apply perp_sym.
apply perp_right_comm.
apply(perp_col O B' B' B A); auto.
Col.

assert(Perp C C' O A).

apply per_perp_in in H5; auto.
apply perp_in_perp_bis in H5.
induction H5.
apply perp_distinct in H5.
tauto.
apply perp_sym.
apply perp_right_comm.
apply(perp_col O C' C' C A); auto.
apply bet_col in H.
ColR.

assert(Par B B' C C').
apply(l12_9 B B' C C' O A);auto.
induction H16.

assert(HH:=l12_6 B B' C C' H16).

assert(TS B B' A C).
unfold TS.
repeat split; Col.
assert(¬Col B' A B).
apply(perp_not_col).
apply perp_left_comm.
apply(perp_col A O B B' B'); Col.
finish.
intro.
apply H17.
Col.
intro.
apply H16.
C.
split; Col.
B.
split; Col.
assert(TS B B' C' A).
apply(l9_8_2 B B' C C' A).

apply l9_2.
assumption.
assumption.
unfold TS in H18.
spliter.
ex_and H20 T.
assert(B'=T).
apply (l6_21 B B' A C'); Col.
intro.
subst C'.
apply between_identity in H21.
subst T.
contradiction.
subst T.
apply between_symmetry.
assumption.
spliter.

assert(Per O C' B).
apply(per_col O C' C B); Col.
assert(B'=C').
apply(per2_col_eq O B' C' B); Col.
ColR.
subst C'.
Between.


induction(eq_dec_points A' B').
subst B'.
Between.

induction(eq_dec_points B C).
subst C.
assert(B' = C').
apply(per2_col_eq O B' C' B); auto.
ColR.
subst C'.
Between.

induction(eq_dec_points B B').
subst B'.
induction(eq_dec_points A' B).
subst B.
Between.

assert(C C').
intro.
subst C'.

assert( ¬ Col O A' A).
apply(per_not_col O A' A ); auto.
apply H13.
apply bet_col in H.
ColR.

assert(Perp A A' O A').
apply per_perp_in in H3; auto.
apply perp_in_comm in H3.
apply perp_in_perp_bis in H3.
induction H3.
finish.
apply perp_distinct in H3.
tauto.

assert(Perp C C' O A').
apply per_perp_in in H5; auto.
apply perp_in_comm in H5.
apply perp_in_perp_bis in H5.
induction H5.
apply perp_sym.
apply (perp_col _ C'); auto.
finish.
ColR.
apply perp_distinct in H5.
tauto.

assert(Par A A' C C').
apply(l12_9 A A' C C' O A');auto.
induction H16.

assert(HH:=l12_6 A A' C C' H16).

assert(OS C C' A A').
apply(l12_6 C C' A A').
finish.
assert(OS C C' A B).
apply(out_one_side C C' A B).
left.
intro.
apply H16.
A.
split; Col.
unfold Out.
repeat split; auto.
intro.
subst C.
apply between_identity in H.
contradiction.
right.
Between.

assert(OS C C' A' B).
apply(one_side_transitivity C C' A' A); auto.
apply one_side_symmetry.
assumption.

assert(Out C' B A').
induction H6.
unfold Out.
repeat split.
intro.
subst C'.
clean_trivial_hyps.
unfold OS in H17.
ex_and H17 T.
unfold TS in H4.
spliter.
apply H4.
Col.
intro.
subst C'.
apply H16.
A'.
split; Col.
left.
Between.

induction H6.

assert(TS C C' B A').
unfold TS.
repeat split.
intro.
unfold OS in H18.
ex_and H18 T.
unfold TS in H21.
spliter.
contradiction.
intro.
apply H16.
A'.
split; Col.
C'.
split; Col.
apply one_side_symmetry in H19.
apply l9_9_bis in H19.
contradiction.

unfold Out.
repeat split.
intro.
subst C'.
apply H16.
A.
apply bet_col in H.
split; Col.
intro.
subst C'.
apply H16.
A'.
split; Col.
right; auto.


assert(Out A' B C').
induction H6.
unfold Out.
repeat split.
intro.
subst A'.
clean_trivial_hyps.
apply H16.
C.
apply bet_col in H.
split; Col.
intro.
subst C'.
unfold Out in H20.
tauto.
left.
auto.

induction H6.
unfold Out in H20.
spliter.
unfold Out.
repeat split.
intro.
subst A'.
apply H16.
C.
apply bet_col in H.
split; Col.
auto.
induction H22.
left.
Between.

apply False_ind.
apply H21.
apply (between_equality _ _ B); Between.


assert(OS A A' B C).
apply(out_one_side A A' B C).
right.
intro.
apply H16.
C.
split; Col.
unfold Out.
repeat split; auto.
intro.
subst C.
apply between_identity in H.
contradiction.

assert(OS A A' C' B).
apply(one_side_transitivity A A' C' C);
apply one_side_symmetry; auto.

assert(TS A A' B C').
unfold TS.
repeat split.
intro.
unfold OS in H21.
ex_and H21 T.
unfold TS in H21.
spliter.
contradiction.
intro.
apply H16.
C'.
split; Col.
A'.
split; Col.
Between.
apply one_side_symmetry in H22.
apply l9_9_bis in H22.
contradiction.

unfold Out in ×.
spliter.
clean_duplicated_hyps.

induction H25; induction H23.
assumption.
apply False_ind.
apply H20.
apply(between_equality _ _ A'); Between.
apply False_ind.
apply H10.
apply(between_equality _ _ C'); Between.
apply False_ind.
apply H24.
apply(between_equality _ _ B); Between.
spliter.

assert(¬Col O C' C).
apply(per_not_col); auto.
apply False_ind.
apply H20.

assert(AC).
intro.
subst C.
apply between_identity in H.
subst B.
tauto.
apply bet_col in H.
ColR.


assert(Perp A A' O A').
apply per_perp_in in H3; auto.
apply perp_in_comm in H3.
apply perp_in_perp_bis in H3.
induction H3.
finish.
apply perp_distinct in H3.
tauto.

assert(Perp B B' O A').
apply per_perp_in in H4; auto.
apply perp_in_comm in H4.
apply perp_in_perp_bis in H4.
induction H4.
apply perp_sym.
apply (perp_col _ B'); Col.
finish.
apply perp_distinct in H4.
tauto.

assert(Par A A' B B').
apply(l12_9 A A' B B' O A');auto.

induction H15.
assert(HH:=l12_6 A A' B B' H15).

assert(TS B B' A C).
unfold TS.
repeat split; Col.
intro.
apply H15.
A.
split; Col.
intro.
apply H11.
apply (l6_21 B B' A C); Col.
intro.
apply H15.
A.
split; Col.
intro.
subst C.
apply between_identity in H.
subst B.
tauto.
B.
split; Col.

assert(OS B B' A A').
apply(l12_6 B B' A A').
finish.

assert(HP:= l9_8_2 B B' A A' C H16 H17).

induction(eq_dec_points C C').
subst C'.
unfold TS in HP.
spliter.
ex_and H20 T.

assert(T = B').
apply (l6_21 B B' A' C); Col.
intro.
subst A'.
apply between_identity in H21.
subst T.
contradiction.
subst T.
assumption.

assert(Perp C C' O A').
apply per_perp_in in H5; auto.
apply perp_in_comm in H5.
apply perp_in_perp_bis in H5.
induction H5.
apply perp_sym.
apply (perp_col _ C'); finish.
ColR.
apply perp_distinct in H5.
tauto.

assert(Par B B' C C').
apply(l12_9 B B' C C' O A');auto.
induction H20.

assert(HQ:=l12_6 B B' C C' H20).

assert(TS B B' C' A').
apply(l9_8_2 B B' C C' A'); auto.
apply l9_2.
assumption.
unfold TS in H21.
spliter.
ex_and H23 T.
assert(T = B').
apply (l6_21 B B' A' C'); Col.
intro.
subst C'.
apply between_identity in H24.
subst T.
contradiction.
subst T.
Between.
spliter.
unfold TS in HP.
spliter.
apply False_ind.
apply H25.
ColR.
spliter.

apply perp_left_comm in H13.
apply perp_not_col in H13.
apply False_ind.
apply H13.
ColR.
Qed.

Lemma per3_preserves_bet2_aux : O A B C B' C', Col O A C A C'
                               Bet A B' C' O A O B' O C'
                                Per O B' B Per O C' C
                                Col A B C Col O A C' Bet A B C.
Proof.
intros O A B C B' C'.
intro HX.
intros.
induction(eq_dec_points A B).
subst B.
Between.
induction(eq_dec_points B C).
subst C.
Between.

assert(Col O A B').
apply bet_col in H0.
ColR.
assert(Col O B' C').
apply bet_col in H0.
ColR.

induction(eq_dec_points B B').
subst B'.
assert(Col O C C').
apply bet_col in H0.
ColR.
assert(C = C').
apply(per_col_eq C C' O); finish.
subst C'.
assumption.
assert(C C').
intro.
subst C'.
apply per_not_col in H4; auto.
apply H4.
ColR.

assert(Perp O A C C').
apply per_perp_in in H5; auto.
apply perp_in_comm in H5.
apply perp_in_perp_bis in H5.
induction H5.
apply (perp_col _ C'); finish.
apply perp_distinct in H5.
tauto.

assert(Perp O A B B').
apply per_perp_in in H4; auto.
apply perp_in_comm in H4.
apply perp_in_perp_bis in H4.
induction H4.
apply (perp_col _ B'); finish.
apply perp_distinct in H4.
tauto.

assert(Par B B' C C').
apply(l12_9 B B' C C' O A);finish.

induction H16.
assert(HH:=l12_6 B B' C C' H16).
assert(TS B B' A C').
repeat split; finish.
intro.
assert(Per B B' A).
apply(per_col B B' O A); finish.
apply per_not_col in H18; auto.
apply H18.
Col.
intro.
subst B'.
clean_trivial_hyps.
apply H16.
C.
split; Col.
intro.
apply H16.
C'.
split; Col.
B'.
split; finish.

assert(TS B B' C A).
apply(l9_8_2 B B' C' C A).
apply l9_2; auto.
apply one_side_symmetry; auto.
unfold TS in H18.
spliter.
ex_and H20 T.
assert(B = T).
apply (l6_21 A C B' B); Col.
assert(A C).
intro.
subst C.
apply between_identity in H21.
subst T.
contradiction.
intro.
apply bet_col in H0.
apply H19.
ColR.
subst T.
Between.

spliter.

assert(B' C').
intro.
subst C'.
clean_trivial_hyps.
assert(Perp O B' C B').
apply(perp_col O A C B' B'); Col.
apply perp_left_comm in H0.
apply perp_not_col in H0.
apply H0.
ColR.

assert(Per C C' B').
apply(per_col C C' O B'); finish.
apply per_not_col in H21; auto.
apply False_ind.
apply H21.
Col.
Qed.

Lemma per3_preserves_bet2 : O A B C A' B' C', Col O A C A' C'
                               Bet A' B' C' O A' O B' O C'
                                Per O A' A Per O B' B Per O C' C
                                Col A B C Col O A' C' Bet A B C.

Proof.
intros O A B C A' B' C'.
intro HX.
intros.
induction(eq_dec_points A A').
subst A'.
apply (per3_preserves_bet2_aux O A B C B' C');auto.
induction(eq_dec_points C C').
subst C'.
apply between_symmetry.
apply(per3_preserves_bet2_aux O C B A B' A'); finish.

assert(Perp O A' C C').
apply per_perp_in in H6; auto.
apply perp_in_comm in H6.
apply perp_in_perp_bis in H6.
induction H6.
apply (perp_col _ C'); finish.
apply perp_distinct in H6.
tauto.

assert(Perp O A' A A').
apply per_perp_in in H4; auto.
apply perp_in_comm in H4.
apply perp_in_perp_bis in H4.
induction H4.
finish.
apply perp_distinct in H4.
tauto.

assert(Par A A' C C').
apply(l12_9 A A' C C' O A');finish.

induction H13.
assert(HH:=l12_6 A A' C C' H13).
apply par_strict_symmetry in H13.
assert(HP:=l12_6 C C' A A' H13).

induction(eq_dec_points B B').
subst B'.

assert(OS A' A B C').
apply out_one_side.
right.
intro.
apply H13.
C'.
split; Col.
repeat split.
intro.
subst A'.
apply H13.
C.
split; Col.
auto.
left; auto.
apply invert_one_side in H14.
assert(OS A A' B C).
apply (one_side_transitivity _ _ _ C').
assumption.
apply one_side_symmetry.
assumption.

assert(Out A B C).
apply (col_one_side_out A A');auto.

assert(OS C' C B A').
apply out_one_side.
right.
intro.
apply H13.
A'.
split; Col.
repeat split.
intro.
subst C'.
apply H13.
A.
split; Col.
auto.
left; Between.
apply invert_one_side in H17.
assert(OS C C' B A).
apply (one_side_transitivity _ _ _ A').
assumption.
apply one_side_symmetry.
assumption.
apply one_side_symmetry in H18.

assert(Out C A B).
apply (col_one_side_out C C');Col.
unfold Out in ×.
spliter.

induction H23; induction H21.
assumption.
assumption.
assert(A = C).
apply (between_equality A C B); auto.
subst C.
apply False_ind.
apply H13.
A.
split; Col.
assert(B = C).
apply (between_equality B C A); Between.
subst C.
Between.


assert(Perp O A' B B').
apply per_perp_in in H5; auto.
apply perp_in_comm in H5.
apply perp_in_perp_bis in H5.
induction H5.
apply (perp_col _ B'); finish.
apply bet_col in H0.
ColR.
apply perp_distinct in H5.
tauto.

assert(Par B B' A A').
apply(l12_9 B B' A A' O A');finish.

induction H16.
assert(HQ:=l12_6 B B' A A' H16).

assert(Par B B' C C').
apply(l12_9 B B' C C' O A');finish.
induction H17.
assert(HR:=l12_6 B B' C C' H17).

assert(TS B B' A' C').
repeat split; auto.
intro.
apply H16.
A'.
split; Col.
intro.
apply H17.
C'.
split; Col.
B'.
split; finish.
apply one_side_symmetry in HQ.
assert(HH1:= l9_8_2 B B' A' A C' H18 HQ).
apply l9_2 in HH1.
apply one_side_symmetry in HR.
assert(HH2:= l9_8_2 B B' C' C A HH1 HR).
unfold TS in HH2.
spliter.
ex_and H21 T.
assert(B = T).
apply (l6_21 B B' A C); Col.
intro.
subst C.
apply H13.
A.
split; Col.
subst T.
Between.
spliter.

induction(eq_dec_points B C).
subst C.
Between.
assert(Col A C C').
ColR.
apply False_ind.
apply H13.
A.
split; Col.
spliter.

induction(eq_dec_points A B).
subst B.
Between.
assert(Col C A A').
ColR.
apply False_ind.
apply H13.
C.
split; Col.
spliter.

assert(A C).
intro.
subst C.
apply H.
apply(per2_col_eq O A' C' A); Col.

assert(Col O C C').
ColR.
apply False_ind.
apply per_not_col in H6; auto.
apply H6.
Col.
Qed.

Lemma symmetry_preserves_per : A P B A' P', Per B P A Midpoint B A A' Midpoint B P P'
                                                    Per B P' A'.
Proof.
intros.
assert(HS:=symmetric_point_construction A P).
ex_and HS C.
assert(HS:=symmetric_point_construction C B).
ex_and HS C'.

assert(HH:= symmetry_preserves_midpoint A P C A' P' C' B H0 H1 H3 H2).
unfold Per.
C'.
split.
assumption.
unfold Per in H.
ex_and H X.
assert(X = C).
apply(symmetric_point_uniqueness A P X C); auto.
subst X.
unfold Midpoint in ×.
spliter.
apply (cong_transitivity _ _ B A).
Cong.
apply(cong_transitivity _ _ B C).
assumption.
Cong.
Qed.

Lemma l13_1 : A B C P Q R,
   ¬ Col A B C Midpoint P B C Midpoint Q A C Midpoint R A B
    X, Y, Perp_at R X Y A B Perp X Y P Q.
Proof.
intros A B C P Q R HC MBC MAC MAB.
assert(Q C).
intro.
subst Q.
unfold Midpoint in MAC.
spliter.
apply cong_identity in H0.
subst C.
apply HC.
Col.
assert(P C).
intro.
subst P.
unfold Midpoint in MBC.
spliter.
apply cong_identity in H1.
subst C.
apply HC.
Col.

assert(D1:QR).
intro.
subst R.
assert(B=C).
apply(symmetric_point_uniqueness A Q); auto.
subst C.
apply l7_3 in MBC.
contradiction.

assert(D2:R B).
intro.
subst R.
unfold Midpoint in MAB.
spliter.
apply cong_identity in H2.
subst B.
apply HC.
Col.

assert(¬Col P Q C).
intro.
apply HC.
unfold Midpoint in ×.
spliter.
apply bet_col in H2.
apply bet_col in H4.
apply bet_col in H6.
ColR.

assert(HH:= l8_18_existence P Q C H1).
ex_and HH C'.

assert(HS1:=symmetric_point_construction C' Q).
ex_and HS1 A'.
assert(HS1:=symmetric_point_construction C' P).
ex_and HS1 B'.

assert(Cong C C' B B').
apply(l7_13 P C C' B B' MBC); finish.
assert(Cong C C' A A').
apply(l7_13 Q C C' A A'); finish.

assert(Per P B' B).
induction(eq_dec_points P C').
subst C'.
unfold Midpoint in H5.
spliter.
apply cong_symmetry in H8.
apply cong_identity in H8.
subst B'.
apply l8_2.
apply l8_5.

apply(symmetry_preserves_per C C' P B B'); finish.
apply perp_in_per.
apply perp_in_comm.
apply perp_perp_in.
apply perp_left_comm.
apply (perp_col _ Q); Col.

assert(Per Q A' A).
induction(eq_dec_points Q C').
subst C'.
unfold Midpoint in H4.
spliter.
apply cong_symmetry in H9.
apply cong_identity in H9.
subst A'.
apply l8_2.
apply l8_5.
apply(symmetry_preserves_per C C' Q A A'); finish.
apply perp_in_per.
apply perp_in_comm.
apply perp_perp_in.
apply perp_left_comm.
apply (perp_col _ P); Col.
finish.

assert(Cl1: Col A' C' Q).
unfold Midpoint in H4.
spliter.
apply bet_col in H4.
Col.

assert(Cl2: Col B' C' P).
unfold Midpoint in H5.
spliter.
apply bet_col in H5.
Col.

assert(NE0: P Q).
apply perp_distinct in H3; tauto.

assert(NE1 : A' B').
intro.
subst B'.
apply NE0.
apply (l7_17 C' A'); auto.

assert(Cl3: Col A' B' P).
induction(eq_dec_points P C').
subst P.
unfold Midpoint in H5.
spliter.
apply cong_symmetry in H10.
apply cong_identity in H10.
subst C'.
Col.
induction(eq_dec_points Q C').
subst Q.
unfold Midpoint in H4.
spliter.
apply cong_symmetry in H11.
apply cong_identity in H11.
subst C'.
Col.
ColR.

assert(Cl4: Col A' B' Q).
induction(eq_dec_points P C').
subst P.
unfold Midpoint in H5.
spliter.
apply cong_symmetry in H10.
apply cong_identity in H10.
subst C'.
Col.
induction(eq_dec_points Q C').
subst Q.
unfold Midpoint in H4.
spliter.
apply cong_symmetry in H11.
apply cong_identity in H11.
subst C'.
Col.
ColR.

assert(Cl5:Col A' B' C').
ColR.

assert(NE2 : C C').
apply perp_distinct in H3.
tauto.

assert(NE3: A A').
intro.
subst A'.
apply cong_identity in H7.
contradiction.

assert(NE4: B B').
intro.
subst B'.
apply cong_identity in H6.
contradiction.

assert(Per P A' A).
induction(eq_dec_points A' Q).
subst Q.
unfold Midpoint in H4.
spliter.
apply cong_identity in H10.
subst C'.
clean_trivial_hyps.
apply perp_left_comm in H3.
apply perp_perp_in in H3.
apply perp_in_comm in H3.
apply perp_in_per in H3.
unfold Midpoint in MAC.
spliter.
apply bet_col in H2.
apply (per_col P A' C A); Col.
apply l8_2.
apply (per_col A A' Q P); finish.
ColR.

assert(Per Q B' B).
induction(eq_dec_points B' P).
subst P.
unfold Midpoint in H5.
spliter.
apply cong_identity in H11.
subst C'.
clean_trivial_hyps.
apply perp_perp_in in H3.
apply perp_in_comm in H3.
apply perp_in_per in H3.
unfold Midpoint in MBC.
spliter.
apply bet_col in H2.
apply (per_col Q B' C B); Col.
apply l8_2.
apply (per_col B B' P Q); finish.
ColR.

assert(Per A' B' B).
apply l8_2.
induction(eq_dec_points B' P).
subst P.
unfold Midpoint in H5.
spliter.
apply cong_identity in H12.
subst C'.
clean_trivial_hyps.
apply(per_col B B' Q A'); finish.
apply(per_col B B' P A'); finish.

assert(Per B' A' A).
apply l8_2.
induction(eq_dec_points A' Q).
subst Q.
unfold Midpoint in H4.
spliter.
apply cong_identity in H13.
subst C'.
clean_trivial_hyps.
apply(per_col A A' P B'); finish.
apply(per_col A A' Q B'); finish.

assert(NC1 : ¬Col A' B' A).
apply per_not_col in H13; auto.
intro.
apply H13.
Col.

assert(NC2 : ¬Col A' B' B).
apply per_not_col in H12; auto.


assert(HM:=midpoint_existence A' B').
ex_and HM X.

assert(HP:=perp_exists X A' B' NE1).
ex_and HP y.

assert(HH:=ex_sym X y A).
ex_and HH B''.

assert( X y).
apply perp_distinct in H15.
tauto.

assert(Reflect B'' A X y).
unfold Reflect.
left.
repeat split;auto.
ex_and H17 M.
M.
split; finish.

assert(Reflect A' B' X y).
unfold Reflect.
left.
split; auto.
repeat split.
X.
split; finish.
left.
finish.
apply l10_4 in H19.

assert(HH:= l10_10 X y B'' B' A A' H19 H20).

assert(Per A' B' B'').
unfold Reflect in ×.
induction H19; induction H20.
spliter.

apply(image_preserves_per B' A' A A' B' B'' X y); auto.
apply l10_4_spec.
assumption.
spliter.
contradiction.
spliter.
contradiction.
spliter.
contradiction.

unfold Reflect in H20.
induction H20.
spliter.
unfold ReflectL in H22.

assert(OS A' B' A B'').
induction H16.
assert(Par A' B' A B'').
apply(l12_9 A' B' A B'' X y); finish.

induction H23.
apply( l12_6 A' B' A B'' H23).
spliter.

apply per_not_col in H21; auto.
apply False_ind.
apply H21.
ColR.
intro.
subst B''.
apply cong_symmetry in HH.
apply cong_identity in HH.
subst A'.
apply cong_identity in H7.
subst C'.
tauto.
subst B''.
apply one_side_reflexivity.
intro.
apply NC1.
Col.

assert(OS A' B' A B).
unfold OS.
C.
split.
unfold TS.
repeat split; Col.
intro.
apply H1.
ColR.
Q.
split; Col.
unfold Midpoint in MAC.
tauto.
unfold TS.
repeat split; Col.
intro.
apply H1.
ColR.
P.
split; Col.
unfold Midpoint in MBC.
tauto.


assert( Col B B'' B').
apply(per_per_col B B'' A' B'); finish.

assert(Cong B B' A A').
apply cong_transitivity with C C'; Cong.

assert(B = B'' Midpoint B' B B'').
apply( l7_20); Col.

apply cong_transitivity with A A'; Cong.
induction H27.
subst B''.

R.
X.

ex_and H17 M.
assert(R = M).
apply (l7_17 A B); auto.
subst M.

assert(A B).
intro.
subst B.
apply HC; Col.

assert(Col R A B).
unfold Midpoint in MAB.
spliter.
apply bet_col in H30.
Col.

assert(X R).
intro.
subst X.
assert(Par A B A' B').
apply(l12_9 A B A' B' R y);finish.
induction H16.
Perp.
contradiction.
induction H31.
apply H31.
R.

unfold Midpoint in H14.
spliter.
apply bet_col in H14.
split; Col.
spliter.
apply NC1.
Col.

split.

apply(l8_14_2_1b_bis R X A B R); Col.
induction H16.
apply perp_left_comm.
apply(perp_col _ y); auto.
contradiction.

apply perp_left_comm.
apply(perp_col _ y);auto.
apply perp_sym.
induction(eq_dec_points B' P).
subst P.
apply(perp_col _ A');auto.
Perp.
Col.
apply(perp_col _ B');auto.
apply perp_left_comm.

apply(perp_col _ A');auto.
Perp.
Col.
ColR.

assert(TS A' B' B B'').
unfold TS.
repeat split; auto.
intro.
apply NC2; Col.
intro.
apply per_not_col in H21; auto.
apply H21.
Col.
intro.
subst B''.
unfold Midpoint in H27.
spliter.
apply cong_identity in H29.
subst B'.
unfold OS in H23.
ex_and H23 T.
unfold TS in H29.
spliter.
apply H29.
Col.
B'.
split; Col.
unfold Midpoint in H27.
tauto.
assert(OS A' B' B B'').
apply (one_side_transitivity A' B' B A ).
apply one_side_symmetry.
assumption.
assumption.
apply l9_9 in H28.
contradiction.
spliter.
contradiction.
Qed.

Lemma per_lt : A B C, A B C B Per A B C Lt A B A C Lt C B A C.
  Proof.
    intros.
    assert(Lt B A A C Lt B C A C).
      apply( l11_46 A B C).
        apply per_not_col; auto.
      left.
      assumption.
    spliter.
    split; apply lt_left_comm; assumption.
  Qed.

Lemma cong_perp_conga : A B C P, Cong A B C B Perp A C B P CongA A B P C B P TS B P A C.
Proof.
    intros.
    assert(A C B P).
      split.
        apply perp_not_eq_1 in H0.
        assumption.
      apply perp_not_eq_2 in H0.
      assumption.
    spliter.
    assert(A B).
      intro.
      subst B.
      apply cong_symmetry in H.
      apply cong_identity in H.
      apply H1.
      auto.
    assert(C B).
      intro.
      subst B.
      apply cong_identity in H.
      contradiction.
    induction(Col_dec A B C).
      assert(¬ Col B A P).
        apply perp_not_col.
        apply perp_comm.
        apply (perp_col _ C); Col.
      assert(Per P B A).
        apply perp_in_per.
        apply perp_in_comm.
        apply perp_perp_in.
        apply perp_sym.
        eapply (perp_col _ C); Col.
      assert(Per P B C).
        apply perp_in_per.
        apply perp_in_comm.
        apply perp_perp_in.
        apply perp_sym.
        eapply (perp_col _ A); Col.
        Perp.
      apply l8_2 in H7.
      apply l8_2 in H8.
      split.
        apply l11_16; auto.
      assert( A = C Midpoint B A C).
        eapply l7_20; Cong.
      induction H9.
        contradiction.
      unfold TS.
      repeat split.
        auto.
        intro.
        apply H6.
        Col.
        intro.
        apply H6.
        ColR.
       B.
      unfold Midpoint in H9.
      spliter.
      split; Between.
    assert(HH:= H0).
    unfold Perp in HH.
    ex_and HH T.
    apply perp_in_col in H6.
    spliter.
    assert(B T).
      intro.
      subst T.
      apply H5.
      Col.
    assert(Perp B T A C).
      apply (perp_col _ P); Perp.
    assert(A T).
      intro.
      subst T.
      apply perp_comm in H9.
      apply perp_perp_in in H9.
      apply perp_in_comm in H9.
      apply perp_in_per in H9.
      assert(Lt B A B C Lt C A B C).
        apply( per_lt B A C); auto.
      spliter.
      unfold Lt in H10.
      spliter.
      apply H12.
      Cong.
    assert(C T).
      intro.
      subst T.
      apply perp_left_comm in H9.
      apply perp_perp_in in H9.
      apply perp_in_comm in H9.
      apply perp_in_per in H9.
      assert(Lt B C B A Lt A C B A).
        apply( per_lt B C A); auto.
      spliter.
      unfold Lt in H11.
      spliter.
      apply H13.
      Cong.
    assert(Perp_at T B T T A).
      apply perp_in_comm.
      apply perp_perp_in.
      apply perp_sym.
      apply (perp_col _ C).
        assumption.
        apply perp_sym.
        apply perp_left_comm.
        apply (perp_col _ P); Perp.
      Col.
    assert(Perp_at T B T T C).
      apply perp_in_comm.
      apply perp_perp_in.
      apply perp_sym.
      apply (perp_col _ A).
        assumption.
        apply perp_sym.
        apply perp_left_comm.
        apply (perp_col _ P); Perp.
      Col.
    assert(Cong T A T C CongA T A B T C B CongA T B A T B C).
      apply( l11_52 A T B C T B); Cong.
        eapply l11_16; auto.
          apply perp_in_per.
          apply perp_in_comm.
          apply perp_in_sym.
          assumption.
        apply perp_in_per.
        apply perp_in_comm.
        apply perp_in_sym.
        assumption.
      assert(Lt B T B A Lt A T B A).
        apply( per_lt B T A); auto.
        apply perp_in_per.
        assumption.
      spliter.
      apply le_comm.
      unfold Lt in H14.
      spliter.
      assumption.
    spliter.
    split.
      induction(bet_dec P B T).
        apply conga_comm.
        eapply l11_13; auto.
          apply H16.
          Between.
        Between.
      apply conga_comm.
      assert(Out B T P).
        unfold Out.
        repeat split; auto.
        induction H7.
          right.
          assumption.
        induction H7.
          left.
          Between.
        apply between_symmetry in H7.
        contradiction.
      eapply out_conga.
        apply H16.
        assumption.
        apply out_trivial.
        auto.
        assumption.
      apply out_trivial.
      auto.
    assert(A = C Midpoint T A C).
      apply l7_20; Col.
    induction H17.
      contradiction.
    unfold TS.
    repeat split; Col.
      assert(¬ Col T A B).
        apply perp_not_col.
        apply perp_in_perp_bis in H12.
        induction H12.
          apply perp_not_eq_1 in H12.
          tauto.
        Perp.
      intro.
      apply H18.
      ColR.
      assert(¬ Col T C B).
        apply perp_not_col.
        apply perp_in_perp_bis in H13.
        induction H13.
          apply perp_not_eq_1 in H13.
          tauto.
        Perp.
      intro.
      apply H18.
      ColR.
     T.
    apply midpoint_bet in H17.
    split; Col.
Qed.

Lemma perp_per_bet : A B C P, ¬Col A B C Col A P C Per A B C Perp_at P P B A C Bet A P C.
Proof.
intros.
assert( A C).
intro.
subst C.
apply H.
Col.
assert(Bet A P C A P C P).
apply(l11_47 A C B P); auto.
Perp.
tauto.
Qed.

Lemma ts_per_per_ts : A B C D, TS A B C D Per B C A Per B D A TS C D A B.
Proof.
intros.
assert(HTS:= H).
    unfold TS in H.
    assert (¬ Col C A B).
      spliter.
      assumption.
    spliter.
    clear H.
    assert (A B).
      intro.
      subst B.
      Col.
    ex_and H4 P.
    assert_diffs.
    show_distinct C D.
contradiction.

unfold TS.
repeat split; auto.
intro.
assert(A = P).
apply bet_col in H5.
apply (l6_21 A B C D); Col.
subst P.
apply H6.
apply(per2_col_eq A C D B); finish.
intro.
assert(B = P).
apply bet_col in H5.
apply (l6_21 A B C D); Col.
subst P.
apply H6.
apply(per2_col_eq B C D A); finish.
P.
split.
finish.

assert( X : Tpoint, Col A B X Perp A B C X).
apply(l8_18_existence A B C); Col.
ex_and H7 C'.

assert( X : Tpoint, Col A B X Perp A B D X).
apply(l8_18_existence A B D); Col.
ex_and H12 D'.

assert( A C').
intro.
subst C'.
apply perp_perp_in in H8.
apply perp_in_comm in H8.
apply perp_in_per in H8.
assert(A = C).
apply (l8_7 B); Perp.
subst C.
tauto.

assert( A D').
intro.
subst D'.
apply perp_perp_in in H14.
apply perp_in_comm in H14.
apply perp_in_per in H14.
assert(A = D).
apply (l8_7 B); Perp.
subst D.
tauto.

assert(Bet A C' B).
apply(perp_per_bet A C B C'); Col.
Perp.
assert(Perp A C' C' C).
apply(perp_col _ B); Col; Perp.
apply perp_in_sym.
apply perp_in_right_comm.
apply(l8_15_1 A B C C'); auto.

assert(Bet A D' B).
apply(perp_per_bet A D B D'); Col.
Perp.
assert(Perp A D' D' D).
apply(perp_col _ B); Col; Perp.
apply perp_in_sym.
apply perp_in_right_comm.
apply(l8_15_1 A B D D'); auto.

induction(eq_dec_points C' P).
subst C'.
assumption.

induction(eq_dec_points D' P).
subst D'.
assumption.

induction(eq_dec_points A P).
subst P.
Between.
induction(eq_dec_points B P).
subst P.
Between.

assert(Bet C' P D').
apply(per13_preserves_bet C P D C' D'); Col.
ColR.
assert(Perp P C' C' C).
apply(perp_col _ A);auto.
apply perp_left_comm.
apply(perp_col _ B);Perp.
Col.
ColR.
apply perp_comm in H24.
apply perp_perp_in in H24.
apply perp_in_comm in H24.
apply perp_in_per in H24.
assumption.

assert(Perp P D' D' D).
apply(perp_col _ A);auto.
apply perp_left_comm.
apply(perp_col _ B);Perp.
Col.
ColR.
apply perp_comm in H24.
apply perp_perp_in in H24.
apply perp_in_comm in H24.
apply perp_in_per in H24.
assumption.

assert(HH:= l5_3 A C' D' B H18 H19).
induction HH.
eBetween.
apply between_symmetry in H24.
eBetween.
Qed.

Lemma l13_2_1 : A B C D E, TS A B C D Per B C A Per B D A Col C D E
     Perp A E C D CongA C A B D A B
     CongA B A C D A E CongA B A D C A E Bet C E D.
Proof.
    intros.
    intros.
    assert(HH:= H).
    unfold TS in HH.
    assert (¬ Col C A B).
      spliter.
      assumption.
    spliter.
    assert(A C A B A D).
      unfold CongA in H4.
      spliter.
      repeat split; auto.
    spliter.
    assert(Cong B C B D Cong A C A D CongA C B A D B A).
      apply(l11_50_2 B A C B A D).
        intro.
        apply H6.
        Col.
        eapply l11_16; auto.
          apply l8_2.
          auto.
          intro.
          subst C.
          apply H6.
          Col.
          apply l8_2.
          auto.
        intro.
        subst D.
        apply H7.
        Col.
        apply conga_comm.
        auto.
      Cong.
    spliter.
    assert(Perp C D A B).
      apply( cong_conga_perp C A D B); Cong.
    assert(Col A B E).
      eapply perp_perp_col.
        apply perp_sym.
        apply H15.
      auto.
    assert(TS C D A B).
      apply ts_per_per_ts; auto.
    unfold TS in H17.
    spliter.
    ex_and H19 T1.
    ex_and H8 T.
    assert(T = T1).
      apply bet_col in H20.
      apply bet_col in H21.
      assert_diffs.
      apply (l6_21 A B C D); Col.
    subst T1.
    assert(T = E).
      assert_diffs.
      apply (l6_21 A B C D); Col.
    subst T.
    split.
      apply conga_left_comm.
      eapply out_conga.
        apply H4.
        apply out_trivial; auto.
        apply out_trivial; auto.
        apply out_trivial; auto.
      unfold Out.
      repeat split; auto.
      intro.
      subst E.
      contradiction.
    split.
      apply conga_sym.
      apply conga_right_comm.
      eapply out_conga.
        apply H4.
        apply out_trivial; auto.
        unfold Out.
        repeat split; auto.
        intro.
        subst E.
        contradiction.
        apply out_trivial; auto.
      apply out_trivial; auto.
    assumption.
Qed.

  Lemma triangle_mid_par : A B C P Q, ¬Col A B C Midpoint P B C Midpoint Q A C Par_strict A B Q P.
  Proof.
  intros.
   assert(HM:= midpoint_existence A B).
   ex_and HM R.
   assert(HH:= l13_1 A B C P Q R H H0 H1 H2).
   ex_and HH X.
   ex_and H3 Y.
assert(HH:= perp_in_col X Y A B R H3).
spliter.
   apply perp_in_perp_bis in H3.
unfold Midpoint in H2.
spliter.
apply bet_col in H2.
assert(X Y).
apply perp_distinct in H4.
tauto.

   induction H3.
   assert(Perp Y X A B).
apply (perp_col _ R); Perp.
Col.
apply perp_left_comm in H9.
assert(Par A B P Q).
   apply(l12_9 A B P Q X Y);Perp.
induction H10.
finish.
spliter.
assert(Col A B P).
ColR.
assert(P = B).
apply (l6_21 A B C P); Col.
unfold Midpoint in H0.
spliter.
apply bet_col in H0.
Col.
intro.
subst P.
contradiction.
subst P.
unfold Midpoint in H0.
spliter.
apply cong_symmetry in H15.
apply cong_identity in H15.
subst C.
contradiction.

assert(Perp X Y A B).
apply (perp_col _ R); Perp.
Col.
assert(Par A B P Q).
   apply(l12_9 A B P Q X Y);Perp.
induction H10.
finish.
spliter.
assert(Col A B P).
ColR.
assert(P = B).
apply (l6_21 A B C P); Col.
unfold Midpoint in H0.
spliter.
apply bet_col in H0.
Col.
intro.
subst P.
contradiction.
subst P.
unfold Midpoint in H0.
spliter.
apply cong_symmetry in H15.
apply cong_identity in H15.
subst C.
contradiction.
Qed.

Lemma perp_in_perp_in_col : A B A' B' X Y P, Perp_at P A B X Y Perp_at P A' B' X Y Col A B A'.
Proof.
intros.
assert(HP1:= H).
assert(HP2:=H0).
assert(Col A B P Col X Y P).
apply perp_in_col in H.
spliter.
split; Col.
spliter.
unfold Perp_at in H.
unfold Perp_at in H0.
spliter.
induction(eq_dec_points A P);
induction(eq_dec_points P X).
subst A.
subst X.
assert(Per B P Y).
apply(H10 B Y); Col.
assert(Per A' P Y).
apply(H6 A' Y); Col.
apply col_permutation_2.
apply(per_per_col B A' Y P); auto.
subst A.
assert(Per B P X).
apply(H10 B X); Col.
assert(Per A' P X).
apply(H6 A' X); Col.
apply col_permutation_2.
apply(per_per_col B A' X P); auto.
subst X.
assert(Per A P Y).
apply(H10 A Y); Col.
induction(eq_dec_points P A').
subst A'.
assert(Per B' P Y).
apply(H6 B' Y); Col.
assert(Col A B' P).
apply(per_per_col A B' Y P); auto.
ColR.

assert(Per A' P Y).
apply(H6 A' Y); Col.
assert(Col A A' P).
apply(per_per_col A A' Y P); auto.
ColR.

assert(Per A P X).
apply(H10 A X); Col.
induction(eq_dec_points P A').
subst A'.
assert(Per B' P X).
apply(H6 B' X); Col.
assert(Col A B' P).
apply(per_per_col A B' X P); auto.
ColR.

assert(Per A' P X).
apply(H6 A' X); Col.
assert(Col A A' P).
apply(per_per_col A A' X P); auto.
ColR.
Qed.

Lemma l13_2 : A B C D E, TS A B C D Per B C A Per B D A Col C D E Perp A E C D
     CongA B A C D A E CongA B A D C A E Bet C E D.
Proof.
    intros.
    assert(HH:= H).
    unfold TS in HH.
    assert(¬ Col C A B).
      spliter.
      assumption.
    spliter.
    assert(C D).
      intro.
      subst D.
      assert(OS A B C C).
        apply one_side_reflexivity.
        assumption.
      apply l9_9 in H.
      contradiction.
    assert( C', CongA B A C D A C' OS D A C' B).
      apply(angle_construction_1 B A C D A B).
        intro.
        apply H5.
        Col.
      intro.
      apply H6.
      Col.
    ex_and H9 E'.
    assert(A B A C A D).
      unfold CongA in H9.
      spliter; auto.
    spliter.
    assert(HH:=l11_22 C A E' B D A B E').
    assert(HH1:=ts_per_per_ts A B C D H H0 H1).
    unfold TS in HH1.
    assert (¬ Col A C D).
      spliter.
      assumption.
    spliter.
    ex_and H7 T.
    ex_and H17 T2.
    assert(T = T2).
      apply (l6_21 A B C D); Col.
    subst T2.
    assert(InAngle B D A C).
      unfold InAngle.
      repeat split; auto.
       T.
      split.
        Between.
      right.
      unfold Out.
      repeat split.
        intro.
        subst T.
        assert(¬ Col C D A Per A E D).
          apply(l8_16_1 C D A D E H8 H2).
            Col.
            intro.
            subst E.
            apply H15.
            auto.
          apply perp_sym.
          assumption.
        spliter.
        apply H20.
        Col.
        auto.
      left.
      assumption.
    assert(LeA C A B C A D).
      unfold LeA.
       B.
      split.
        apply l11_24.
        assumption.
      apply conga_refl; auto.
    assert(InAngle E' D A C).
      eapply lea_in_angle.
        apply lea_comm.
        eapply l11_30.
        apply H21.
        apply conga_comm.
        assumption.
        apply conga_refl; auto.
      assert(HH1:=ts_per_per_ts A B C D H H0 H1).
      assert(OS D A C B).
        apply ts_ts_os.
          apply invert_two_sides.
          assumption.
        apply l9_2.
        assumption.
      eapply one_side_transitivity.
        apply H22.
      apply one_side_symmetry.
      assumption.
    unfold InAngle in H22.
    spliter.
    ex_and H25 E''.
    induction H26.
      subst E''.
      apply False_ind.
      apply H15.
      apply bet_col in H25.
      Col.
    assert(CongA B A C D A E'').
      eapply (out_conga B A C D A E').
        auto.
        apply out_trivial; auto.
        apply out_trivial; auto.
        apply out_trivial; auto.
      apply l6_6.
      auto.
    assert(A T).
      intro.
      subst T.
      apply H15.
      Col.
    induction(eq_dec_points E'' T).
      subst E''.
      apply l13_2_1; auto.
      eapply out_conga.
        apply conga_left_comm.
        apply H27.
        apply out_trivial; auto.
        apply out_trivial; auto.
        apply out_trivial; auto.
      unfold Out.
      repeat split; auto.
    assert(D E'').
      intro.
      subst E''.
      apply conga_sym in H27.
      apply eq_conga_out in H27.
      apply out_col in H27.
      apply H5.
      Col.
    assert(C E'').
      intro.
      subst E''.
      assert(Out A B D TS C A B D).
        apply(conga__or_out_ts C A B D).
        apply conga_comm.
        assumption.
      induction H31.
        apply out_col in H31.
        apply H6.
        Col.
      assert(OS A C B D).
        apply ts_ts_os.
          assumption.
        apply ts_per_per_ts; auto.
      apply invert_one_side in H32.
      apply l9_9 in H31.
      contradiction.
    assert(A E'').
      intro.
      subst E''.
      unfold Out in H26.
      tauto.
    assert(¬ Col E'' A B).
      intro.
      apply H29.
      apply bet_col in H25.
      apply (l6_21 A B C D); Col.
    assert(CongA C A E'' D A B).
      apply (l11_22 C A E'' B D A B E'').
      split.
        induction(one_side_dec A B C E'').
          right.
          split.
            auto.
          unfold OS.
           C.
          split.
            unfold TS.
            repeat split.
              auto.
              intro.
              apply H15.
              apply bet_col in H25.
              apply col_permutation_1.
              eapply (col_transitivity_1 _ E''); Col.
              intro.
              apply bet_col in H25.
              apply H15.
              apply col_permutation_2.
              eapply (col_transitivity_1 _ E''); Col.
             E''.
            split; Col.
          assert(TS A E'' T C).
            unfold TS.
            repeat split.
              auto.
              intro.
              apply H29.
              apply (l6_21 A B C D);Col.
              eapply (col_transitivity_1 _ T); Col.
              apply bet_col in H25.
              Col.
              intro.
              apply H15.
              ColR.
             E''.
            split.
              Col.
            assert(Bet C T E'' Bet C E'' T).
              eapply l5_3.
                apply H18.
              Between.
            induction H35.
              assert(TS A B C E'').
                unfold TS.
                repeat split; auto.
                 T.
                split.
                  Col.
                auto.
              apply l9_9 in H36.
              contradiction.
            Between.
          eapply (l9_5 _ _ T _ A); Col.
          unfold Out.
          repeat split; auto.
        left.
        apply not_one_side_two_sides in H34; auto.
        split.
          auto.
        assert(OS A B D E'').
          eapply l9_8_1.
            apply l9_2.
            apply H.
          apply l9_2.
          assumption.
        assert(TS A E'' T D).
          unfold TS.
          repeat split.
            auto.
            intro.
            apply H33.
            apply col_permutation_2.
            apply(col_transitivity_1 _ T); Col.
            intro.
            apply bet_col in H25.
            apply H15.
            apply col_permutation_1.
            eapply (col_transitivity_1 _ E''); Col.
           E''.
          split.
            Col.
          assert(Bet D T E'' Bet D E'' T).
            eapply l5_3.
              apply between_symmetry.
              apply H18.
            assumption.
          induction H36.
            assert(TS A B D E'').
              unfold TS.
              repeat split; auto.
               T.
              split; Col.
            apply l9_9 in H37.
            contradiction.
          Between.
        apply l9_2.
        eapply (l9_5 _ _ T _ A).
          auto.
          Col.
        unfold Out.
        repeat split; auto.

      split.
        apply conga_left_comm.
        auto.
      apply conga_right_comm.
      apply conga_refl; auto.
    prolong B C C' B C.
    prolong B D D' B D.
    assert(Cong_3 B A D D' A D).
      apply l8_2 in H1.
      unfold Per in H1.
      ex_and H1 D''.
      assert(Midpoint D B D').
        unfold Midpoint.
        split; Cong.
      assert(D' = D'').
        eapply symmetric_point_uniqueness.
          apply H40.
        auto.
      subst D''.
      repeat split; Cong.
    assert(CongA B A D D' A D).
      apply cong3_conga; auto.
    assert(Cong_3 B A C C' A C).
      apply l8_2 in H0.
      unfold Per in H0.
      ex_and H0 C''.
      assert(Midpoint C B C').
        unfold Midpoint.
        split; Cong.
      assert(C' = C'').
        eapply symmetric_point_uniqueness.
          apply H42.
        auto.
      subst C''.
      repeat split; Cong.
    assert(CongA B A C C' A C).
      apply cong3_conga; auto.
    assert(CongA E'' A C' D' A E'').
      apply l11_22 with C D.
      split.
        clear HH.
        left.
        assert(OS C A D E'').
          eapply out_out_one_side.
            apply one_side_reflexivity.
            intro.
            apply H15.
            Col.
          unfold Out.
          repeat split; auto.
          right.
          Between.
        assert(OS C A B D).
          apply in_angle_one_side.
            intro.
            apply H15.
            Col.
            intro.
            apply H5.
            Col.
          apply l11_24.
          auto.
        assert(TS C A B C').
          unfold TS.
          repeat split.
            auto.
            intro.
            apply H5.
            Col.
            intro.
            apply H5.
            apply bet_col in H35.
            assert(C C').
              intro.
              subst C'.
              apply cong_symmetry in H36.
              apply cong_identity in H36.
              subst C.
              apply H16.
              Col.
            eapply (col_transitivity_1 _ C'); Col.
           C.
          split; Col.
        assert(OS C A B E'').
          eapply one_side_transitivity.
            apply H44.
          auto.
        assert(OS D A C E'').
          eapply out_out_one_side.
            apply one_side_reflexivity.
            intro.
            apply H15.
            Col.
          unfold Out.
          repeat split; auto.
        assert(OS D A B C).
          apply in_angle_one_side.
            intro.
            apply H15.
            Col.
            intro.
            apply H6.
            Col.
          auto.
        assert(TS D A B D').
          unfold TS.
          repeat split.
            auto.
            intro.
            apply H6.
            Col.
            intro.
            apply H6.
            apply bet_col in H37.
            assert(D D').
              intro.
              subst D'.
              apply cong_symmetry in H38.
              apply cong_identity in H38.
              subst D.
              apply H16.
              Col.
            eapply (col_transitivity_1 _ D'); Col.
           D.
          split; Col.
        assert(OS D A B E'').
          eapply one_side_transitivity.
            apply H48.
          auto.
        split.
          apply invert_two_sides.
          eapply l9_8_2.
            apply H45.
          auto.
        apply invert_two_sides.
        apply l9_2.
        eapply l9_8_2.
          apply H49.
        auto.
      split.
        eapply conga_trans.
          apply conga_comm.
          apply H34.
        apply H40.
      apply conga_sym.
      eapply conga_trans.
        apply conga_sym.
        apply H27.
      apply conga_right_comm.
      auto.
    assert(D' B).
      intro.
      subst D'.
      apply between_identity in H37.
      subst D.
      apply H16.
      Col.
    assert(C' B).
      intro.
      subst C'.
      apply between_identity in H35.
      subst C.
      apply H16.
      Col.
    assert(¬ Col C' D' B).
      intro.
      apply H16.
      apply bet_col in H35.
      apply bet_col in H37.
      assert(Col C' B D).
        ColR.
      ColR.
    assert(Par_strict C' D' C D).
      apply(triangle_mid_par C' D' B D C).
        auto.
        unfold Midpoint.
        split.
          Between.
        Cong.
      unfold Midpoint.
      split.
        Between.
      Cong.
    assert(TS A E'' C D).
      unfold TS.
      repeat split.
        auto.
        intro.
        apply H15.
        apply bet_col in H25.
        apply col_permutation_2.
        eapply (col_transitivity_1 _ E''); Col.
        intro.
        apply H15.
        apply bet_col in H25.
        apply col_permutation_1.
        eapply (col_transitivity_1 _ E''); Col.
       E''.
      split; Col.
      Between.
    assert(TS B A C D).
      apply in_angle_two_sides.
        intro.
        apply H5.
        Col.
        intro.
        apply H6.
        Col.
      apply l11_24.
      assumption.
    assert (OS A B C C').
      apply (out_one_side_1 _ _ _ _ B); Col.
      unfold Out.
      repeat split; auto.
      intro.
      subst C.
      apply H5.
      Col.
    assert (OS A B D D').
      apply (out_one_side_1 _ _ _ _ B); Col.
      unfold Out.
      repeat split; auto.
      intro.
      subst D.
      apply H6.
      Col.
    apply invert_two_sides in H49.
    assert(TS A B C' D).
      eapply l9_8_2.
        apply H49.
      auto.
    assert(TS A B C' D').
      apply l9_2.
      eapply l9_8_2.
        apply l9_2.
        apply H52.
      auto.
    assert(Perp C' D' A E'').
      eapply cong_conga_perp.
        apply conga_right_comm in H43.
        apply conga__or_out_ts in H43.
        induction H43.
          assert(OS A B C' D').
            eapply (out_one_side_1 _ _ _ _ A); Col.
            intro.
            assert(B C').
              intro.
              subst C'.
              apply H46.
              Col.
            apply H5.
            apply col_permutation_1.
            eapply col_transitivity_1.
              apply H55.
              apply bet_col in H35.
              Col.
            Col.
          apply l9_9 in H53.
          contradiction.
        apply invert_two_sides.
        assumption.
        unfold Cong_3 in ×.
        spliter.
        apply cong_transitivity with B A; Cong.
      apply conga_left_comm.
      assumption.

assert(Cong A C' A B).
apply l8_2 in H0.
unfold Per in H0.
ex_and H0 C''.
assert(C' = C'').
apply(symmetric_point_uniqueness B C C' C''); finish.
split; finish.
subst C''.
Cong.

assert(Cong A D' A B).
apply l8_2 in H1.
unfold Per in H1.
ex_and H1 D''.
assert(D' = D'').
apply(symmetric_point_uniqueness B D D' D''); finish.
split; finish.
subst D''.
Cong.

assert(Cong A C' A D').
apply cong_transitivity with A B; Cong.

assert(HM:=midpoint_existence C' D').
ex_and HM R.
assert( X Y : Tpoint, Perp_at R X Y C' D' Perp X Y D C).
apply(l13_1 C' D' B D C R);
finish.
split; Between; Cong.
split; Between; Cong.
ex_and H59 X.
ex_and H60 Y.

assert(HXY:X Y).
apply perp_distinct in H60.
tauto.

assert(Perp C D A E'').

induction(eq_dec_points A R).
subst R.

assert(Perp_at A C' D' A E'').
assert_cols.
apply(l8_14_2_1b_bis C' D' A E'' A); Col.

assert(Col X Y A).
apply(perp_in_perp_in_col X Y A E'' C' D' A); finish.
assert(Col X Y E'').
apply(perp_in_perp_in_col X Y E'' A C' D' A); finish.
apply perp_sym.
induction(eq_dec_points Y A).
subst Y.
apply(perp_col _ X).
auto.
Perp.
Col.
apply(perp_col _ Y).
auto.
apply perp_left_comm.
apply (perp_col _ X); Col.
Perp.
ColR.

assert(R C').
intro.
subst R.
unfold Midpoint in H58.
spliter.
apply cong_symmetry in H62.
apply cong_identity in H62.
subst D'.
apply perp_distinct in H54.
tauto.

assert(Per A R C').
unfold Per.
D'.
split; finish.
apply per_perp_in in H63; auto.
apply perp_in_sym in H63.
apply perp_in_perp_bis in H63.
induction H63.
apply perp_comm in H63.
assert(Perp C' D' R A).
apply(perp_col _ R).
intro.
subst D'.
apply perp_distinct in H54.
tauto.
assumption.
assert_cols.
Col.

assert(Perp_at R C' D' R A).
apply(l8_14_2_1b_bis C' D' R A R); Col.
assert_cols.
Col.

assert( Col X Y A).
apply(perp_in_perp_in_col X Y A R C' D' R); Perp.
assert( Col X Y R).
apply(perp_in_perp_in_col X Y R A C' D' R); Perp.

assert(Col A E'' R).
apply(perp_perp_col A E'' R C' D'); Perp.

assert(Col A R X).
ColR.
assert(Col A R Y).
ColR.

apply perp_sym.
induction(eq_dec_points X A).
subst X.
apply (perp_col _ Y); finish.
ColR.
apply (perp_col _ X); finish.
apply perp_left_comm.
apply(perp_col _ Y); finish.
ColR.
apply perp_distinct in H63.
tauto.

    assert(Col A E E'').
      eapply perp_perp_col.

        apply H3.
Perp.

    assert(E'' = E).
      apply (l6_21 C D A E); Col.
      apply perp_not_eq_1 in H3.
      assumption.
    subst E''.
    split.
      auto.
    split.
      apply conga_sym.
      apply conga_right_comm.
      auto.
    Between.
Qed.

Lemma perp2_refl : A B P, A B Perp2 A B A B P.
Proof.
    intros.
    induction(Col_dec A B P).
      assert(HH:=not_col_exists A B H).
      ex_and HH X.
      assert(HH:=l10_15 A B P X H0 H1).
      ex_and HH Q.
      unfold Perp2.
       Q.
       P.
      split; Perp.
      Col.
    assert(HH:=l8_18_existence A B P H0).
    ex_and HH Q.
    unfold Perp2.
     P.
     Q.
    split; Perp.
    Col.
Qed.

Lemma perp2_sym : A B C D P, Perp2 A B C D P Perp2 C D A B P.
Proof.
    unfold Perp2.
    intros.
    ex_and H X.
    ex_and H0 Y.
     X.
     Y.
    repeat split; Perp.
Qed.

Lemma perp2_left_comm : A B C D P, Perp2 A B C D P Perp2 B A C D P.
Proof.
    unfold Perp2.
    intros.
    ex_and H X.
    ex_and H0 Y.
     X.
     Y.
    repeat split; Perp.
Qed.

Lemma perp2_right_comm : A B C D P, Perp2 A B C D P Perp2 A B D C P.
Proof.
    unfold Perp2.
    intros.
    ex_and H X.
    ex_and H0 Y.
     X.
     Y.
    repeat split; Perp.
Qed.

Lemma perp2_comm : A B C D P, Perp2 A B C D P Perp2 B A D C P.
Proof.
    unfold Perp2.
    intros.
    ex_and H X.
    ex_and H0 Y.
     X.
     Y.
    repeat split; Perp.
Qed.

Lemma perp2_trans : A B C D E F P, Perp2 A B C D P Perp2 C D E F P Perp2 A B E F P.
Proof.
    intros.
    unfold Perp2 in ×.
    ex_and H X.
    ex_and H1 Y.
    ex_and H0 X'.
    ex_and H3 Y'.
    assert(Par X Y X' Y').
      eapply (l12_9 _ _ _ _ C D); Perp.
     X.
     Y.
    assert(Col X X' Y').
      induction H5.
        unfold Par_strict in H5.
        spliter.
        apply False_ind.
        apply H8.
         P.
        split; Col.
      spliter.
      auto.
    assert(Col Y X' Y').
      induction H5.
        unfold Par_strict in H5.
        spliter.
        apply False_ind.
        apply H9.
         P.
        split; Col.
      spliter.
      auto.
    repeat split; auto.
    assert(X Y).
      apply perp_not_eq_1 in H1.
      assert(X' Y').
        apply perp_not_eq_1 in H3.
        auto.
      auto.
    induction(eq_dec_points X Y').
      subst Y'.
      apply (perp_col _ X').
        auto.
        Perp.
      ColR.
    apply (perp_col _ Y').
      auto.
      apply perp_left_comm.
      apply(perp_col _ X').
        auto.
        Perp.
      ColR.
    apply par_symmetry in H5.
    induction H5.
      unfold Par_strict in H5.
      spliter.
      apply False_ind.
      apply H12.
       P.
      split; Col.
    spliter.
    Col.
Qed.

Lemma perp2_par : A B C D O, Perp2 A B C D O Par A B C D.
Proof.
    intros.
    unfold Perp2 in H.
    ex_and H X.
    ex_and H0 Y.
    eapply (l12_9 _ _ _ _ X Y).
      Perp.
    Perp.
Qed.

Lemma perp2_preserves_bet23 : O A B A' B', Bet O A B Col O A' B' ¬Col O A A'
    Perp2 A A' B B' O Bet O A' B'.

Proof.
intros.

assert(HD1: A A').
intro.
subst A'.
apply H1.
Col.

induction(eq_dec_points A' B').
subst B'.
Between.

assert(A B).
intro.
subst B.
unfold Perp2 in H2.
ex_and H2 X.
ex_and H4 Y.
assert(Col A A' B').
apply(perp_perp_col A A' B' X Y); Perp.
apply H1.
ColR.

assert(Par A A' B B').
apply(perp2_par A A' B B' O H2).
induction H5.
assert(OS A A' B B').
apply l12_6; Par.
assert(TS A A' O B).
repeat split; Col.
intro.
apply H5.
B.
split; Col.
A.
split; Col.

assert(TS A A' B' O).
apply( l9_8_2 A A' B B' O); auto.
apply l9_2.
auto.

unfold TS in H8.
spliter.
ex_and H10 T.
assert(T = A').
apply (l6_21 A A' O B'); Col.
intro.
subst B'.
apply between_identity in H11.
subst T.
contradiction.
subst T.
Between.

spliter.
apply False_ind.
apply H1.
ColR.
Qed.

Lemma perp2_preserves_bet13 : O B C B' C', Bet B O C Col O B' C' ¬Col O B B'
    Perp2 B C' C B' O Bet B' O C'.

Proof.
intros.

induction(eq_dec_points C' O).
subst C'.
Between.
induction(eq_dec_points B' O).
Between.

assert(B O).
intro.
subst B.
apply H1.
Col.

assert(B' O).
intro.
subst B'.
apply H1.
Col.

assert(Col B O C).
apply bet_col.
Between.

induction(eq_dec_points B C).
subst C.
apply between_identity in H.
contradiction.

assert(Par B C' C B').
apply (perp2_par _ _ _ _ O); auto.
assert(Par_strict B C' C B').
induction H9.
assumption.
spliter.
apply False_ind.
apply H1.
ColR.

assert(C O).
intro.
subst C.
assert(Par_strict B C' O C').
apply(par_strict_col_par_strict _ _ _ B'); auto.
apply H11.
C'.
Col.

assert(B' O).
intro.
subst B'.
assert(Par_strict B C' O B).
apply(par_strict_col_par_strict _ _ _ C); auto.
apply par_strict_right_comm.
assumption.
Col.
apply H12.
B.
split; Col.

unfold Perp2 in H2.
ex_and H2 X.
ex_and H13 Y.

assert(X Y).
apply perp_distinct in H13.
tauto.

induction(Col_dec X Y B).
assert(Col X Y C).
ColR.

apply(per13_preserves_bet_inv B' O C' C B); Between.
Col.

apply perp_in_per.
induction(eq_dec_points X C).
subst X.
assert(Perp C O B' C).
apply(perp_col _ Y); Perp.
ColR.
apply perp_perp_in in H18.
Perp.
assert(Perp X C C B').
apply(perp_col _ Y); Perp.
assert(Perp C O B' C).
apply(perp_col _ X); Perp.
ColR.
apply perp_perp_in in H20.
Perp.

apply perp_in_per.
induction(eq_dec_points X B).
subst X.
assert(Perp B O C' B).
apply(perp_col _ Y); Perp.
ColR.
apply perp_perp_in in H18.
Perp.
assert(Perp X B C' B).
apply(perp_col _ Y); Perp.
assert(Perp B O C' B).
apply(perp_col _ X); Perp.
ColR.
apply perp_perp_in in H20.
Perp.

assert(HP1:=l8_18_existence X Y B H16).
ex_and HP1 B0.
assert(¬Col X Y C).
intro.
apply H16.
ColR.
assert(HP1:=l8_18_existence X Y C H19).
ex_and HP1 C0.

assert(B0 O).
intro.
subst B0.
assert(Par B O B C').
apply(l12_9 B O B C' X Y); Perp.
induction H22.
apply H22.
B.
split; Col.
spliter.
apply H1.
ColR.

assert(C0 O).
intro.
subst C0.
assert(Par C O C B').
apply(l12_9 C O C B' X Y); Perp.
induction H23.
apply H23.
C.
split; Col.
spliter.
apply H1.
ColR.

assert(Bet B0 O C0).

apply(per13_preserves_bet B O C B0 C0); auto.
Between.
ColR.
apply perp_in_per.
induction(eq_dec_points X B0).
subst X.
assert(Perp B0 O B B0).
apply(perp_col _ Y); Perp.
Col.
apply perp_perp_in in H24.
Perp.
assert(Perp X B0 B B0).
apply(perp_col _ Y); Perp.
assert(Perp B0 O B B0).
apply (perp_col _ X); Perp.
ColR.
apply perp_perp_in in H26.
Perp.

apply perp_in_per.
induction(eq_dec_points X C0).
subst X.
assert(Perp C0 O C C0).
apply(perp_col _ Y); Perp.
Col.
apply perp_perp_in in H24.
Perp.
assert(Perp X C0 C C0).
apply(perp_col _ Y); Perp.
assert(Perp C0 O C C0).
apply (perp_col _ X); Perp.
ColR.
apply perp_perp_in in H26.
Perp.

induction(eq_dec_points C' B0).
subst B0.
assert(B' = C0).
apply bet_col in H24.
apply (l6_21 C' O C C0); Col.
assert(Par C B' C C0).
apply(l12_9 C B' C C0 X Y); Perp.

induction H25.
apply False_ind.
apply H25.
C.
split; Col.
spliter.
Col.
intro.
apply H1.
ColR.
intro.
subst C0.
apply H1.
ColR.
apply(perp_perp_col C C0 B' X Y); Perp.
subst C0.
Between.

assert(B' C0).
intro.
subst C0.
apply H25.
apply (l6_21 B' O B B0); Col.
intro.
subst B0.
Col.
assert(Par B C' B B0).
apply(l12_9 B C' B B0 X Y); Perp.

induction H26.
apply False_ind.
apply H26.
B.
split; Col.
spliter.
Col.

assert(Col C C0 B').
apply(perp_perp_col C C0 B' X Y); Perp.
assert(Col B B0 C').
apply(perp_perp_col B B0 C' X Y); Perp.

apply(per13_preserves_bet_inv B' O C' C0 B0); Between.
Col.

apply perp_in_per.
induction(eq_dec_points X C0).
subst X.
assert(Perp C0 O C B').
apply (perp_col _ Y); Perp.
Col.
assert(Perp B' C0 C0 O).
apply(perp_col _ C); Perp.
Col.
apply perp_comm in H30.
apply perp_perp_in in H30.
Perp.

assert(Perp X C0 C B').
apply(perp_col _ Y); Perp.
assert(Perp C0 O C B').
apply (perp_col _ X); Perp.
ColR.
assert(Perp B' C0 C0 O).
apply(perp_col _ C); Perp.
Col.
apply perp_comm in H32.
apply perp_perp_in in H32.
Perp.

apply perp_in_per.

assert(Perp C' B0 X Y).
apply (perp_col _ B); Perp.
Col.
induction (eq_dec_points X O).
subst X.
assert(Perp O B0 B0 C').
apply(perp_col _ Y);Perp.
apply perp_comm in H30.
apply perp_perp_in in H30.
Perp.

assert(Perp X O C' B0).
apply(perp_col _ Y); Perp.
Col.
assert(Perp O B0 B0 C').
apply(perp_col _ X); Perp.
ColR.
apply perp_comm in H32.
apply perp_perp_in in H32.
Perp.

Qed.

Lemma is_image_perp_in : A A' X Y, A A' X Y Reflect A A' X Y P, Perp_at P A A' X Y.
Proof.
intros.
unfold Reflect in H.
induction H1.
spliter.
unfold ReflectL in H2.
spliter.
ex_and H2 P.
induction H3.
P.

apply perp_in_sym.
apply perp_in_right_comm.
apply(l8_14_2_1b_bis X Y A' A P); Col.
assert_cols.
Col.
subst A'.
tauto.
spliter.
contradiction.
Qed.

Lemma perp_inter_perp_in_n
     : A B C D : Tpoint,
       Perp A B C D
        P : Tpoint, Col A B P Col C D P Perp_at P A B C D.
Proof.
intros.
assert(A B C D).
apply perp_distinct in H.
tauto.
spliter.
induction(Col_dec A B C).
C.
split; Col.
split; Col.
apply(l8_14_2_1b_bis A B C D C); Col.

assert(HH:=l8_18_existence A B C H2).
ex_and HH P.
P.
assert(Col C D P).
apply(perp_perp_col C D P A B); Perp.
split; Col.
split; Col.
apply(l8_14_2_1b_bis A B C D P); Col.
Qed.

Lemma perp2_perp_in : A B C D O, Perp2 A B C D O ¬Col O A B ¬Col O C D
     P, Q, Col A B P Col C D Q Col O P Q Perp_at P O P A B Perp_at Q O Q C D.
  Proof.
    intros.
    unfold Perp2 in H.
    ex_and H X.
    ex_and H1 Y.
    assert(X Y).
      apply perp_not_eq_1 in H2.
      auto.
    assert(HH:= perp_inter_perp_in_n X Y A B H2).
    ex_and HH P.
    assert(HH:= perp_inter_perp_in_n X Y C D H3).
    ex_and HH Q.
     P.
     Q.
    split; auto.
    split; auto.
    split.
      apply (col3 X Y); Col.
    split.
      induction(eq_dec_points X O).
        subst X.
        apply perp_in_sym.
        apply(perp_in_col_perp_in A B O Y P P).
          intro.
          subst P.
          apply H.
          Col.
          Col.
        apply perp_in_sym.
        auto.
      assert(Perp_at P A B X O).
        apply(perp_in_col_perp_in A B X Y O P H11).
          Col.
        apply perp_in_sym.
        auto.
      apply perp_in_right_comm in H12.
      eapply (perp_in_col_perp_in _ _ _ _ P) in H12 .
        apply perp_in_sym.
        auto.
        intro.
        subst P.
        apply H.
        Col.
      ColR.
    induction(eq_dec_points X O).
      subst X.
      apply perp_in_sym.
      apply(perp_in_col_perp_in C D O Y Q Q).
        intro.
        subst Q.
        apply H0.
        Col.
        Col.
      apply perp_in_sym.
      auto.
    assert(Perp_at Q C D X O).
      apply(perp_in_col_perp_in C D X Y O Q H11).
        Col.
      apply perp_in_sym.
      auto.
    apply perp_in_right_comm in H12.
    eapply (perp_in_col_perp_in _ _ _ _ Q) in H12 .
      apply perp_in_sym.
      auto.
      intro.
      subst Q.
      apply H0.
      Col.
    ColR.
Qed.

Lemma l13_8 : O P Q U V, U O V O Col O P Q Col O U V
     Per P U O Per Q V O (Out O P Q Out O U V).
Proof.
    intros.
    induction(eq_dec_points P U).
      subst P.
      assert(Col Q V O).
        ColR.
      assert(HH:= l8_9 Q V O H4 H5).
      induction HH.
        subst Q.
        tauto.
      subst V.
      tauto.
    assert(Q V).
      intro.
      subst Q.
      assert(HH:= per_not_col P U O H5 H H3).
      apply HH.
      ColR.
split.
intro.
unfold Out in H7.
spliter.
induction H9.

assert(HH:= per23_preserves_bet O P Q U V).
repeat split; auto.
left.
apply(per23_preserves_bet O P Q U V); auto.
Perp.
Perp.
repeat split; auto.
right.
apply(per23_preserves_bet O Q P V U); Col.
Perp.
Perp.

intro.
unfold Out in H7.
spliter.

repeat split.
intro.
subst P.
apply l8_8 in H3.
contradiction.
intro.
subst Q.
apply l8_8 in H4.
contradiction.
induction H9.
left.
apply(per23_preserves_bet_inv O P Q U V); Perp.
right.
apply(per23_preserves_bet_inv O Q P V U); Perp.
Col.
Qed.

Lemma perp_in_rewrite : A B C D P, Perp_at P A B C D
                                          Perp_at P A P P C
                                          Perp_at P A P P D
                                          Perp_at P B P P C
                                          Perp_at P B P P D.
Proof.
intros.
assert(HH:= perp_in_col A B C D P H).
spliter.
induction(eq_dec_points A P);
induction(eq_dec_points C P).
subst A .
subst C.
right;right;right.
Perp.
subst A.
right; right; left.
apply perp_in_right_comm.
assert(HP:=perp_in_col_perp_in P B C D P P H3 H1 H).
Perp.
subst C.
right; left.
apply perp_in_sym.
apply(perp_in_col_perp_in P D A B P P H2 H0).
Perp.
left.
assert(HP:= perp_in_col_perp_in A B C D P P H3 H1 H).
apply perp_in_sym.
apply perp_in_left_comm.
apply(perp_in_col_perp_in C P A B P P H2 H0).
Perp.
Qed.

Lemma gta_to_lta : A B C D E F, GtA A B C D E F LtA D E F A B C.
Proof.
intros.
unfold GtA in H.
assumption.
Qed.

Lemma lta_to_gta : A B C D E F, LtA A B C D E F GtA D E F A B C.
Proof.
intros.
unfold GtA.
assumption.
Qed.

Lemma conga_preserves_obtuse : A B C A' B' C', Obtuse A B C CongA A B C A' B' C' Obtuse A' B' C'.
Proof.
intros.
unfold Obtuse in ×.
ex_and H A1.
ex_and H1 B1.
ex_and H C1.

A1.
B1.
C1.
split; auto.

assert(A1 B1 C1 B1).
unfold GtA in H1.
unfold LtA in H1.
spliter.
unfold LeA in H1.
ex_and H1 P.
unfold CongA in H3.
spliter.
split; auto.

unfold GtA in ×.
spliter.
apply(conga_preserves_lta A1 B1 C1 A B C A1 B1 C1 A' B' C'); auto.
apply conga_refl; auto.
Qed.

Lemma perp_out_acute : A B C C', Out B A C' Perp A B C C' Acute A B C.
Proof.
intros.
assert(A B C' B).
apply out_distinct.
assumption.
spliter.

assert(Perp B C' C C').
apply(perp_col _ A); Perp.
apply out_col in H.
Col.
assert(Per C C' B).
apply perp_in_per.
apply perp_sym in H3.
apply perp_left_comm in H3.
apply perp_perp_in in H3.
apply perp_in_comm.
assumption.
assert(Acute C' C B Acute C' B C).
apply( l11_43 C' C B).

apply perp_left_comm in H3.
apply perp_not_col in H3.
intro.
apply H3.
assert_cols.
ColR.
left.
assumption.
spliter.

assert(C B).
intro.
subst C.
apply l8_8 in H4.
subst C'.
apply perp_distinct in H0.
tauto.

assert(CongA C' B C A B C ).
apply(out_conga A B C A B C C' C A C); auto.
apply conga_refl; auto.
apply out_trivial; auto.
apply out_trivial; auto.
apply out_trivial; auto.
apply (acute_conga__acute C' B C); auto.
Qed.

Lemma flat_all_lea : A B C, A B C B Bet A B C P, P B LeA A B P A B C.
Proof.
intros.
unfold LeA.
P.
spliter.
split.
unfold InAngle.
repeat split; auto.
B.
split; auto.
apply conga_refl; auto.
Qed.

Lemma acute_bet_obtuse : A B C P, B C Bet A B C Acute A B P Obtuse C B P.
Proof.
intros.

assert(A C).
intro.
subst C.
apply between_identity in H0.
subst B.
tauto.

assert(A B).
unfold Acute in H1.
ex_and H1 A'.
ex_and H3 B'.
ex_and H1 P'.
unfold LtA in H3.
spliter.
unfold LeA in H3.
ex_and H3 X.
apply conga_distinct in H5.
tauto.

assert(D : P B).
unfold Acute in H1.
ex_and H1 A'.
ex_and H4 B'.
ex_and H1 Q'.
unfold LtA in H4.
spliter.
unfold LeA in H4.
ex_and H4 X.
apply conga_distinct in H6.
tauto.

induction(Col_dec A B P).
assert(HH:= perp_exists B A B H3).
ex_and HH Q.

assert(HD: Q B).
apply perp_distinct in H5.
intro.
subst Q.
tauto.

assert(Per A B Q).
apply perp_in_per.
apply perp_perp_in in H5.
Perp.

unfold Obtuse.
A.
B.
Q.
split; auto.

assert(Out B A P).
apply(col_in_angle_out A B Q); Col.
intro.
apply perp_not_col in H5.
apply H5.
apply bet_col in H7.
Col.

unfold Acute in H1.
ex_and H1 A'.
ex_and H7 B'.
ex_and H1 Q'.

assert(CongA A B Q A' B' Q').
apply l11_16; auto.

intro.
subst B'.
unfold LtA in H7.
spliter.
unfold LeA in H7.
ex_and H7 X.
apply conga_distinct in H9.
tauto.
intro.
subst Q'.
unfold LtA in H7.
spliter.
unfold LeA in H7.
ex_and H7 X.
unfold InAngle in H7.
tauto.

assert(LtA A B P A B Q).

apply(conga_preserves_lta A B P A' B' Q' A B P A B Q).
apply conga_refl;auto.
apply conga_sym.
assumption.
assumption.
unfold InAngle.
repeat split; auto.
unfold LtA in H9.
spliter.
A.
split.
Between.
right.

induction H4.

assert(HH:= flat_all_lea A B P H3 D H4).
assert(HP:=HH Q HD).
assert(HQ:=lea_asym A B P A B Q H9 HP).
contradiction.

induction H4.
unfold Out.
repeat split; auto.
unfold Out.
repeat split; auto.
left.
Between.

unfold GtA.
unfold LtA.
split.
unfold LeA.
Q.
split.
unfold InAngle.
repeat split; auto.
B.
split.

induction H7.
spliter.
induction H9.

apply (outer_transitivity_between _ _ A); Between.
apply (between_inner_transitivity _ _ _ A); Between.
left.
auto.
apply l11_16; Perp.

assert(Perp B C B Q).
apply (perp_col _ A);Perp.
apply bet_col in H0.
Col.
apply perp_in_per.
apply perp_right_comm in H8.
apply perp_perp_in in H8.
Perp.
intro.

assert(HH:= l11_17 A B Q C B P H6 H8).
apply per_not_col in HH; auto.
apply HH.
apply bet_col in H0.
ColR.

assert(HC:Col A B C).
apply bet_col in H0.
Col.

assert( Q : Tpoint, Perp A C Q B OS A C P Q).
apply(l10_15 A C B P); Col.
intro.
apply H4.
ColR.

ex_and H5 Q.
assert(Perp A B Q B).
apply (perp_col _ C); Perp.
Col.
apply perp_left_comm in H7.

assert(¬Col B A Q).
apply perp_not_col in H7.
assumption.

assert(Per A B Q).
apply perp_in_per.
apply perp_perp_in in H7.
Perp.

assert(B Q).
intro.
subst Q.
apply H8.
Col.

assert(OS B Q A P).
unfold Acute in H1.
ex_and H1 A'.
ex_and H11 B'.
ex_and H1 Q'.
assert(CongA A B Q A' B' Q').
apply l11_16; auto.
unfold LtA in H11.
spliter.
unfold LeA in H11.
ex_and H11 X.
apply conga_distinct in H13.
tauto.
unfold LtA in H11.
spliter.
unfold LeA in H11.
ex_and H11 X.
unfold InAngle in H11.
tauto.

assert(LtA A B P A B Q).
apply(conga_preserves_lta A B P A' B' Q' A B P A B Q ); auto.
apply conga_refl; auto.
apply conga_sym.
assumption.
unfold LtA in H13.
spliter.
unfold LeA in H13.
ex_and H13 P0.

assert(InAngle P A B Q).

apply(conga_preserves_in_angle A B Q P0 A B Q P).
apply conga_refl; auto.
apply conga_sym.
assumption.
assumption.
apply (col_one_side _ C); Col.

unfold InAngle in H16.
spliter.

ex_and H19 X.

induction H20.
subst X.
apply False_ind.
apply H8.
apply bet_col in H19.
Col.

assert(OS Q B A X).
apply out_one_side.
left.
intro.
apply H8.
Col.
repeat split.
intro.
subst Q.
apply l8_8 in H9.
contradiction.
intro.
subst X.
apply H14.
apply conga_sym.
apply(out_conga A B P A B P A Q A P).
apply conga_refl; auto.
apply out_trivial; auto.
apply l6_6.
assumption.
apply out_trivial; auto.
apply out_trivial; auto.
right.
Between.

assert(OS B Q X P).

apply( out_one_side B Q X P).
right.
intro.
apply H14.

apply conga_sym.
apply(out_conga A B P A B P A Q A P).
apply conga_refl; auto.
apply out_trivial; auto.

apply(col_one_side_out _ C).
Col.
apply invert_one_side.

apply(col_one_side _ A); Col.
apply invert_one_side.
assumption.
apply out_trivial; auto.
apply out_trivial; auto.
assumption.
apply invert_one_side in H21.
eapply(one_side_transitivity _ _ _ X); auto.

assert(TS B Q A C).
unfold TS.
repeat split; auto.
intro.
apply H8.
Col.
intro.
apply H8.
ColR.
B.
split; Col.

assert(TS B Q P C).
apply(l9_8_2 B Q A P C); auto.

unfold Obtuse.
A.
B.
Q.
split; auto.
unfold GtA.
unfold LtA.

assert(HP:Per C B Q).
assert(Perp B C Q B).
apply(perp_col _ A); Perp.
Col.
apply perp_in_per.
apply perp_perp_in in H14.
Perp.

split.
unfold LeA.
Q.
split.
unfold InAngle.
repeat split; auto.
unfold TS in H13.
spliter.
ex_and H15 X.
X.
split; Between.
right.

assert(OS C A X P).
apply out_one_side.
right.
intro.
apply H4.
ColR.
repeat split.
intro.
subst X.
contradiction.
intro.
subst P.
apply between_identity in H16.
subst X.
contradiction.
left.
Between.
apply invert_one_side in H17.
assert(OS A C X Q).
apply (one_side_transitivity _ _ _ P); auto.
apply(col_one_side_out B C X Q).
Col.
apply invert_one_side.
apply(col_one_side _ A); Col.
apply invert_one_side.
assumption.
apply l11_16; Perp.

assert(CongA A B Q C B Q).
apply l11_16; Perp.
intro.
assert(CongA C B Q C B P).
apply(conga_trans _ _ _ A B Q); auto.
apply conga_sym.
auto.

unfold Acute in H1.
ex_and H1 A'.
ex_and H17 B'.
ex_and H1 Q'.
assert(CongA A B Q A' B' Q').
apply l11_16; Perp.
intro.
subst B'.
unfold LtA in H17.
spliter.
unfold LeA in H17.
ex_and H17 X.
apply conga_distinct in H19.
tauto.
intro.
subst Q'.
unfold LtA in H17.
spliter.
unfold LeA in H17.
ex_and H17 X.
unfold InAngle in H17.
tauto.
assert(LtA A B P A B Q).
apply(conga_preserves_lta A B P A' B' Q' A B P A B Q); auto.
apply conga_refl; auto.
apply conga_sym; auto.
unfold LtA in H19.
spliter.
apply H20.
apply conga_sym.
apply(l11_13 C B Q C B P A A H16); Between.
Qed.

Lemma perp_bet_obtuse : A B C C', B C' Perp A B C C' Bet A B C' Obtuse A B C.
Proof.
intros.
assert(HPO:=perp_out_acute).
assert(HBO:=acute_bet_obtuse).
assert(Col A B C').
apply bet_col in H1.
Col.
assert(Acute C' B C).
apply (HPO _ _ _ C').
apply out_trivial; auto.
apply perp_left_comm.
apply(perp_col _ A); Perp.
Col.
apply (HBO C').
intro.
subst B.
apply perp_distinct in H0.
tauto.
Between.
assumption.
Qed.

End L13_1.