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