proposition: Lemma pasch_col_case : forall A B C P Q : ITpoint, BetT A P C -> BetT B Q C -> ICol A B C -> exists x : ITpoint, BetT P x B /\ BetT Q x A.
proof: Proof. intros. elim (eq_dec A B);intro. subst. exists B. unfold BetT;auto. elim (eq_dec A C);intro. subst. apply BetT_id in H. subst. exists P. unfold BetT;auto. elim (eq_dec B C);intro. subst. apply BetT_id in H0. subst. exists Q. unfold BetT;auto. elim (eq_dec B Q);intro. subst. exists Q. unfold BetT;auto. elim (eq_dec C Q);intro. subst. exists P. split. unfold BetT;auto. apply BetT_symmetry. auto. elim (eq_dec A P);intro. subst. exists P. unfold BetT;auto. elim (eq_dec C P);intro. subst. exists Q. split. apply BetT_symmetry. auto. unfold BetT;auto. unfold ICol in H1. spliter. apply not_and_or in H1. induction H1. apply NNPP in H1. unfold IT in *. apply not_and_or in H1. induction H1. apply NNPP in H1. subst. intuition. apply not_and_or in H1. induction H1. apply NNPP in H1. subst. intuition. apply NNPP in H1. exists A. split. apply Ibetween_symmetry in H1. induction H. assert (T:=Ibetween_inner_transitivity B A P C H1 H). unfold BetT. left. apply Ibetween_symmetry;auto. induction H;subst. unfold BetT;auto. left. apply Ibetween_symmetry;auto. unfold BetT;auto. apply not_and_or in H1. induction H1. apply NNPP in H1. unfold IT in H1. apply not_and_or in H1. induction H1. apply NNPP in H1. subst. intuition. apply not_and_or in H1. induction H1. apply NNPP in H1. subst. intuition. apply NNPP in H1. exists C. unfold BetT in H. induction H;induction H0. split. apply BetT_symmetry. left. apply Ibetween_inner_transitivity with A. apply Ibetween_symmetry;auto. apply Ibetween_symmetry;auto. apply BetT_symmetry. left. apply Ibetween_inner_transitivity with B. assumption. apply Ibetween_symmetry;auto. induction H0;subst;intuition. induction H;subst;intuition. induction H;subst;intuition. apply NNPP in H1. induction H;induction H0. exists B. split. unfold BetT;auto. left. apply Ibetween_symmetry. apply Ibetween_inner_transitivity with C. unfold IT in H1. apply not_and_or in H1. induction H1. apply NNPP in H1. subst. intuition. apply not_and_or in H1. induction H1. apply NNPP in H1. subst. intuition. apply NNPP in H1. assumption. assumption. induction H0;subst;intuition. induction H;subst;intuition. induction H;subst;intuition. Qed.
imports: GeoCoq.Axioms.beeson_s_axioms GeoCoq.Axioms.tarski_axioms Classical