proposition: Lemma bet_dec_eq_dec : (forall A B C, Bet A B C \/ ~ Bet A B C) -> (forall A B:Tpoint, A=B \/ A<>B).
proof: Proof. intros. induction (H A B A). left; apply between_identity; assumption. right; intro; subst; apply H0; apply between_trivial. Qed.
imports: GeoCoq.Tarski_dev.Ch05_bet_le GeoCoq.Utils.all_equiv