proposition: Lemma same_or_opp_dir : forall A B C D, Par A B C D -> Same_dir A B C D \/ Opp_dir A B C D.
proof: Proof. intros. induction (same_dir_dec A B C D). left. assumption. right. unfold Opp_dir. unfold Same_dir. right. assert(HH:= vector_construction A B D). ex_and HH C'. exists C'. split; trivial. unfold EqV in H1. induction (eq_dec_points B C'). subst C'. induction H1. induction H1. apply False_ind. apply plgs_permut in H1. apply plgs_sym in H1. apply H1. Col. apply plgf_permut in H1. apply plgf_trivial_neq in H1. spliter. subst D. induction H. apply False_ind. apply H. exists A. split; Col. spliter. induction H4. unfold Out. repeat split; auto. left. Between. induction H4. unfold Out. repeat split; auto. apply False_ind. apply H0. apply same_dir_sym. apply bet_same_dir2; auto. unfold Out. repeat split. auto. auto. right. assumption. spliter. subst A. subst D. apply par_distinct in H. tauto. induction H1. assert(Col C' C D /\ Col D C D). apply plg_par in H1. spliter. apply(parallel_uniqueness A B C D C' D D); Col. apply par_distinct in H. tauto. assumption. spliter. clear H4. unfold Out. repeat split. apply par_distinct in H. tauto. intro. subst C'. induction H1. apply H1. Col. apply plgf_sym in H1. apply plgf_trivial_neq in H1. spliter. apply par_distinct in H. tauto. induction H3. left. Between. induction H3. apply False_ind. assert(Same_dir A B D C'). apply plg_opp_dir. assumption. assert(Same_dir C D D C'). apply bet_same_dir2. apply par_distinct in H. spliter. auto. intro. subst C'. induction H1. apply H1. Col. apply plgf_sym in H1. apply plgf_trivial_neq in H1. spliter. apply par_distinct in H. tauto. assumption. apply False_ind. apply H0. apply (same_dir_trans _ _ D C'). apply H4. apply same_dir_sym. auto. right. assumption. apply par_distinct in H. tauto. Qed.
imports: GeoCoq.Tarski_dev.Annexes.quadrilaterals_inter_dec