proposition: Lemma per_preserves_bet : forall P Q A B C A' B' C', P <> Q -> Bet A B C -> Per A A' P -> 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 A A'). subst A'. eapply (per_preserves_bet_aux1 P Q A B C B' C'); assumption. induction(eq_dec_points B B'). subst B'. eapply (per_preserves_bet_aux2 P Q A B C A' C'); assumption. induction(eq_dec_points C C'). subst C'. assert(HH:=(per_preserves_bet_aux1 P Q C B A B' A')). apply between_symmetry. apply HH; try assumption. Between. induction (eq_dec_points A B). subst B. assert(A'=B'). eapply (per_id A _ _ P); try auto. ColR. subst B'. apply between_trivial2. induction (eq_dec_points C B). subst B. assert(C'=B'). eapply (per_id C _ _ P); try auto. ColR. subst B'. apply between_trivial. assert(A <> C). intro. subst C. apply between_identity in H0. contradiction. assert(Perp B' B' B' P \/ Perp B B' B' P). eapply perp_in_perp_bis. apply per_perp_in. auto. auto. assumption. induction H16. apply perp_not_eq_1 in H16. 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 H17. apply perp_not_eq_1 in H17. tauto. assert(Perp A' A' A' P \/ Perp A A' A' P). eapply perp_in_perp_bis. apply per_perp_in. auto. auto. assumption. induction H18. apply perp_not_eq_1 in H18. tauto. assert(Par B B' C C'). eapply l12_9_2D. apply H16. apply perp_sym. apply perp_left_comm. eapply perp_col. auto. apply perp_left_comm. apply perp_sym. apply H17. eapply (col_transitivity_1 _ Q); auto. assert(Par B B' A A'). eapply l12_9_2D. apply H16. apply perp_sym. apply perp_left_comm. eapply perp_col. auto. apply perp_left_comm. apply perp_sym. apply H18. eapply (col_transitivity_1 _ Q); auto. assert(Col A B C). apply bet_col. assumption. induction(eq_dec_points A' C'). subst C'. assert(Col A C A'). eapply per2__col. apply H1. auto. assumption. assert(Col A B A'). eapply (col_transitivity_1 _ C); try auto. Col. assert(Per B A' P). apply l8_2. eapply (per_col _ _ A). auto. apply l8_2. assumption. Col. assert(A' = B'). eapply (per_id B _ _ P); try auto. intro. subst A'. apply par_right_comm in H20. apply par_id in H20. assert(Per P B B'). eapply (per_col _ _ A). auto. apply l8_2. assumption. Col. apply H11. eapply l8_7. apply H25. apply l8_2. assumption. ColR. subst B'. apply between_trivial. assert(Par A A' C C'). eapply par_trans. apply par_symmetry. apply H20. assumption. assert(A' <> B'). intro. subst B'. apply H22. assert(Col A B A'). eapply per2__col. apply H1. auto. assumption. assert(Col C A A'). ColR. assert(Per P A' C). eapply (per_col _ _ A). auto. apply l8_2. assumption. Col. apply l8_2 in H26. apply per_id with C P; auto. intro. subst C. apply perp_comm in H17. apply perp_not_col in H17. apply H17. ColR. ColR. assert(C' <> B'). intro. subst B'. apply H22. assert(Col B C C'). eapply per2__col. apply H3. auto. assumption. assert(Col A C C'). ColR. assert(Per P C' A). eapply (per_col _ _ C). auto. apply l8_2. assumption. Col. apply l8_2 in H27. apply per_id with A P; auto. ColR. assert(Par_strict B B' C C'). induction H19. assumption. spliter. apply False_ind. apply H25. apply per_id with B P; auto. intro. subst B. apply perp_comm in H16. apply perp_not_col in H16. apply H16. ColR. apply l8_2. apply (per_col _ _ C). auto. apply l8_2. assumption. Col. ColR. assert(Par_strict B B' A A'). induction H20. assumption. spliter. apply False_ind. apply H24. apply per_id with B P; auto. intro. subst B. apply perp_comm in H16. apply perp_not_col in H16. apply H16. ColR. apply l8_2. eapply (per_col _ _ A). auto. apply l8_2. assumption. Col. ColR. assert(OS B B' A A'). apply l12_6. assumption. assert(OS B B' C C'). apply l12_6. assumption. assert(TS B B' A C). unfold TS. repeat split; auto. intro. apply H24. apply per_id with A P; auto. apply l8_2. apply per_col with B. auto. apply l8_2. apply H3. Col. ColR. intro. apply H25. apply per_id with C P; auto. apply l8_2. apply per_col with B. auto. apply l8_2. apply H3. Col. ColR. exists B. split. Col. assumption. assert(TS B B' A' C). eapply l9_8_2. apply H30. assumption. assert(TS B B' A' C'). apply l9_2. eapply l9_8_2. apply l9_2. apply H31. assumption. unfold TS in H32. spliter. ex_and H34 BB. assert(BB = B'). apply (l6_21 B B' C' A'); ColR. subst BB. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec