proposition: Lemma col_dec : forall A B C, Col A B C \/ ~ Col A B C.
proof: Proof. intros. unfold Col. elim (bet_dec A B C); intro; elim (bet_dec B C A); intro; elim (bet_dec C A B); intro; tauto. Qed.
imports: GeoCoq.Tarski_dev.Ch04_col