proposition: Lemma hilbert_s_version_of_pasch : forall A B C P Q, Coplanar A B C P -> ~ Col C Q P -> ~ Col A B P -> BetS A Q B -> exists X, Col P Q X /\ (BetS A X C \/ BetS B X C).
proof: Proof. intros A B C P Q HCop HNC1 HNC2 HAQB. rewrite BetSEq in HAQB; spliter. destruct (hilbert_s_version_of_pasch_aux C A B Q P) as [X [HPQX HBetS]]; Cop. exists X; split; Col; unfold BetS. induction HBetS; spliter; repeat split; Between. Qed.
imports: GeoCoq.Meta_theory.Dimension_axioms.upper_dim_2 GeoCoq.Tarski_dev.Ch10_line_reflexivity