proposition: Lemma bet_dec : forall A B C, Bet A B C \/ ~ Bet A B C.
proof: Proof. intros. elim (segment_construction A B B C); intros C' HC'. spliter. elim (eq_dec_points C C'); intro. subst; tauto. elim (eq_dec_points A B);intro. left; subst; Between. right; intro; apply H1; apply between_cong_3 with A B; Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch04_col