proposition: Lemma lower_dim_3' : {A : Tpoint & {B : Tpoint & {C : Tpoint & {D | ~ exists p, IncidentP A p /\ IncidentP B p /\ IncidentP C p /\ IncidentP D p}}}}.
proof: Proof. exists S1, S2, S3, S4. intros [p]; spliter. apply tarski_axioms.lower_dim_3, plane_cop with p; assumption. 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