proposition: Lemma same_dir_refl : forall A B, Same_dir A B A B.
proof: Proof. intros. unfold Same_dir. induction (eq_dec_points A B). left. tauto. right. exists B. split. apply out_trivial. auto. apply eqv_refl. Qed.
imports: GeoCoq.Tarski_dev.Annexes.quadrilaterals_inter_dec