proposition: Lemma or_bet_out : forall A B C, Bet A B C \/ Out B A C \/ ~Col A B C.
proof: Proof. intros. destruct (col_dec A B C); auto. destruct (out_dec B A C); auto. left; apply not_out_bet; trivial. Qed.
imports: GeoCoq.Tarski_dev.Ch05_bet_le