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