proposition: Lemma same_dir_out1 : forall A B C, Same_dir A B B C -> Out A B C \/ A = B /\ A = C.
proof: Proof. intros. unfold Same_dir in H. induction H. right. spliter. subst B. tauto. 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. unfold Parallelogram_flat in H0. spliter. assert(A = D' \/ Midpoint B A D'). apply l7_20. Col. Cong. induction H5. subst D'. tauto. left. unfold Midpoint in H5. spliter. unfold Out. repeat split. intro. subst B. apply cong_symmetry in H6. apply cong_identity in H6. induction H4; tauto. intro. subst C. unfold Out in H. spliter. induction H8. apply H. apply (between_equality _ _ D'); Between. apply H7. apply (between_equality _ _ A); Between. induction H. spliter. induction H8. left. apply (between_inner_transitivity _ _ _ D'). apply H5. apply H8. left. apply (outer_transitivity_between _ _ D'). apply H5. auto. auto. spliter. subst B. subst D'. unfold Out in H. tauto. Qed.
imports: GeoCoq.Tarski_dev.Annexes.quadrilaterals_inter_dec