proposition: Lemma same_dir_id : forall A B, Same_dir A B B A -> A = B.
proof: Proof. intros. unfold Same_dir in H. induction H. tauto. ex_and H C. apply eqv_mid in H0. unfold Midpoint in H0. unfold Out in H. spliter. induction H3. apply (between_equality _ _ C). apply H0. assumption. apply False_ind. apply H2. apply (between_equality _ _ A). Between. assumption. Qed.
imports: GeoCoq.Tarski_dev.Annexes.quadrilaterals_inter_dec