proposition: Lemma incidentp_eqp : forall A B C p, forall H : ~ Col_H A B C, IncidentP A p -> IncidentP B p -> IncidentP C p -> (Plan A B C H) =p= p.
proof: Proof. intros A B C p HNCol HA HB HC X. unfold IncidentP in *; simpl. assert (Hp := NCol p). apply ncols_coincide in Hp. apply ncols_coincide in HNCol. split; intro; [apply coplanar_pseudo_trans with A B C; trivial|]; apply coplanar_pseudo_trans with (M1 p) (M2 p) (M3 p); 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