proposition: Lemma per_preserves_bet_aux1 : forall P Q A B C B' C', P <> Q -> Bet A B C -> Col P Q A -> Per B B' P -> Col P Q B' -> Per C C' P -> Col P Q C' -> P <> A -> P <> B' -> P <> C' -> Bet A B' C'.
proof: Proof. intros. induction(eq_dec_points B B'). subst B'. assert(Col A B C'). apply (col3 P Q); try auto. assert(Col P A B). eapply (col_transitivity_1 _ Q); try auto. assert(Col Q A B). eapply (col_transitivity_1 _ P). auto. Col. Col. induction(eq_dec_points A B). subst B. apply between_trivial2. assert(Col P Q C). eapply col3. apply H12. Col. Col. apply bet_col. assumption. assert(Col P C' C). eapply col_transitivity_1. apply H. assumption. assumption. assert(P=C' \/ C=C'). eapply l8_9. apply l8_2. assumption. assumption. induction H15. subst C'. tauto. subst C'. assumption. induction(eq_dec_points A C). subst C. apply between_identity in H0. subst B. assert(B'=C'). apply per_id with A P; auto. apply (col_transitivity_1 _ Q); auto. subst C'. apply between_trivial. assert(C <> C'). intro. subst C'. assert(Col P A C). eapply (col_transitivity_1 _ Q); try auto. assert(Col A C B'). eapply col3. apply H. assumption. assumption. assumption. assert(Col P B' B). apply (col3 A C); Col. assert(B=B' \/ P=B'). eapply l8_9. assumption. Col. induction H14. subst B'. tauto. auto. induction (eq_dec_points A B'). subst B'. apply between_trivial2. assert(A <> B). intro. subst B. apply per_not_col in H2. apply H2. ColR. assumption. auto. induction(col_dec C B B'). assert(C=B). eapply (l6_21 B B'). assert(Per B B' A). eapply (per_col _ _ P). auto. assumption. ColR. apply per_not_col in H15. apply H15. auto. auto. apply H13. Col. Col. apply bet_col. apply H0. Col. subst C. assert(B'=C'). apply per_id with B P; ColR. subst C'. apply between_trivial. assert(Perp B' B' B' P \/ Perp B B' B' P). eapply perp_in_perp_bis. apply per_perp_in. auto. auto. assumption. induction H15. apply perp_not_eq_1 in H15. tauto. assert(Perp C' C' C' P \/ Perp C C' C' P). eapply perp_in_perp_bis. apply per_perp_in. auto. auto. assumption. induction H16. apply perp_not_eq_1 in H16. tauto. assert(Par B B' C C'). eapply l12_9_2D. apply H15. apply perp_sym. apply perp_left_comm. eapply perp_col. auto. apply perp_left_comm. apply perp_sym. apply H16. eapply (col_transitivity_1 _ Q); auto. unfold Par in H17. assert(Par_strict B B' C C'). induction H17. assumption. spliter. apply False_ind. apply H14. ColR. clear H17. assert(OS B B' C C'). eapply l12_6. assumption. assert(Per B B' A). eapply (per_col _ _ P); try auto. ColR. induction(eq_dec_points A C'). subst C'. assert(TS B B' A C). unfold TS. repeat split; try auto. apply per_not_col in H19. intro. apply H19. Col. auto. auto. exists B. split. Col. assumption. apply l9_2 in H20. apply l9_9 in H20. contradiction. assert(TS B B' A C). unfold TS. repeat split; try auto. apply per_not_col in H19. intro. apply H19. Col. auto. auto. exists B. split. Col. assumption. assert(TS B B' C' A). eapply l9_8_2. apply l9_2. apply H21. assumption. unfold TS in H22. spliter. ex_and H24 T. assert(T = B'). apply (l6_21 B B' A C'); ColR. subst T. Between. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec