proposition: Lemma perp2_preserves_bet23 : forall O A B A' B', Bet O A B -> Col O A' B' -> ~Col O A A' -> Perp2 A A' B B' O -> Bet O A' B'.
proof: Proof. intros. assert(HD1: A <> A'). intro. subst A'. apply H1. Col. induction(eq_dec_points A' B'). subst B'. Between. assert(A <> B). intro. subst B. unfold Perp2 in H2. ex_and H2 X. ex_and H4 Y. assert(Col A A' B'). apply(cop_perp2__col A A' B' X Y); Perp. exists O. left. split; Col. apply H1. ColR. assert(Par A A' B B'). unfold Perp2 in H2. ex_and H2 X. ex_and H5 Y. assert(Coplanar X Y A B). exists O. left. split; Col. apply (l12_9 _ _ _ _ X Y); Perp. induction(col_dec B X Y). exists A. left. assert_diffs. split; ColR. apply coplanar_trans_1 with B; Cop. induction(col_dec A X Y). exists B. left. assert_diffs. split; ColR. apply coplanar_trans_1 with A; Cop. exists O. left. split; Col. induction H5. assert(OS A A' B B'). apply l12_6; Par. assert(TS A A' O B). repeat split; Col. intro. apply H5. exists B. split; Col. exists A. split; Col. assert(TS A A' B' O). apply( l9_8_2 A A' B B' O); auto. apply l9_2. auto. unfold TS in H8. spliter. ex_and H10 T. assert(T = A'). apply (l6_21 A A' O B'); Col. intro. subst B'. apply between_identity in H11. subst T. contradiction. subst T. Between. spliter. apply False_ind. apply H1. ColR. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel