proposition: Lemma Col_nCol_False : forall A B C, nCol A B C -> Col A B C -> False.
proof: Proof. unfold Col, nCol;intuition. Qed.
imports: Classical GeoCoq.Elements.OriginalProofs.euclidean_defs GeoCoq.Elements.OriginalProofs.general_tactics