proposition: Lemma same_dir_null : forall A B C, Same_dir A A B C -> B = C.
proof: Proof. intros. unfold Same_dir in H. induction H. tauto. ex_and H D. apply null_vector in H0. subst D. unfold Out in H. tauto. Qed.
imports: GeoCoq.Tarski_dev.Annexes.quadrilaterals_inter_dec