proposition: Lemma Col_or_nCol : forall A B C, Col A B C \/ nCol A B C.
proof: Proof. unfold nCol, Col. intros. tauto. Qed.
imports: Classical GeoCoq.Elements.OriginalProofs.euclidean_defs GeoCoq.Elements.OriginalProofs.general_tactics