proposition: Lemma proj_preserves_bet1 : forall A B C 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. 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 B B'). subst B'. assert(C = C'). apply (proj3_id A B C C' P Q); Col. subst C'. assumption. induction (eq_dec_points A C'). subst C'. assert(Col P A B'). ColR. assert(proj B P Q A). apply col_proj_proj with C. auto. Col. assumption. assert(A = B'). eapply proj_uniqueness. apply H13. assumption. subst B'. apply l7_3_2. induction(eq_dec_points B' C'). subst C'. apply between_trivial. assert(HH:= proj_not_eq_not_col B C B' C' P Q H13 H11 H1 H2). assert(A <> B'). intro. subst B'. assert(Col B C C'). apply col_proj_col with A P Q; Col. apply HH. ColR. assert(HH1:= proj_one_side B C B' C' P Q H11 H1 H2). assert(Col A B' C'). eapply proj3_col. apply H0. apply H1. apply H2. induction HH1. apply False_ind. apply HH. assert(Col A B B'). ColR. ColR. assert(TS B B' A C). unfold TS. repeat split. assert(~Col B B' A). eapply proj_not_eq_not_col; auto. apply H1. apply H0. intro. apply H17. Col. intro. apply HH. apply col_permutation_2. eapply (col_transitivity_1 _ A). auto. Col. ColR. exists B. split; Col. assert(TS B B' A C'). apply l9_2. eapply l9_8_2. apply l9_2. apply H17. assumption. unfold TS in H18. spliter. ex_and H20 BB. assert(BB= B'). apply (l6_21 B B' C' A); Col. subst BB. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel_inter_dec