proposition: Lemma opp_not_same_dir : forall A B C D, A <> B -> Opp_dir A B C D -> ~ Same_dir A B C D.
proof: Proof. unfold Opp_dir. intros. intro. apply same_dir_to_null in H0. tauto. assumption. Qed.
imports: GeoCoq.Tarski_dev.Annexes.quadrilaterals_inter_dec