proposition: Lemma perp2_preserves_bet13 : forall O B C B' C', Bet B O C -> Col O B' C' -> ~Col O B B' -> Perp2 B C' C B' O -> Bet B' O C'.
proof: Proof. intros. induction(eq_dec_points C' O). subst. Between. induction(eq_dec_points B' O). subst. Between. assert(B <> O). intro. subst B. apply H1. Col. assert(B' <> O). intro. subst B'. apply H1. Col. assert(Col B O C). apply bet_col. Between. induction(eq_dec_points B C). subst C. apply between_identity in H. contradiction. assert(Par B C' C B'). unfold Perp2 in H2. ex_and H2 X. ex_and H9 Y. assert(Coplanar X Y B C). exists O. left. split; Col. assert(Coplanar X Y C' B'). exists O. left. split; Col. apply (l12_9 _ _ _ _ X Y); Perp. induction(col_dec C' X Y). exists B'. left. assert_diffs. split; ColR. apply coplanar_trans_1 with C'; Cop. induction(col_dec B X Y). exists C. left. assert_diffs. split; ColR. apply coplanar_trans_1 with B; Cop. assert(Par_strict B C' C B'). induction H9. assumption. spliter. apply False_ind. apply H1. ColR. assert(C<> O). intro. subst C. assert(Par_strict B C' O C'). apply(par_strict_col_par_strict _ _ _ B'); auto. apply H11. exists C'. Col. assert(B' <> O). intro. subst B'. assert(Par_strict B C' O B). apply(par_strict_col_par_strict _ _ _ C); auto. apply par_strict_right_comm. assumption. Col. apply H12. exists B. split; Col. unfold Perp2 in H2. ex_and H2 X. ex_and H13 Y. assert(X <> Y). apply perp_distinct in H13. tauto. induction(col_dec X Y B). assert(Col X Y C). ColR. apply(per13_preserves_bet_inv B' O C' C B); Between. Col. apply perp_in_per. induction(eq_dec_points X C). subst X. assert(Perp C O B' C). apply(perp_col _ Y); Perp. ColR. apply perp_perp_in in H18. Perp. assert(Perp X C C B'). apply(perp_col _ Y); Perp. assert(Perp C O B' C). apply(perp_col _ X); Perp. ColR. apply perp_perp_in in H20. Perp. apply perp_in_per. induction(eq_dec_points X B). subst X. assert(Perp B O C' B). apply(perp_col _ Y); Perp. ColR. apply perp_perp_in in H18. Perp. assert(Perp X B C' B). apply(perp_col _ Y); Perp. assert(Perp B O C' B). apply(perp_col _ X); Perp. ColR. apply perp_perp_in in H20. Perp. assert(HP1:=l8_18_existence X Y B H16). ex_and HP1 B0. assert(~Col X Y C). intro. apply H16. ColR. assert(HP1:=l8_18_existence X Y C H19). ex_and HP1 C0. assert(B0 <> O). intro. subst B0. assert(Par B O B C'). apply(l12_9 B O B C' X Y); Perp; Cop. induction H22. apply H22. exists B. split; Col. spliter. apply H1. ColR. assert(C0 <> O). intro. subst C0. assert(Par C O C B'). apply(l12_9 C O C B' X Y); Perp; Cop. induction H23. apply H23. exists C. split; Col. spliter. apply H1. ColR. assert(Bet B0 O C0). apply(per13_preserves_bet B O C B0 C0); auto. Between. ColR. apply perp_in_per. induction(eq_dec_points X B0). subst X. assert(Perp B0 O B B0). apply(perp_col _ Y); Perp. Col. apply perp_perp_in in H24. Perp. assert(Perp X B0 B B0). apply(perp_col _ Y); Perp. assert(Perp B0 O B B0). apply (perp_col _ X); Perp. ColR. apply perp_perp_in in H26. Perp. apply perp_in_per. induction(eq_dec_points X C0). subst X. assert(Perp C0 O C C0). apply(perp_col _ Y); Perp. Col. apply perp_perp_in in H24. Perp. assert(Perp X C0 C C0). apply(perp_col _ Y); Perp. assert(Perp C0 O C C0). apply (perp_col _ X); Perp. ColR. apply perp_perp_in in H26. Perp. induction(eq_dec_points C' B0). subst B0. assert(B' = C0). apply bet_col in H24. apply (l6_21 C' O C C0); Col. assert(Par C B' C C0). apply(l12_9 C B' C C0 X Y); Perp; Cop. induction H25. apply False_ind. apply H25. exists C. split; Col. spliter. Col. intro. apply H1. ColR. intro. subst C0. apply H1. ColR. apply(cop_perp2__col C C0 B' X Y); Perp. exists C0. left. split; Col. subst C0. Between. assert(B' <> C0). intro. subst C0. apply H25. apply (l6_21 B' O B B0); Col. intro. subst B0. Col. assert(Par B C' B B0). apply(l12_9 B C' B B0 X Y); Perp; Cop. induction H26. apply False_ind. apply H26. exists B. split; Col. spliter. Col. assert(Col C C0 B'). apply(cop_perp2__col C C0 B' X Y); Perp. exists C0. left. split; Col. assert(Col B B0 C'). apply(cop_perp2__col B B0 C' X Y); Perp. exists B0. left. split; Col. apply(per13_preserves_bet_inv B' O C' C0 B0); Between. Col. apply perp_in_per. induction(eq_dec_points X C0). subst X. assert(Perp C0 O C B'). apply (perp_col _ Y); Perp. Col. assert(Perp B' C0 C0 O). apply(perp_col _ C); Perp. Col. apply perp_comm in H30. apply perp_perp_in in H30. Perp. assert(Perp X C0 C B'). apply(perp_col _ Y); Perp. assert(Perp C0 O C B'). apply (perp_col _ X); Perp. ColR. assert(Perp B' C0 C0 O). apply(perp_col _ C); Perp. Col. apply perp_comm in H32. apply perp_perp_in in H32. Perp. apply perp_in_per. assert(Perp C' B0 X Y). apply (perp_col _ B); Perp. Col. induction (eq_dec_points X O). subst X. assert(Perp O B0 B0 C'). apply(perp_col _ Y);Perp. apply perp_comm in H30. apply perp_perp_in in H30. Perp. assert(Perp X O C' B0). apply(perp_col _ Y); Perp. Col. assert(Perp O B0 B0 C'). apply(perp_col _ X); Perp. ColR. apply perp_comm in H32. apply perp_perp_in in H32. Perp. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel