proposition: Lemma per3_preserves_bet1 : forall O A B C A' B' C', Col O A B -> Bet A B C -> O <> A' -> O <> B' -> O <> C' -> Per O A' A -> Per O B' B -> Per O C' C -> Col A' B' C' -> Col O A' B' -> Bet A' B' C'.
proof: Proof. intros O A B C A' B' C'. intro HC. intros. induction(eq_dec_points A B). subst B. assert(A' = B'). apply(per2_col_eq O A' B' A H0 H1 H3 H4); Col. subst B'. Between. induction (eq_dec_points A A'). subst A'. induction(eq_dec_points B B'). subst B'. assert(Col O C C'). apply bet_col in H. ColR. assert(C = C'). apply bet_col in H. assert(O = C' \/ C = C'). apply(l8_9 O C' C H5); Col. induction H10. contradiction. assumption. subst C'. assumption. induction(eq_dec_points A B'). subst B'. Between. assert(A <> C). intro. subst C. apply between_identity in H. contradiction. assert( ~ Col O B' B). apply(per_not_col O B' B H1); auto. assert(C <> C'). intro. subst C'. clean_trivial_hyps. apply H12. apply bet_col in H. ColR. assert(Perp B B' O A). apply per_perp_in in H4; auto. apply perp_in_perp_bis in H4. induction H4. apply perp_distinct in H4. tauto. apply perp_sym. apply perp_right_comm. apply(perp_col O B' B' B A); auto. Col. assert(Perp C C' O A). apply per_perp_in in H5; auto. apply perp_in_perp_bis in H5. induction H5. apply perp_distinct in H5. tauto. apply perp_sym. apply perp_right_comm. apply(perp_col O C' C' C A); auto. apply bet_col in H. ColR. assert(Par B B' C C'). apply(l12_9 B B' C C' O A); Cop. induction H16. assert(HH:=l12_6 B B' C C' H16). assert(TS B B' A C). unfold TS. repeat split; Col. assert(~Col B' A B). apply(perp_not_col). apply perp_left_comm. apply(perp_col A O B B' B'); Col. Perp. intro. apply H17. Col. intro. apply H16. exists C. split; Col. exists B. split; Col. assert(TS B B' C' A). apply(l9_8_2 B B' C C' A). apply l9_2. assumption. assumption. unfold TS in H18. spliter. ex_and H20 T. assert(B'=T). apply (l6_21 B B' A C'); Col. intro. subst C'. apply between_identity in H21. subst T. contradiction. subst T. apply between_symmetry. assumption. spliter. assert(Per O C' B). apply(per_col O C' C B); Col. assert(B'=C'). apply(per2_col_eq O B' C' B); Col. ColR. subst C'. Between. induction(eq_dec_points A' B'). subst B'. Between. induction(eq_dec_points B C). subst C. assert(B' = C'). apply(per2_col_eq O B' C' B); auto. ColR. subst C'. Between. induction(eq_dec_points B B'). subst B'. induction(eq_dec_points A' B). subst B. Between. assert(C <> C'). intro. subst C'. assert( ~ Col O A' A). apply(per_not_col O A' A ); auto. apply H13. apply bet_col in H. ColR. assert(Perp A A' O A'). apply per_perp_in in H3; auto. apply perp_in_comm in H3. apply perp_in_perp_bis in H3. induction H3. Perp. apply perp_distinct in H3. tauto. assert(Perp C C' O A'). apply per_perp_in in H5; auto. apply perp_in_comm in H5. apply perp_in_perp_bis in H5. induction H5. apply perp_sym. apply (perp_col _ C'); auto. Perp. ColR. apply perp_distinct in H5. tauto. assert(Col O A A'). ColR. assert(Par A A' C C'). apply(l12_9 A A' C C' O A'); Cop. induction H17. assert(HH:=l12_6 A A' C C' H17). assert(OS C C' A A'). apply(l12_6 C C' A A'). Par. assert(OS C C' A B). apply(out_one_side C C' A B). left. intro. apply H17. exists A. split; Col. unfold Out. repeat split; auto. intro. subst C. apply between_identity in H. contradiction. right. Between. assert(OS C C' A' B). apply(one_side_transitivity C C' A' A); auto. apply one_side_symmetry. assumption. assert(Out C' B A'). induction H6. unfold Out. repeat split. intro. subst C'. clean_trivial_hyps. unfold OS in H18. ex_and H18 T. unfold TS in H4. spliter. apply H4. Col. intro. subst C'. apply H17. exists A'. split; Col. left. Between. induction H6. assert(TS C C' B A'). unfold TS. repeat split. intro. unfold OS in H19. ex_and H19 T. unfold TS in H22. spliter. contradiction. intro. apply H17. exists A'. split; Col. exists C'. split; Col. apply one_side_symmetry in H20. apply l9_9_bis in H20. contradiction. unfold Out. repeat split. intro. subst C'. apply H17. exists A. apply bet_col in H. split; Col. intro. subst C'. apply H17. exists A'. split; Col. right; auto. assert(Out A' B C'). induction H6. unfold Out. repeat split. intro. subst A'. clean_trivial_hyps. apply H17. exists C. apply bet_col in H. split; Col. intro. subst C'. unfold Out in H21. tauto. left. auto. induction H6. unfold Out in H21. spliter. unfold Out. repeat split. intro. subst A'. apply H17. exists C. apply bet_col in H. split; Col. auto. induction H23. left. Between. apply False_ind. apply H22. apply (between_equality _ _ B); Between. assert(OS A A' B C). apply(out_one_side A A' B C). right. intro. apply H17. exists C. split; Col. unfold Out. repeat split; auto. intro. subst C. apply between_identity in H. contradiction. assert(OS A A' C' B). apply(one_side_transitivity A A' C' C); apply one_side_symmetry; auto. assert(TS A A' B C'). unfold TS. repeat split. intro. unfold OS in H22. ex_and H22 T. unfold TS in H22. spliter. contradiction. intro. apply H17. exists C'. split; Col. exists A'. split; Col. Between. apply one_side_symmetry in H23. apply l9_9_bis in H23. contradiction. unfold Out in *. spliter. clean_duplicated_hyps. induction H26; induction H24. assumption. apply False_ind. apply H21. apply(between_equality _ _ A'); Between. apply False_ind. apply H10. apply(between_equality _ _ C'); Between. apply False_ind. apply H25. apply(between_equality _ _ B); Between. spliter. assert(~Col O C' C). apply(per_not_col); auto. apply False_ind. apply H21. assert(A<>C). intro. subst C. apply between_identity in H. subst B. tauto. apply bet_col in H. ColR. assert(Perp A A' O A'). apply per_perp_in in H3; auto. apply perp_in_comm in H3. apply perp_in_perp_bis in H3. induction H3. Perp. apply perp_distinct in H3. tauto. assert(Perp B B' O A'). apply per_perp_in in H4; auto. apply perp_in_comm in H4. apply perp_in_perp_bis in H4. induction H4. apply perp_sym. apply (perp_col _ B'); Col. Perp. apply perp_distinct in H4. tauto. assert(Par A A' B B'). apply(l12_9 A A' B B' O A'); Cop. induction H15. assert(HH:=l12_6 A A' B B' H15). assert(TS B B' A C). unfold TS. repeat split; Col. intro. apply H15. exists A. split; Col. intro. apply H11. apply (l6_21 B B' A C); Col. intro. apply H15. exists A. split; Col. intro. subst C. apply between_identity in H. subst B. tauto. exists B. split; Col. assert(OS B B' A A'). apply(l12_6 B B' A A'). Par. assert(HP:= l9_8_2 B B' A A' C H16 H17). induction(eq_dec_points C C'). subst C'. unfold TS in HP. spliter. ex_and H20 T. assert(T = B'). apply (l6_21 B B' A' C); Col. intro. subst A'. apply between_identity in H21. subst T. contradiction. subst T. assumption. assert(Perp C C' O A'). apply per_perp_in in H5; auto. apply perp_in_comm in H5. apply perp_in_perp_bis in H5. induction H5. apply perp_sym. apply (perp_col _ C'); Perp. ColR. apply perp_distinct in H5. tauto. assert(Par B B' C C'). apply(l12_9 B B' C C' O A'); auto. exists O. left. split; ColR. exists C'. left. split; ColR. exists B'. left. split; Col. exists B'. left. split; Col. induction H20. assert(HQ:=l12_6 B B' C C' H20). assert(TS B B' C' A'). apply(l9_8_2 B B' C C' A'); auto. apply l9_2. assumption. unfold TS in H21. spliter. ex_and H23 T. assert(T = B'). apply (l6_21 B B' A' C'); Col. intro. subst C'. apply between_identity in H24. subst T. contradiction. subst T. Between. spliter. unfold TS in HP. spliter. apply False_ind. apply H25. ColR. spliter. apply perp_left_comm in H13. apply perp_not_col in H13. apply False_ind. apply H13. ColR. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel