proposition: Lemma inner_pasch_aux : forall A B C P Q, ~ ColH B C P -> Bet A P C -> Bet B Q C -> exists X, Bet P X B /\ Bet Q X A.
proof: Proof. unfold Bet. intros. induction H0; induction H1. elim (eq_dec_pointsH Q A);intros HQA. subst. exfalso. apply H. apply betH_expand in H1;spliter. apply betH_expand in H0;spliter. ColHR. line Q A l HQA. induction(eq_dec_pointsH P A). subst P. exists A. split; unfold Bet. right; left. auto. right; right. auto. induction(eq_dec_pointsH Q C). subst Q. exists P. split; unfold Bet in *. right; left; auto. left. apply between_comm. assumption. assert(HI:~IncidL P l). intro. apply H. apply between_col in H0. apply between_col in H1. spliter. line_col A P Q. assert(ColH P C Q). eapply (colH_trans A P); Col. eapply (colH_trans Q C); Col. induction(eq_dec_pointsH B Q). subst Q. exists B. split; right. right; auto. left; auto. induction(eq_dec_pointsH A C). subst C. apply False_ind. apply betH_distincts in H0. solve [intuition]. assert(~IncidL B l). intro. line_col A B Q. assert(ColH A B C). apply between_col in H0. apply between_col in H1. spliter. apply(colH_trans B Q); Col. apply between_col in H0. apply between_col in H1. spliter. apply H. apply (colH_trans A C); Col. assert(~IncidL C l). intro. line_col A C Q. assert(ColH A B C). apply between_col in H1. spliter. apply(colH_trans C Q); Col. apply H. apply between_col in H0. apply between_col in H1. spliter. apply (colH_trans A C); Col. assert(cut l B C). unfold cut. repeat split; auto. exists Q. split; auto. destruct (plane_existence B C P H) as [p]. spliter. assert(PH:=pasch B C P l p). induction PH; trivial. clear dependent p. unfold cut in H14. spliter. destruct H13 as [X HX]. exists X. spliter. split. left. apply between_comm. assumption. induction(eq_dec_pointsH A X). subst X. right; right; auto. assert(A <> Q). intro. subst Q. apply between_col in H0. apply between_col in H1. spliter. apply H. apply (colH_trans A C); Col. assert(P <> C). intro. subst P. apply H. Col. assert(A <> B). intro. subst B. apply between_col in H0. spliter. apply H. Col. assert(X <> Q). intro. subst X. apply H. apply between_col in H1. apply between_col in H14. spliter. apply (colH_trans B Q); Col. assert(ColH A X Q). unfold ColH. exists l. split; auto. assert(HN:~ ColH A C Q). intro. apply H9. col_line H21 l00. lines_eq l l00. assumption. assert (HPB : P<>B). apply ncolH_distincts in H. intuition. line P B m HPB. assert(~ IncidL Q m). intro. apply H. unfold ColH. unfold ColH. exists m. repeat split; try assumption. apply between_col in H1. spliter. col_line H1 m0. lines_eq m m0. assumption. assert(~ColH A B P). intro. apply H. apply(colH_trans A P); Col. assert(cut m A C). unfold cut. split. intro. apply H24. unfold ColH. exists m. repeat split; auto. split. intro. apply H. unfold ColH. unfold ColH. exists m. repeat split; auto. exists P. split; auto. destruct (plane_existence A C Q HN) as [p]. spliter. assert(HH:= pasch A C Q m p). induction HH; trivial. clear dependent p. unfold cut in H29. spliter. destruct H28 as [Y H28]. spliter. assert(X=Y). apply(inter_incid_uniquenessH B X Y l m); auto. apply between_col in H29. spliter. unfold ColH in H29. destruct H29 as [l0 H29]. spliter. lines_eq l0 l. assumption. apply between_col in H14. spliter. col_line H14 m0. lines_eq m m0. assumption. subst Y. left. apply between_comm. assumption. clear dependent p. unfold cut in H29. spliter. destruct H28 as [I H28]. spliter. assert(ColH C I Q). apply between_col in H29. tauto. col_line H30 o. assert(~IncidL C m). intro. apply H. unfold ColH. unfold ColH. exists m. repeat split; auto. assert(IncidL B o). apply between_col in H1. spliter. col_line H1 n0. lines_eq o n0. assumption. assert(HH:= inter_incid_uniquenessH C I B m o H34 H31 H28 H22 H32 H35). subst I. apply False_ind. apply between_only_one' in H1. spliter. apply H36. apply between_comm. assumption. apply (line_on_plane P B). assumption. assumption. assumption. apply (line_on_plane' A C); Col. apply (line_on_plane' Q C); Col. clear dependent p. unfold cut in H14. spliter. destruct H13 as [I H13]. spliter. assert(A = I). line A C s H7. apply (inter_incid_uniquenessH Q A I s l); auto. intro. assert( A <> Q). intro. subst Q. apply between_col in H1. spliter. apply H. apply between_col in H0. unfold ColH. spliter. apply (colH_trans A C); Col. lines_eq l s. unfold cut in H10. spliter. contradiction. apply between_col in H14. spliter. apply between_col in H0. spliter. unfold ColH in H0. destruct H0 as [s0 H0]. spliter. lines_eq s s0. col_line H14 s1. apply ncolH_distincts in H;spliter. lines_eq s s1. assumption. subst I. apply between_only_one in H14. spliter. contradiction. apply (line_on_plane Q A). assumption. assumption. assumption. apply (line_on_plane' B C); Col. apply (between_diff B Q C H1). apply betH_colH in H0. spliter. apply (line_on_plane' P C); Col. induction H1. subst Q. exists B. split. right;right; auto. right;left;auto. subst Q. exists P. split. right;left; auto. left. apply between_comm. assumption; subst P. induction H0. subst P. exists A. split. right; left; auto. right; right; auto. subst P. apply False_ind. apply H. Col. induction H0. subst P. exists A. split. right;left; auto. right; right; auto. subst P. apply False_ind. apply H. Col. 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