proposition: Lemma pasch : forall A B C P Q : ITpoint, BetT A P C -> BetT B Q C -> exists x : ITpoint, BetT P x B /\ BetT Q x A.
proof: Proof. intros. induction (col_dec A B C). eapply pasch_col_case;eauto. unfold BetT in *. decompose [or] H;clear H. decompose [or] H0;clear H0. elim (Iinner_pasch A B C P Q H2 H H1). intros. spliter. exists x. split. tauto. tauto. subst. exists Q;auto. subst. exists P. split. auto. left. apply Ibetween_symmetry. auto. subst. exists P;auto. subst. decompose [or] H0;clear H0. exists Q. split. left. apply Ibetween_symmetry. auto. auto. subst. exists Q;auto. subst. exists C;auto. Qed.
imports: GeoCoq.Axioms.beeson_s_axioms GeoCoq.Axioms.tarski_axioms Classical