proposition: Lemma par_ts_same_dir : forall A B C D, Par_strict A B C D -> (exists M, Bet A M D /\ Bet B M C) -> Same_dir A B C D.
proof: Proof. intros. ex_and H0 M. unfold Same_dir. right. assert(HH:=vector_construction A B C). ex_and HH D'. exists D'. split; trivial. assert(A <> B /\ C <> D). apply par_strict_distinct in H. spliter. split; auto. spliter. assert(A <> M). intro. subst M. apply False_ind. apply H. exists C. apply bet_col in H1. split; Col. induction (eq_dec_points B D'). subst D'. assert( A = C). apply (vector_uniqueness B). apply eqv_comm. apply H2. subst C. assert(Bet A D B \/ Bet A B D). apply (l5_1 _ M). apply H5. auto. Between. unfold Out. repeat split; auto. induction H2. assert(Par A B D' C). apply plg_par in H2; auto. spliter. auto. assert(Col C D D'). apply col_permutation_1. apply (parallel_uniqueness A B _ _ C _ C). left. apply H. Col. apply par_right_comm. apply H7. Col. induction H2. assert(HH := (plgs_two_sides A B D' C H2)). spliter. assert(TS B C A D). unfold TS. unfold TS in H10. spliter. repeat split; auto. intro. apply H11. ColR. exists M. split. apply bet_col in H1. Col. auto. assert(OS B C D D'). apply (l9_8_1 _ _ _ _ A). apply l9_2. apply H11. apply l9_2. auto. apply (one_side_col_out _ B). Col. apply invert_one_side. apply H12. apply False_ind. unfold Parallelogram_flat in H2. spliter. apply H. exists C. split; Col. spliter. subst D'. subst B. tauto. Qed.
imports: GeoCoq.Tarski_dev.Annexes.quadrilaterals_inter_dec