proposition: Lemma per13_preserves_bet : forall A B C A' C', Bet A B C -> B <> A' -> B <> C' -> Col A' B C' -> Per B A' A -> Per B C' C -> Bet A' B C'.
proof: Proof. intros. assert(Col A B C). apply bet_col in H. Col. induction(eq_dec_points A A'). subst A'. assert(Col B C' C). ColR. assert(B = C' \/ C = C'). apply l8_9; auto. induction H7. contradiction. subst C'. assumption. assert(C <> C'). intro. subst C'. assert(Col A A' B). ColR. assert(B = A' \/ A = A'). apply l8_9; Col. induction H8; tauto. assert(Perp B A' A' 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 C' C' C). 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' B A'); Perp; Cop. apply perp_sym. apply(perp_col _ C'); Perp. ColR. induction H10. assert(HH:=par_strict_symmetry A A' C C' H10). apply l12_6 in H10. apply l12_6 in HH. assert(~Col A A' B). apply per_not_col in H3; auto. intro. apply H3. Col. assert(~Col C C' B). apply per_not_col in H4; auto. intro. apply H4. Col. assert(OS A A' B C). apply out_one_side. left; auto. repeat split. intro. subst A. unfold OS in H10. ex_and H10 X. unfold TS in H13. spliter. apply H13. Col. intro. subst C. unfold OS in H10. ex_and H10 X. unfold TS in H10. spliter. apply H10. Col. left. assumption. assert(OS C C' B A). apply out_one_side. left; auto. repeat split. intro. subst C. apply H12. Col. intro. subst C. unfold OS in H10. ex_and H10 X. unfold TS in H10. spliter. apply H10. Col. left. Between. assert(OS A A' B C'). apply(one_side_transitivity _ _ _ C); auto. assert(OS C C' B A'). apply(one_side_transitivity _ _ _ A); auto. apply invert_one_side in H15. apply invert_one_side in H16. assert(HP:= col_one_side_out A' A B C' H2 H15). assert(Out C' B A'). apply(col_one_side_out C' C B A'); Col. unfold Out in *. spliter. induction H19. Between. induction H22. Between. apply False_ind. apply H18. apply (between_equality _ _ B); Between. spliter. induction(eq_dec_points A C). subst C. apply between_identity in H. subst B. clean_duplicated_hyps. clean_trivial_hyps. apply l8_8 in H4. contradiction. assert(Col B C' C). ColR. apply per_not_col in H4; auto. contradiction. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel