proposition: Lemma cop_plane : forall A B C D, Coplanar A B C D -> exists p, IncidentP A p /\ IncidentP B p /\ IncidentP C p /\ IncidentP D p.
proof: Proof. intros A B C D HCop. destruct (eq_dec_points A B) as [|HAB]; [destruct (eq_dec_points A C); [destruct (eq_dec_points A D)|]|]. - destruct (another_point D) as [E]. destruct (cop_plane_aux D E E E) as [p []]; Cop. subst; exists p; repeat split; assumption. - destruct (cop_plane_aux A D B C) as [p]; Cop. spliter; exists p; repeat split; assumption. - destruct (cop_plane_aux A C B D) as [p]; Cop. spliter; exists p; repeat split; assumption. - apply (cop_plane_aux A B C D HCop HAB). 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