proposition: Lemma exists_not_incident : forall A B : Tpoint, forall HH : A <> B , exists C, ~ IncidentL C (Lin A B HH).
proof: Proof. intros. unfold IncidentL. assert(HC:=not_col_exists A B HH). ex_and HC C. exists C. intro. apply H. simpl in H0. Col. Qed.
imports: Morphisms GeoCoq.Axioms.hilbert_axioms GeoCoq.Axioms.parallel_postulates GeoCoq.Meta_theory.Parallel_postulates.tarski_playfair GeoCoq.Meta_theory.Parallel_postulates.SPP_ID GeoCoq.Meta_theory.Dimension_axioms.upper_dim_3 GeoCoq.Meta_theory.Parallel_postulates.parallel_postulates GeoCoq.Utils.triples