proposition: Lemma not_bet_distincts : forall A B C, ~ Bet A B C -> A <> B /\ B <> C.
proof: Proof. intros A B C HNBet. repeat split; intro; subst B; apply HNBet. apply between_trivial2. apply between_trivial. Qed.
imports: GeoCoq.Tarski_dev.Ch02_cong