proposition: Lemma axiom_plane_uniqueness : forall A B C p q, ~ Col_H A B C -> IncidentP A p -> IncidentP B p -> IncidentP C p -> IncidentP A q -> IncidentP B q -> IncidentP C q -> p =p= q.
proof: Proof. intros A B C p q H; intros. assert (Heq : (Plan A B C H) =p= p). apply incidentp_eqp;assumption. assert ((Plan A B C H) =p= q). apply incidentp_eqp;assumption. rewrite <- Heq. 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