proposition: Lemma pasch_general_case: forall A B C P Q : Point, Bet A P C -> Bet B Q C -> A <> P -> P <> C -> B <> Q -> Q <> C -> ~ (Bet A B C \/ Bet B C A \/ Bet C A B) -> exists x : Point, Bet P x B /\ Bet Q x A.
proof: Proof. intros. induction (eq_dec_pointsH A B). - subst. unfold Bet in *;intuition. - induction (eq_dec_pointsH B C). subst;unfold Bet in *;intuition. induction (eq_dec_pointsH A C). subst;unfold Bet in *;intuition. apply inner_pasch_aux with C;auto. apply bet_colH in H. intro. assert (ColH A B C). apply colH_trans with P C;Col. apply H5. apply between_one in H10;auto. unfold Bet. intuition (auto using between_comm). Qed.
imports: Setoid Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop GeoCoq.Axioms.gupta_inspired_variant_axioms GeoCoq.Meta_theory.Models.gupta_inspired_to_tarski GeoCoq.Tactics.Coinc.tactics_axioms GeoCoq.Tactics.Coinc.ColR GeoCoq.Meta_theory.Dimension_axioms.upper_dim_3 GeoCoq.Meta_theory.Parallel_postulates.parallel_postulates GeoCoq.Axioms.hilbert_axioms