proposition: Lemma cop_plane_aux : forall A B C D, Coplanar A B C D -> A <> B -> exists p, IncidentP A p /\ IncidentP B p /\ IncidentP C p /\ IncidentP D p.
proof: Proof. intros A B C D HCop HAB. destruct (col_dec A B C) as [|HNCol]; [destruct (col_dec A B D) as [|HNCol]|]. - destruct (not_col_exists A B HAB) as [E HNCol]. apply ncols_coincide in HNCol. exists (Plan A B E HNCol). unfold IncidentP; simpl; repeat split; Cop. - apply ncols_coincide in HNCol. exists (Plan A B D HNCol). unfold IncidentP; simpl; repeat split; Cop. - apply ncols_coincide in HNCol. exists (Plan A B C HNCol). unfold IncidentP; simpl; repeat split; Cop. 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