proposition: Lemma axiom_pasch : forall A B C l p, ~ Col_H A B C -> IncidentP A p -> IncidentP B p -> IncidentP C p -> IncidentLP l p -> ~ IncidentL C l -> cut l A B -> cut l A C \/ cut l B C.
proof: Proof. intros. apply cut_two_sides in H5. assert(~Col A B C). apply ncols_coincide. assumption. assert(HH:=H5). unfold TS in HH. spliter. unfold IncidentL in H4. assert (HCop : Coplanar (P1 l) (P2 l) A C). apply plane_cop with p; trivial; apply H3; unfold IncidentL; simpl; Col. assert(HH:= cop__one_or_two_sides (P1 l)(P2 l) A C HCop H7 H4). induction HH. left. apply <-cut_two_sides. assumption. right. apply <-cut_two_sides. apply l9_2. eapply l9_8_2. apply H5. 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