proposition: Lemma nCol_notCol : forall A B C, ~ Col A B C -> nCol A B C.
proof: Proof. intros. unfold nCol, Col, neq in *. intuition. Qed.
imports: Classical GeoCoq.Elements.OriginalProofs.euclidean_defs GeoCoq.Elements.OriginalProofs.general_tactics