proposition: Lemma same_dir_comm : forall A B C D, Same_dir A B C D -> Same_dir B A D C.
proof: Proof. intros. unfold Same_dir in *. induction H. left. auto. spliter. split; auto. right. ex_and H D'. assert(A <> B). intro. subst B. apply null_vector in H0. unfold Out in H. spliter. auto. assert(HH:=vector_construction B A D). ex_and HH C'. exists C'. split; trivial. unfold Out in *. spliter. unfold EqV in *. induction H4. repeat split. auto. intro. subst C'. apply eqv_sym in H2. apply null_vector in H2. subst B. tauto. left. induction H0; induction H2;try tauto. assert(Parallelogram C D' D C' \/ C = D' /\ B = A /\ C' = D /\ C = C'). apply(plg_pseudo_trans C D' B A C' D). apply plg_sym. apply plg_comm2. assumption. assumption. induction H5. assert(Parallelogram_flat C D' D C'). induction H5. apply False_ind. apply plgs_par_strict in H5. spliter. apply H5. exists D. apply bet_col in H4. split; Col. assumption. unfold Parallelogram_flat in H6. spliter. apply (col_cong2_bet1 D'). Col. Between. Cong. Cong. spliter. subst B. tauto. spliter. subst B. tauto. repeat split. auto. intro. subst C'. induction H2. induction H2. apply H2. Col. apply plgf_sym in H2. apply plgf_trivial_neq in H2. spliter. auto. spliter. auto. induction H0; induction H2;try tauto. induction(eq_dec_points C C'). subst C'. left. Between. assert(Parallelogram C D' D C' \/ C = D' /\ B = A /\ C' = D /\ C = C'). apply(plg_pseudo_trans C D' B A C' D). apply plg_sym. apply plg_comm2. assumption. assumption. induction H6. assert(Parallelogram_flat C D' D C'). induction H6. apply False_ind. apply plgs_par_strict in H6. spliter. apply H6. exists D. apply bet_col in H4. split; Col. assumption. right. assert(HH:= H7). unfold Parallelogram_flat in H7. spliter. apply plgf_bet in HH. induction HH. spliter. apply False_ind. apply H3. apply (between_equality _ _ D). apply between_symmetry. apply H13. assumption. induction H12. spliter. assert(D = D'). apply (between_equality _ _ C). Between. Between. subst D'. apply cong_identity in H10. contradiction. induction H12. spliter. eBetween. spliter. eBetween. spliter. subst B. tauto. spliter. subst B. tauto. Qed.
imports: GeoCoq.Tarski_dev.Annexes.quadrilaterals_inter_dec