proposition: Lemma axiom_line_on_plane : forall A B l p, A <> B -> IncidentL A l -> IncidentL B l -> IncidentP A p -> IncidentP B p -> IncidentLP l p.
proof: Proof. intros A B l p HAB HAl HBl HAp HBp X HXl. destruct (ex_ncol_cop (M1 p) (M2 p) (M3 p) A B HAB) as [C [HCp HNCol]]. apply ncols_coincide in HNCol. assert (Heq : (Plan A B C HNCol) =p= p). apply incidentp_eqp; auto. rewrite <- Heq. unfold IncidentP; simpl. exists X; left; split. apply cols_coincide_1; exists l; repeat split; assumption. Col. 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