proposition: Lemma same_dir_ts : forall A B C D, Same_dir A B C D -> exists M, Bet A M D /\ Bet B M C.
proof: Proof. intros. induction H. spliter. subst B. subst D. exists A. split; Between. ex_and H D'. induction H0. assert(exists M : Tpoint, Midpoint M A D' /\ Midpoint M B C). apply plg_mid. assumption. ex_and H1 M. unfold Midpoint in *. spliter. induction H0. assert(HH:=plgs_two_sides A B D' C H0). spliter. assert(B <> C). intro. subst C. unfold TS in H6. spliter. Col. assert(~ Col B C D'). intro. unfold TS in H6. spliter. apply H9. Col. assert(OS B C D' D). apply l6_6 in H. apply (out_one_side_1 _ _ _ _ C); Col. assert(TS B C A D). apply l9_2. apply (l9_8_2 _ _ D'). apply l9_2. apply H6. auto. assert(~ Col A B C). induction H10. assumption. induction H10. spliter. ex_and H13 T. assert(OS A B D' C /\ OS D' C A B). apply(plgs_one_side A B D' C). assumption. spliter. assert(~Col A B C). assumption. assert(Par_strict A B D' C /\ Par_strict A C B D'). apply(plgs_par_strict A B D' C). assumption. spliter. assert(A <> B). intro. subst B. apply H18. exists C. split; Col. assert(Par C D A B). apply (par_col_par_2 _ D'). unfold Out in H. spliter. auto. apply out_col in H. Col. apply par_symmetry. apply par_right_comm. left. assumption. assert(Par_strict A B C D). apply par_strict_symmetry. induction H21. auto. spliter. apply False_ind. apply H17. Col. induction(col_dec A B T). apply False_ind. assert(B = T). apply (l6_21 A B C B); Col. subst T. apply H22. exists D. apply bet_col in H14. split; Col. induction(col_dec C D T). apply False_ind. assert(C = T). apply (l6_21 C D B C); Col. subst T. apply H22. exists A. apply bet_col in H14. split; Col. induction H13. assert(OS B A T D). apply (out_one_side_1 _ _ _ _ A); Col. unfold Out. repeat split. intro. subst T. apply H23. Col. intro. subst D. apply H22. exists A. split; Col. left. auto. assert(OS B A T C). apply (one_side_transitivity _ _ _ D). apply H25. apply (par_strict_one_side _ _ _ C). apply par_strict_comm. apply H22. Col. assert(TS B A T C). unfold TS. repeat split; Col. exists B. split; Col. apply l9_9 in H26. contradiction. assumption. induction H13. assert(OS C D T A). apply (out_one_side_1 _ _ _ _ D). auto. Col. unfold Out. repeat split. intro. subst T. apply H24. Col. intro. subst D. apply H22. exists A. split; Col. left. Between. assert(OS C D T B). apply (one_side_transitivity _ _ _ A). apply H25. apply (par_strict_one_side _ _ _ B). apply par_strict_symmetry. apply H22. Col. assert(TS C D T B). unfold TS. repeat split. unfold Out in H. spliter. auto. intro. apply H24. Col. intro. apply H22. exists B. split; Col. exists C. split. Col. Between. apply l9_9 in H27. contradiction. exists T. split; Between. assert(HH:= plgf_bet A B C D' H0). induction (eq_dec_points A D'). subst D'. unfold Parallelogram_flat in H0. spliter. assert(B = C \/ Midpoint A B C). apply l7_20. Col. Cong. induction H9. subst C. tauto. exists A. split. Between. apply midpoint_bet. assumption. induction (eq_dec_points B C). subst C. unfold Parallelogram_flat in H0. spliter. assert(A = D' \/ Midpoint B A D'). apply l7_20. Col. Cong. induction H10. subst D'. tauto. exists B. split. induction H10. unfold Out in H. spliter. induction H13. apply (between_inner_transitivity _ _ _ D'). apply H10. auto. apply (outer_transitivity_between _ _ D'). apply H10. auto. auto. Between. induction HH. spliter. exists A. split. Between. apply (outer_transitivity_between _ _ D'); Between. induction H7. spliter. exists A. split. Between. apply between_symmetry. apply (outer_transitivity_between _ _ D'); Between. induction H7. spliter. exists C. split. induction H. spliter. induction H10. assert(Bet C B D \/ Bet C D B). apply (l5_3 _ _ _ D'); auto. induction H11. apply (outer_transitivity_between _ _ B); Between. apply (between_inner_transitivity _ _ _ B). apply H7. auto. apply (outer_transitivity_between _ _ B); Between. apply (between_exchange4 _ _ D'). apply H8. auto. Between. spliter. exists B. split. unfold Out in H. spliter. induction H10. assert(Bet B C D). apply (between_inner_transitivity _ _ _ D'). apply H8. assumption. eBetween. apply (outer_transitivity_between _ _ C). apply H7. apply (outer_transitivity_between _ _ D' ). apply H8. auto. auto. auto. Between. spliter. subst B. subst D'. exists A. split; Between. Qed.
imports: GeoCoq.Tarski_dev.Annexes.quadrilaterals_inter_dec