proposition: Lemma per3_preserves_bet2 : forall O A B C A' B' C', Col O A C -> A' <> C' -> 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' C' -> Bet A B C.
proof: Proof. intros O A B C A' B' C'. intro HX. intros. induction(eq_dec_points A A'). subst A'. apply (per3_preserves_bet2_aux O A B C B' C');auto. induction(eq_dec_points C C'). subst C'. apply between_symmetry. apply(per3_preserves_bet2_aux O C B A B' A'); Col; Between. assert(Perp O A' C C'). apply per_perp_in in H6; auto. apply perp_in_comm in H6. apply perp_in_perp_bis in H6. induction H6. apply (perp_col _ C'); Col; Perp. apply perp_distinct in H6. tauto. assert(Perp O A' A A'). apply per_perp_in in H4; auto. apply perp_in_comm in H4. apply perp_in_perp_bis in H4. induction H4. Perp. apply perp_distinct in H4. tauto. assert(Par A A' C C'). apply(l12_9 A A' C C' O A'); [Cop..|Perp|Perp]. induction H13. assert(HH:=l12_6 A A' C C' H13). apply par_strict_symmetry in H13. assert(HP:=l12_6 C C' A A' H13). induction(eq_dec_points B B'). subst B'. assert(OS A' A B C'). apply out_one_side. right. intro. apply H13. exists C'. split; Col. repeat split. intro. subst A'. apply H13. exists C. split; Col. auto. left; auto. apply invert_one_side in H14. assert(OS A A' B C). apply (one_side_transitivity _ _ _ C'). assumption. apply one_side_symmetry. assumption. assert(Out A B C). apply (col_one_side_out A A');auto. assert(OS C' C B A'). apply out_one_side. right. intro. apply H13. exists A'. split; Col. repeat split. intro. subst C'. apply H13. exists A. split; Col. auto. left; Between. apply invert_one_side in H17. assert(OS C C' B A). apply (one_side_transitivity _ _ _ A'). assumption. apply one_side_symmetry. assumption. apply one_side_symmetry in H18. assert(Out C A B). apply (col_one_side_out C C');Col. unfold Out in *. spliter. induction H23; induction H21. assumption. assumption. assert(A = C). apply (between_equality A C B); auto. subst C. apply False_ind. apply H13. exists A. split; Col. assert(B = C). apply (between_equality B C A); Between. subst C. Between. assert(Perp O A' B B'). apply per_perp_in in H5; auto. apply perp_in_comm in H5. apply perp_in_perp_bis in H5. induction H5. apply (perp_col _ B'); Col; Perp. apply bet_col in H0. ColR. apply perp_distinct in H5. tauto. assert(Par B B' A A'). apply(l12_9 B B' A A' O A'); Perp. exists O. left. assert_diffs. split; ColR. exists A'. left. split; Col. exists B'. left. split; ColR. exists A'. left. split; Col. induction H16. assert(HQ:=l12_6 B B' A A' H16). assert(Par B B' C C'). apply(l12_9 B B' C C' O A'); Perp. exists O. left. assert_diffs. split; ColR. exists C'. left. split; Col. exists B'. left. assert_diffs. split; ColR. exists A'. left. split; Col. induction H17. assert(HR:=l12_6 B B' C C' H17). assert(TS B B' A' C'). repeat split; auto. intro. apply H16. exists A'. split; Col. intro. apply H17. exists C'. split; Col. exists B'. split; Col. apply one_side_symmetry in HQ. assert(HH1:= l9_8_2 B B' A' A C' H18 HQ). apply l9_2 in HH1. apply one_side_symmetry in HR. assert(HH2:= l9_8_2 B B' C' C A HH1 HR). unfold TS in HH2. spliter. ex_and H21 T. assert(B = T). apply (l6_21 B B' A C); Col. intro. subst C. apply H13. exists A. split; Col. subst T. Between. spliter. induction(eq_dec_points B C). subst C. Between. assert(Col A C C'). ColR. apply False_ind. apply H13. exists A. split; Col. spliter. induction(eq_dec_points A B). subst B. Between. assert(Col C A A'). ColR. apply False_ind. apply H13. exists C. split; Col. spliter. assert(A <> C). intro. subst C. apply H. apply(per2_col_eq O A' C' A); Col. assert(Col O C C'). ColR. apply False_ind. apply per_not_col in H6; auto. apply H6. Col. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel