proposition: Lemma bet_same_dir1 : forall A B C, A <> B -> B <> C -> Bet A B C -> Same_dir A B A C.
proof: Proof. intros. unfold Same_dir. right. exists B. split. unfold Out. repeat split. intro. subst C. apply between_identity in H1. tauto. auto. right. assumption. apply eqv_refl. Qed.
imports: GeoCoq.Tarski_dev.Annexes.quadrilaterals_inter_dec