proposition: Lemma hilbert_s_version_of_pasch_aux : forall A B C I P, Coplanar A B C P -> ~ Col A I P -> ~ Col B C P -> Bet B I C -> B <> I -> I <> C -> B <> C -> exists X, Col I P X /\ ((Bet A X B /\ A <> X /\ X <> B /\ A <> B) \/ (Bet A X C /\ A <> X /\ X <> C /\ A <> C)).
proof: Proof. intros A B C I P HCop HNC HNC' HBet HBI HIC HBC. assert (HTS : TS I P B C). { assert_cols; split; try (intro; apply HNC'; ColR). split; try (intro; apply HNC'; ColR). exists I; Col. } assert (HCop1 : Coplanar A P B I) by (assert_diffs; apply col_cop__cop with C; Cop; Col). elim (two_sides_dec I P A B); intro HTS'. { destruct HTS' as [Hc1 [Hc2 [T [HCol HBet']]]]. exists T; split; Col. left; split; Col. split; try (intro; treat_equalities; Col). split; intro; treat_equalities; Col. } { rename HTS' into HOS. assert (HTS' : TS I P A C). { apply l9_8_2 with B; Col. unfold TS in HTS; spliter. apply cop_nts__os; Cop. intro; apply HOS; apply l9_2; Col. } destruct HTS' as [Hc1 [Hc2 [T [HCol HBet']]]]. exists T; split; Col. right; split; Col. split; try (intro; treat_equalities; Col). split; intro; treat_equalities; Col. } Qed.
imports: GeoCoq.Meta_theory.Dimension_axioms.upper_dim_2 GeoCoq.Tarski_dev.Ch10_line_reflexivity