proposition: Lemma per_preserves_bet_aux2 : forall P Q A B C A' C', P <> Q -> Bet A B C -> Per A A' P -> Col P Q A' -> 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 A A'). subst A'. 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. apply False_ind. apply H9. apply l8_9 in H1. induction H1. assumption. subst A'. tauto. ColR. assert(~Col P Q A). intro. assert (Col A A' P). ColR. apply l8_9 in H1. induction H1;tauto. assumption. assert(A <> B). intro. subst B. contradiction. induction (eq_dec_points C C'). subst C'. assert(Col A' B C). eapply (col3 P Q ); assumption. assert(Col C A' P). ColR. assert(B=C). eapply l6_21. apply H11. apply H12. Col. Col. Col. Col. subst C. apply between_trivial. induction(eq_dec_points A' C'). subst C'. assert(Per A A' B). apply per_col with P; ColR. assert(Per C A' B). apply per_col with P; ColR. eapply l8_6 in H14. subst B. apply between_trivial. apply H15. Between. assert(HH:=ex_per_cong P Q B A P Q). assert(exists T, Per T B P /\ Cong T B P Q /\ OS P Q T A). apply HH; auto. ex_and H15 T. clear HH. assert(Perp B B B P \/ Perp T B B P). eapply perp_in_perp_bis. apply per_perp_in. intro. subst T. apply cong_symmetry in H16. apply cong_identity in H16. contradiction. auto. auto. induction H18. apply perp_not_eq_1 in H18. 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 H19. apply perp_not_eq_1 in H19. tauto. assert(Par T B C C'). eapply l12_9_2D. apply H18. apply perp_sym. apply perp_left_comm. eapply perp_col. auto. apply perp_left_comm. apply perp_sym. apply H19. eapply (col_transitivity_1 _ Q); auto. assert(Perp A' A' A' P \/ Perp A A' A' P). eapply perp_in_perp_bis. apply per_perp_in. auto. auto. assumption. induction H21. apply perp_not_eq_1 in H21. tauto. assert(Par T B A A'). eapply l12_9_2D. apply H18. apply perp_sym. apply perp_left_comm. eapply perp_col. auto. apply perp_left_comm. apply perp_sym. apply H21. eapply (col_transitivity_1 _ Q); auto. assert(Par_strict T B C C'). induction H20. assumption. spliter. apply False_ind. apply H14. apply per_id with A P; auto. apply l8_2. eapply per_col with C. auto. apply l8_2. apply H4. auto. apply col_permutation_2. apply col_transitivity_1 with B. assert(~Col P Q C). intro. assert (Col C C' P). ColR. apply l8_9 in H4. induction H1;tauto. assumption. intro. subst C. contradiction. Col. Col. ColR. assert(Par_strict T B A A'). induction H22. assumption. spliter. apply False_ind. apply H14. eapply sym_equal. apply per_id with C P; auto. apply l8_2. apply per_col with A. auto. apply l8_2. apply H1. apply col_permutation_2. apply col_transitivity_1 with B; Col. ColR. assert(OS T B C C'). apply l12_6. assumption. assert(OS T B A A'). apply l12_6. assumption. assert(TS T B A C). unfold TS. repeat split. intro. unfold Par_strict in H24. spliter. apply H28. exists A. split. assumption. Col. intro. unfold Par_strict in H23. spliter. apply H28. exists C. split. assumption. Col. exists B. split. Col. assumption. assert(TS T B C' A). eapply l9_8_2. apply l9_2. apply H27. assumption. assert(TS T B A' C'). eapply l9_8_2. apply l9_2. apply H28. assumption. unfold TS in H29. spliter. ex_and H31 BB. assert(B=BB). eapply (l6_21 T B A' C'); Col. ColR. subst BB. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec