proposition: Lemma nCol_not_Col : forall A B C, nCol A B C -> ~ Col A B C.
proof: Proof. unfold nCol. unfold Col. intuition. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel GeoCoq.Axioms.euclidean_axioms GeoCoq.Axioms.continuity_axioms GeoCoq.Meta_theory.Continuity.elementary_continuity_props GeoCoq.Meta_theory.Parallel_postulates.parallel_postulates