proposition: Lemma same_dir_sym : forall A B C D, Same_dir A B C D -> Same_dir C D A B.
proof: Proof. intros. induction (eq_dec_points A B). subst B. apply same_dir_null in H. subst D. left. tauto. unfold Same_dir in *. induction H. left. tauto. ex_and H D'. right. assert(HH:=vector_construction C D A). ex_and HH B'. exists B'. split. unfold EqV in H1. unfold EqV in H2. unfold Out in *. spliter. induction H1; induction H2. repeat split. auto. intro. subst B'. induction H2. apply H2. Col. apply plgf_sym in H2. apply plgf_trivial_neq in H2. spliter. auto. induction H4. right. apply (plg_plg_bet C D _ _ D'). apply H2. apply H4. apply plg_sym. apply plg_comm2. assumption. left. apply (plg_plg_bet C D' _ _ D). apply plg_sym. apply plg_comm2. apply H1. apply H4. assumption. spliter. subst D. tauto. spliter. subst B. tauto. spliter. subst D. tauto. assumption. Qed.
imports: GeoCoq.Tarski_dev.Annexes.quadrilaterals_inter_dec