proposition: Lemma lower_dim : exists A, exists B, exists C, ~ (Bet A B C \/ Bet B C A \/ Bet C A B).
proof: Proof. exists P0. exists P1. exists P2. unfold Bet. intro. intuition discriminate. Qed.
imports: GeoCoq.Axioms.tarski_axioms