Library Ch13_1

Require Export project.

Section L13.

Context `{MT:Tarski_2D_euclidean}.
Context `{EqDec:EqDecidability Tpoint}.
Context `{InterDec:InterDecidability Tpoint Col}.

Lemma triangle_mid_par : ∀ A B C P Q, ¬Col A B C → is_midpoint P B C → is_midpoint Q A C → Par_strict A B Q P.
Proof.
intros.
apply not_col_distincts in H.
spliter.
assert(∃ D : Tpoint, Parallelogram C A B D).
apply(plg_existence C A B); auto.
ex_and H5 D.

assert(Parallelogram_strict C A B D).
induction H6.
assumption.
unfold Parallelogram_flat in H5.
spliter.
apply False_ind.
apply H.
ColR.
assert(HH:= midpoint_existence B D).
ex_and HH R.

assert(Par Q R C D ∧ is_midpoint P Q R ∧ Cong C D Q R).

apply(half_plgs C A B D Q R P); Midpoint.
spliter.
assert(Par Q P C D).
eapply (par_col_par_2 _ R).
intro.
subst Q.
apply is_midpoint_id in H9.
subst R.
apply par_distincts in H8.
tauto.
unfold is_midpoint in H9.
spliter.
apply bet_col in H9.
Col.
assumption.
assert(Par Q P A B).
eapply par_trans.
apply H11.
apply plg_par; auto.
apply par_symmetry in H12.
induction H12.
assumption.
spliter.
assert(Col A B P).
ColR.
unfold is_midpoint in H0.
spliter.
apply bet_col in H0.

assert(B ≠ P).
intro.
subst P.
apply cong_symmetry in H17.
apply cong_identity in H17.
contradiction.
apply False_ind.
apply H.
ColR.
Qed.

Lemma l13_1 : ∀ A B C P Q R, ¬Col A B C → is_midpoint P B C → is_midpoint Q A C → is_midpoint R A B
                                       → ∃ X, ∃ Y, Perp_in R X Y A B ∧ Perp X Y P Q.
intros.
apply not_col_distincts in H.
spliter.
∃ R.
assert(Col A B R).
unfold is_midpoint in H2.
spliter.
apply bet_col in H2.
Col.

assert(HH:=l10_15 A B R C H6 H).
ex_and HH T.
∃ T.
split.
assert(A ≠ R).
intro.
subst R.
apply is_midpoint_id in H2.
contradiction.
assert(Perp A R T R).
eapply (perp_col _ B); auto.
apply perp_left_comm in H10.
apply perp_perp_in in H10.

eapply (perp_in_col_perp_in _ _ _ R); Col.
apply perp_in_comm.
apply perp_in_sym.
assumption.
apply perp_sym.
eapply par_perp_perp.
2: apply perp_right_comm.
2: apply H7.
left.
apply par_strict_right_comm.
apply (triangle_mid_par _ _ C); auto.
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.
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 ∧ two_sides B P A C.
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 ∨ is_midpoint B A C).
eapply l7_20; Cong.
induction H9.
contradiction.
unfold two_sides.
repeat split.
auto.
intro.
apply H6.
Col.
intro.
apply H6.
ColR.
∃ B.
unfold is_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_in 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_in 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 ∨ is_midpoint T A C).
apply l7_20;
Col.
induction H17.
contradiction.
unfold two_sides.
repeat split; Col.

assert(¬ Col T A B).
apply perp_not_col.
apply perp_in_perp 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 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 os_out_os : ∀ A B C D C' P , Col A B P → one_side A B C D → out P C C' → one_side A B C' D.
intros.

assert(A ≠ B ∧ ¬ Col C A B).
unfold one_side in H0.
ex_and H0 T.
unfold two_sides in H0.
tauto.
spliter.

prolong C P T C P.

assert(P ≠ T).
intro.
subst T.
apply cong_symmetry in H5.
apply cong_identity in H5.
subst P.
apply H3.
Col.

assert(two_sides A B C T).
unfold two_sides.
repeat split; Col.

intro.
apply H3.
assert(Col P T A).
ColR.
assert(Col P T B).
ColR.
apply bet_col in H4.
apply (col3 P T); Col.
∃ P.
split; Col.

assert(two_sides A B T C').
apply bet_col in H4.
eapply (out_out_two_sides _ _ T C _ _ P); Col.
apply l9_2.
assumption.
apply out_trivial.
auto.

assert(one_side A B C C').
eapply l9_8_1.
apply H7.
apply l9_2.
assumption.
eapply one_side_transitivity.
apply one_side_symmetry.
apply H9.
assumption.
Qed.

Lemma ts_ts_os : ∀ A B C D, two_sides A B C D → two_sides C D A B → one_side A C B D.
intros.
unfold two_sides in ×.
spliter.
ex_and H6 T1.
ex_and H3 T.
assert(T1 = T).
apply bet_col in H7.
apply bet_col in H8.
apply (inter_unicity A B C D); Col.
subst T1.

prolong A T A' A T.
prolong C T C' C T.
assert(Parallelogram A C A' C').
eapply (mid_plg _ _ _ _ T).
left.
intro.
subst A'.
apply between_identity in H9.
subst T.
contradiction.
unfold is_midpoint; split; Cong.
unfold is_midpoint; split; Cong.

assert(A ≠ A').
intro.
subst A'.
apply between_identity in H9.
subst T.
contradiction.

assert(C ≠ C').
intro.
subst C'.
apply between_identity in H11.
subst T.
contradiction.

assert(Parallelogram_strict A C A' C').
induction H13.
assumption.
unfold Parallelogram_flat in H13.
spliter.
apply False_ind.

apply H4.
apply bet_col in H7.
apply bet_col in H8.
apply bet_col in H9.
apply bet_col in H11.
assert(Col A C T).
ColR.
assert(Col A T B).
ColR.
assert(A ≠ T).
intro.
subst T.
apply cong_identity in H10.
contradiction.
ColR.

apply plgs_par_strict in H16.
spliter.

assert(one_side A C A' C').
eapply l12_6.
assumption.

assert(out A B A').
repeat split; auto.
eapply (l5_1 _ T); Between.
intro.
subst T.
apply cong_identity in H10.
subst A'.
tauto.

assert(out C C' D).
repeat split; auto.
eapply (l5_1 _ T); Between.
intro.
subst T.
apply cong_identity in H12.
subst C'.
tauto.

assert(one_side A C A' B).
eapply (os_out_os _ _ B _ _ A); Col.
apply one_side_reflexivity.
intro.
apply H4.
Col.

assert(one_side A C C' D).
apply invert_one_side.
apply one_side_symmetry.
eapply (os_out_os _ _ C' _ _ C); Col.
apply one_side_reflexivity.
intro.
apply H1.
apply out_col in H20.
ColR.

eapply one_side_transitivity.
apply one_side_symmetry.
apply H21.
eapply one_side_transitivity.
apply H18.
assumption.
Qed.

Lemma ts_per_per_ts : ∀ A B C D, two_sides A B C D → Per B C A → Per B D A → two_sides C D A B.
intros.
unfold two_sides in H.
spliter.
ex_and H4 P.

assert(C ≠ D).
intro.
subst D.
apply between_identity in H5.
subst P.
contradiction.

assert(B ≠ C).
intro.
subst C.
apply H2.
Col.

assert(B ≠ D).
intro.
subst D.
apply H3.
Col.

assert( A ≠ C).
intro.
subst C.
apply H2.
Col.

assert( A ≠ D).
intro.
subst D.
apply H3.
Col.

assert(Perp B C C A).
apply per_perp_in in H0; auto.
apply perp_in_comm in H0.
apply perp_in_perp in H0.
induction H0.
apply perp_comm.
assumption.
apply perp_not_eq_1 in H0.
tauto.

assert(Perp B D D A).
apply per_perp_in in H1; auto.
apply perp_in_comm in H1.
apply perp_in_perp in H1.
induction H1.
apply perp_comm.
assumption.
apply perp_not_eq_1 in H1.
tauto.

assert(¬ Col A C D).
intro.
assert(Par B C B D).
eapply l12_9.
apply I.
apply H11.
apply perp_sym.
apply perp_comm.
eapply (perp_col _ D); Col.
Perp.
induction H14.
apply H14.
∃ B.
split; Col.
spliter.
apply H2.
eapply (col_transitivity_1 _ D); Col.

assert(¬ Col B C D).
intro.

assert(Par A C A D).
eapply l12_9.
apply I.
apply perp_comm.
apply perp_sym.
apply H11.
apply perp_sym.
apply perp_comm.
eapply (perp_col _ D); Col.
induction H15.
apply H15.
∃ A.
split; Col.
spliter.
apply H2.
eapply (col_transitivity_1 _ D); Col.

unfold two_sides.
repeat split; auto.

∃ P.
split.
apply bet_col in H5.
Col.

assert(∃ X : Tpoint, Col A B X ∧ Perp A B C X).
apply(l8_18_existence A B C).
intro.
apply H2.
Col.

assert(∃ X : Tpoint, Col A B X ∧ Perp A B D X).
apply(l8_18_existence A B D).
intro.
apply H3.
Col.

ex_and H15 PC.
ex_and H16 PD.

assert(Perp_in PC A B C PC).
apply(l8_14_2_1b_bis A B C PC PC H17); Col.

assert(Perp_in PD A B D PD).
apply(l8_14_2_1b_bis A B D PD PD H18); Col.

assert(Bet A PC B ∧ Distincts A PC B).
apply(l11_47 A B C PC).
apply l8_2.
assumption.
Perp.

assert(Bet A PD B ∧ Distincts A PD B).
apply(l11_47 A B D PD).
apply l8_2.
assumption.
Perp.

spliter.

assert(Bet PC P PD).

eapply (projp_preserves_bet C P D).
assumption.
unfold projp.
split.
apply H.
left.
split; Col.
unfold projp.
split.
assumption.
right.
split; Col.
unfold projp.
split.
assumption.
left.
split; Col.

induction(eq_dec_points PC PD).
subst PD.
apply between_identity in H25.
subst PC.
assumption.

assert(Bet A PC PD ∨ Bet A PD PC).
eapply l5_3.
apply H21.
assumption.
induction H27.
eBetween.
apply between_exchange4 with PC.
apply between_exchange2 with PD; Between.
Between.
Qed.

Lemma lea_in_angle : ∀ A B C A' B' C' P, lea A' B' C' A B C → Conga A B P A' B' C' → one_side A B C P
                                               → InAngle P A B C.
intros.

unfold lea in H.
ex_and H T.
eapply conga_preserves_in_angle.
3: apply H.
apply conga_refl.
assert(HH0:=H0).
unfold Conga in HH0.
spliter.
clear H6.
repeat split; auto.
intro.
subst C.
unfold one_side in H1.
ex_and H1 X.
unfold two_sides in H1.
spliter.
apply H4.
Col.
eapply conga_trans; apply conga_sym.
apply H2.
apply H0.
apply one_side_symmetry.
assumption.
Qed.

Lemma l13_2_1 : ∀ A B C D E, two_sides 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.
intros.
intros.
assert(HH:= H).
unfold two_sides in HH.
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(two_sides C D A B).
apply ts_per_per_ts; auto.
unfold two_sides in H17.
spliter.
ex_and H20 T1.
ex_and H8 T.
assert(T = T1).
apply bet_col in H21.
apply bet_col in H22.
apply (inter_unicity A B C D); Col.
subst T1.
assert(T = E).
apply (inter_unicity 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 inangle_one_side : ∀ A B C P Q , ¬ Col A B C → ¬ Col A B P → ¬ Col A B Q
                                            → InAngle P A B C → InAngle Q A B C
                                            → one_side A B P Q.
intros.
unfold InAngle in ×.
spliter.
ex_and H9 P'.
ex_and H6 Q'.
induction H10.
subst P'.
apply bet_col in H9.
contradiction.
induction H11.
subst Q'.
apply bet_col in H6.
contradiction.

assert(one_side A B P' Q').
prolong P' A T A C.
unfold one_side.
∃ T.
unfold two_sides.

assert(A ≠ P').
intro.
subst P'.
apply out_col in H10.
apply H0.
Col.

repeat split; auto.

intro.
apply H0.

assert(P' ≠ B).
unfold out in H10.
spliter.
assumption.
apply out_col in H10.
ColR.

intro.

induction(eq_dec_points A T).
subst T.
apply cong_symmetry in H13.
apply cong_identity in H13.
subst C.
apply H.
Col.

apply H.
apply bet_col in H9.
apply bet_col in H12.
assert(Col T A C).
ColR.

eapply (col_transitivity_1 _ T); Col.
∃ A.
split; Col.

intro.
apply H1.

assert(Q' ≠ B).
unfold out in H11.
spliter.
assumption.
apply out_col in H11.
ColR.

intro.

induction(eq_dec_points A T).
subst T.
apply cong_symmetry in H13.
apply cong_identity in H13.
subst C.
apply H.
Col.

apply H.
apply bet_col in H9.
apply bet_col in H12.
assert(Col T A C).
ColR.

eapply (col_transitivity_1 _ T); Col.
∃ A.
split; Col.

assert(Bet A P' Q' ∨ Bet A Q' P').
eapply l5_3.
apply H9.
assumption.
induction H15.
eapply (outer_transitivity_between2 _ P');
Between.
eapply (between_exchange3 P'); Between.

assert(one_side A B P P').
eapply (out_one_side_1 _ _ _ _ B); Col.
apply l6_6.
auto.

assert(one_side A B Q Q').
eapply (out_one_side_1 _ _ _ _ B); Col.
apply l6_6.
auto.

eapply one_side_transitivity.
apply H13.
apply one_side_symmetry.
eapply one_side_transitivity.
apply H14.
apply one_side_symmetry.
assumption.
Qed.

Lemma inangle_one_side2 : ∀ A B C P Q , ¬ Col A B C → ¬ Col A B P → ¬ Col A B Q
                                              → ¬ Col C B P → ¬ Col C B Q
                                            → InAngle P A B C → InAngle Q A B C
                                            → one_side A B P Q ∧ one_side C B P Q.
intros.
split.
apply (inangle_one_side _ _ C); Col.
apply (inangle_one_side _ _ A); Col.
apply l11_24.
auto.
apply l11_24.
auto.
Qed.

Lemma l13_2 : ∀ A B C D E, two_sides 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.
intros.
assert(HH:= H).
unfold two_sides in HH.
spliter.

assert(C ≠ D).
intro.
subst D.
assert(one_side A B C C).
apply one_side_reflexivity.
assumption.
apply l9_9 in H.
contradiction.

assert(∃ C', Conga B A C D A C' ∧ one_side 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 two_sides in HH1.
spliter.
ex_and H7 T.
ex_and H17 T2.
assert(T = T2).
eapply (inter_unicity A B C D).
Col.
apply bet_col in H18.
Col.
apply bet_col in H19.
Col.
Col.
intro.
apply H5.
Col.
assumption.
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.
apply H21.
apply conga_sym.
assumption.

assert(HH1:=ts_per_per_ts A B C D H H0 H1).
assert(one_side 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 ∨ two_sides C A B D).
apply(l11_22_aux C A B D).
apply conga_comm.
assumption.
induction H31.
apply out_col in H31.
apply H6.
Col.
assert(one_side 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 (inter_unicity 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 one_side.
∃ C.
split.

unfold two_sides.
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(two_sides A E'' T C).
unfold two_sides.
repeat split.
auto.
intro.
apply H29.
apply (inter_unicity 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(two_sides A B C E'').
unfold two_sides.
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(one_side A B D E'').
eapply l9_8_1.
apply l9_2.
apply H.
apply l9_2.
assumption.

assert(two_sides A E'' T D).
unfold two_sides.
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(two_sides A B D E'').
unfold two_sides.
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(is_midpoint D B D').
unfold is_midpoint.
split; Cong.
assert(D' = D'').
eapply symmetric_point_unicity.
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(is_midpoint C B C').
unfold is_midpoint.
split; Cong.
assert(C' = C'').
eapply symmetric_point_unicity.
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(one_side 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(one_side C A B D).
apply in_angle_one_side.
intro.
apply H15.
Col.
intro.
apply H5.
Col.
apply l11_24.
auto.

assert(two_sides C A B C').
unfold two_sides.
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(one_side C A B E'').
eapply one_side_transitivity.
apply H44.
auto.

assert(one_side D A C E'').

eapply out_out_one_side.
apply one_side_reflexivity.
intro.
apply H15.
Col.
unfold out.
repeat split; auto.

assert(one_side D A B C).
apply in_angle_one_side.
intro.
apply H15.
Col.
intro.
apply H6.
Col.
auto.

assert(two_sides D A B D').
unfold two_sides.
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(one_side 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 is_midpoint.
split.
Between.
Cong.
unfold is_midpoint.
split.
Between.
Cong.

assert(two_sides A E'' C D).

unfold two_sides.
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(two_sides B A C D).
apply in_angle_two_sides.
intro.
apply H5.
Col.
intro.
apply H6.
Col.
apply l11_24.
assumption.
assert (one_side A B C C').
apply (out_one_side_1 _ _ _ _ B); Col.
unfold out.
repeat split; auto.

intro.
subst C.
apply H5.
Col.

assert (one_side 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(two_sides A B C' D).
eapply l9_8_2.
apply H49.
auto.

assert(two_sides 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 l11_22_aux in H43.

induction H43.

assert(one_side 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.
eCong.
apply conga_left_comm.
assumption.

assert(Perp C D A E'').
eapply par_perp_perp.
left.
apply H47.
assumption.
assert(Col A E E'').
eapply perp_perp_col.
apply H3.
apply perp_sym.
assumption.

assert(E'' = E).
eapply (inter_unicity C D A E).
apply bet_col in H25.
Col.
apply out_col in H26.
Col.
Col.
Col.
intro.
apply H15.
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 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).
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.

assert(projp P U O U).
unfold projp.
split.
auto.
left.
split.
Col.
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_right_comm.
assumption.

assert(projp Q V O U).
unfold projp.
split.
auto.
left.
split.
Col.
apply per_perp_in in H4; auto.
apply perp_in_perp in H4.
induction H4.
apply perp_not_eq_1 in H4.
tauto.
eapply perp_col.
auto.

apply perp_sym.
apply perp_right_comm.
apply H4.
Col.

assert(projp O O O U).
unfold projp.
split.
auto.
right; Col.

split.
intro.
unfold out.
repeat split; auto.
unfold out in H10.
spliter.
induction H12.

left.
apply (projp_preserves_bet O P Q _ _ _ O U); auto.

right.
apply (projp_preserves_bet O Q P _ _ _ O U); auto.

intro.

assert(HH:= perp_vector U O H).
ex_and HH X.

ex_and H11 Y.

assert(P ≠ O).
intro.
subst P.
apply perBAB in H3.
subst U.
tauto.

assert(Q ≠ O).
intro.
subst Q.
apply perBAB in H4.
subst V.
tauto.

assert(X ≠ Y).
apply perp_not_eq_2 in H12.
auto.

assert(¬ Par O P X Y ).
intro.

assert(Perp O P U O).
apply(par_perp_perp X Y O P U O).
apply par_symmetry.
assumption.
Perp.
assert(Per P O U).
eapply perp_in_per.
apply perp_in_sym.
apply perp_perp_in.
Perp.
apply H.
eapply (l8_7 P); auto.

assert(project O O O P X Y).
unfold project.
split.
auto.
split.
auto.
split.
auto.
split.
Col.
right.
auto.

assert(project U P O P X Y).
split.
auto.
split.
auto.
split.
auto.
split.
Col.
left.
apply per_perp_in in H3; auto.
apply perp_in_sym in H3.
apply perp_in_perp in H3.
induction H3.
apply (l12_9 _ _ _ _ O U).
apply I.
Perp.
Perp.
apply perp_not_eq_1 in H3.
tauto.

assert(project V Q O P X Y).
split.
auto.
split.
auto.
split.
auto.
split.
Col.
left.
apply per_perp_in in H4; auto.
apply perp_in_sym in H4.
apply perp_in_perp in H4.
induction H4.
apply (l12_9 _ _ _ _ O V).
apply I.
eauto with perp.
eauto with perp.
apply perp_not_eq_1 in H4.
tauto.

repeat split;
auto.

unfold out in H10.
spliter.
induction H20.
left.
eapply project_preserves_bet.
apply H20.
apply H16.
assumption.
assumption.

right.
eapply project_preserves_bet.
apply H20.
apply H16.
assumption.
assumption.
Qed.

Definition Perp2 := fun A B C D P ⇒ ∃ X, ∃ Y, Col P X Y ∧ Perp X Y A B ∧ Perp X Y C D.

Lemma perp2_refl : ∀ A B P, A ≠ B → Perp2 A B A B P.
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.
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.
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.
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.
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.
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.
apply I.
∃ 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.
intros.
unfold Perp2 in H.
ex_and H X.
ex_and H0 Y.
eapply (l12_9 _ _ _ _ X Y).
apply I.
Perp.
Perp.
Qed.

Lemma perp2_preserves_bet : ∀ 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(O ≠ A').
intro.
subst A'.
apply H1.
Col.
assert( A ≠ A').
intro.
subst A'.
apply H1.
Col.

assert(¬ Par O A' A A').
intro.
unfold Par in H5.
induction H5.
unfold Par_strict in H5.
spliter.
apply H8.
∃ A'.
split; Col.
spliter.
contradiction.

eapply (project_preserves_bet O A' A A' O A B O A' B');
auto;
unfold project;
repeat split; Col.
left.
apply par_reflexivity.
auto.
left.
apply perp2_par in H2.
apply par_symmetry.
auto.
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_in P O P A B ∧ Perp_in 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 X Y A B H2).
ex_and HH P.
assert(HH:= perp_inter_perp_in 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_in 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_in 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 perp_vector1 : ∀ A B P, A ≠ B → ∃ Q, Perp A B P Q.
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.
∃ Q.
Perp.

assert(HH:=l8_18_existence A B P H0).
ex_and HH Q.
∃ Q.
auto.
Qed.

Lemma par_perp2 : ∀ A B C D P, Par A B C D → Perp2 A B C D P.
intros.
apply par_distincts in H.
spliter.
unfold Perp2.
assert(HH:= perp_vector1 A B P H0).
ex_and HH Q.
∃ P.
∃ Q.
repeat split.
Col.
Perp.
apply perp_sym.
apply (par_perp_perp A B); auto.
Qed.

End L13.