proposition: Lemma same_dir_out : forall A B C, Same_dir A B A C -> Out A B C \/ A = B /\ A = C.
proof: Proof. intros. unfold Same_dir in H. induction H. right. auto. ex_and H D'. unfold EqV in H0. induction H0. induction H0. apply plgs_par_strict in H0. spliter. apply False_ind. apply H1. exists B. split; Col. apply plgf_permut in H0. apply plgf_sym in H0. apply plgf_trivial_neq in H0. spliter. subst D'. left. apply l6_6. assumption. spliter. subst D'. subst B. unfold Out in H. tauto. Qed.
imports: GeoCoq.Tarski_dev.Annexes.quadrilaterals_inter_dec