proposition: Lemma plane_cop: forall A B C D p, IncidentP A p -> IncidentP B p -> IncidentP C p -> IncidentP D p -> Coplanar A B C D.
proof: Proof. unfold IncidentP. intros A B C D p HA HB HC HD. assert (HNCol := NCol p). apply ncols_coincide in HNCol. apply coplanar_pseudo_trans with (M1 p) (M2 p) (M3 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