proposition: Lemma opp_dir_to_null : forall A B C D, Opp_dir A B C D -> Opp_dir A B D C -> A = B /\ C = D.
proof: Proof. unfold Opp_dir. intros. apply same_dir_to_null; auto. Qed.
imports: GeoCoq.Tarski_dev.Annexes.quadrilaterals_inter_dec