proposition: Lemma not_bet_and_out : forall A B C, ~ (Bet A B C /\ Out B A C).
proof: Proof. intros. intro. spliter. unfold Out in H0. spliter. induction H2. assert ( A = B). eapply between_equality. apply H. assumption. contradiction. assert(C = B). eapply between_equality. apply between_symmetry. apply H. assumption. contradiction. Qed.
imports: GeoCoq.Tarski_dev.Ch05_bet_le