proposition: Lemma proj_preserves_bet : forall A B C A' B' C' P Q, Bet A B C -> proj A P Q A' -> proj B P Q B' -> proj C P Q C' -> Bet A' B' C'.
proof: Proof. intros. induction(eq_dec_points A B). subst B. assert(A' = B'). eapply proj_uniqueness. apply H0. assumption. subst B'. apply between_trivial2. induction(eq_dec_points B C). subst C. assert(B' = C'). eapply proj_uniqueness. apply H1. assumption. subst C'. apply between_trivial. assert(A <> C). intro. subst C. apply between_identity in H. contradiction. induction (eq_dec_points A' C'). subst C'. assert(A' = B'). apply proj_perp_id with A B C P Q; Col. subst B'. apply l7_3_2. assert(P <> Q). eapply proj_diff. apply H0. assert(Col A' P Q). eapply proj_col. apply H0. assert(Col B' P Q). eapply proj_col. apply H1. assert(Col C' P Q). eapply proj_col. apply H2. assert(Col A B C). eapply bet_col. assumption. induction (eq_dec_points A A'). subst A'. eapply (proj_preserves_bet1 A B C _ _ P Q); assumption. assert(~Col A P Q). intro. apply proj_not_col in H0. apply H0. Col. assumption. induction (eq_dec_points B B'). subst B. assert(C <> C'). intro. subst C'. apply H13. assert(Col B' C P). ColR. assert(Col B' C Q). ColR. eapply (col3 B' C); Col. apply col_permutation_1 in H9. assert(~Col C P Q). intro. apply proj_not_col in H2. apply H2. Col. assumption. assert(HH:= proj_inv_exists P Q B' H7 H9). ex_and HH B. assert(HH:=proj_diff_not_col_inv B A B' A' P Q H16 H17 H0). destruct HH. assert(HH:=proj_diff_not_col_inv B C B' C' P Q H16 H17 H2). destruct HH. assert(HH:= proj_one_side B A B' A' P Q H16 H17 H0). induction HH. assert(B' = A'). apply H19. Col. subst B'. apply between_trivial2. assert(HH:= proj_one_side B C B' C' P Q H16 H17 H2). induction HH. assert(B' = C'). apply H21. Col. subst B'. apply between_trivial. assert(HH:=proj_diff_not_col_inv B A B' A' P Q H16 H17 H0). destruct HH. assert(HH:=proj_diff_not_col_inv B C B' C' P Q H16 H17 H2). destruct HH. assert(TS B B' A C). unfold TS. repeat split. intro. assert(B' = A'). apply H25. Col. subst B'. assert(Col A' B C). ColR. assert(A' = C'). apply H27. Col. contradiction. intro. assert(B' = C'). apply H27. Col. subst B'. assert(Col C' A C). ColR. assert(C' = A'). apply H25. ColR. subst C'. tauto. exists B'. split; Col. assert(TS B B' A' C). eapply l9_8_2. apply H28. assumption. assert(TS B B' C' A'). eapply l9_8_2. apply l9_2. apply H29. assumption. unfold TS in H30. spliter. ex_and H32 BB. assert(BB= B'). apply (l6_21 B B' A' C'); Col. apply (proj3_col A C B A' C' B' P Q); auto. subst BB. Between. induction(eq_dec_points C C'). subst C'. apply between_symmetry. eapply (proj_preserves_bet1 C B A _ _ P Q); try assumption. Between. assert(HH:=proj_diff_not_col_inv B A B' A' P Q H14 H1 H0). destruct HH. assert(HH:=proj_diff_not_col_inv B C B' C' P Q H14 H1 H2). destruct HH. assert(HH:= proj_one_side B A B' A' P Q H14 H1 H0). induction HH. assert(B' = A'). apply H17. Col. subst B'. apply between_trivial2. assert(HH:= proj_one_side B C B' C' P Q H14 H1 H2). induction HH. assert(B' = C'). apply H19. Col. subst B'. apply between_trivial. assert(HH:=proj_diff_not_col_inv B A B' A' P Q H14 H1 H0). destruct HH. assert(HH:=proj_diff_not_col_inv B C B' C' P Q H14 H1 H2). destruct HH. assert(TS B B' A C). unfold TS. repeat split. intro. assert(B' = A'). apply H23. Col. subst B'. assert(Col A' B C). ColR. assert(A' = C'). apply H25. Col. contradiction. intro. assert(B' = C'). apply H25. Col. subst B'. assert(Col C' A C). ColR. assert(C' = A'). apply H23. ColR. subst C'. tauto. exists B. split; Col. assert(TS B B' A' C). eapply l9_8_2. apply H26. assumption. assert(TS B B' C' A'). eapply l9_8_2. apply l9_2. apply H27. assumption. unfold TS in H28. spliter. ex_and H30 BB. assert(BB= B'). apply (l6_21 B B' A' C'); Col. apply (proj3_col A C B A' C' B' P Q); auto. subst BB. Between. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec