proposition: Lemma not_out_bet : forall A B C, Col A B C -> ~ Out B A C -> Bet A B C.
proof: Proof. intros. unfold Out in H0. induction (eq_dec_points A B). subst. Between. induction (eq_dec_points B C). subst. Between. unfold Col in *. decompose [or] H;clear H. assumption. exfalso. apply H0. intuition. exfalso. apply H0. intuition. Qed.
imports: GeoCoq.Tarski_dev.Ch05_bet_le