proposition: Lemma l13_8 : forall O P Q U V, U <> O -> V <> O -> Col O P Q -> Col O U V -> Per P U O -> Per Q V O -> (Out O P Q <-> Out O U V).
proof: Proof. intros. induction(eq_dec_points P U). subst P. assert(Col Q V O). ColR. assert(HH:= l8_9 Q V O H4 H5). induction HH. subst Q. tauto. subst V. tauto. assert(Q <> V). intro. subst Q. assert(HH:= per_not_col P U O H5 H H3). apply HH. ColR. split. intro. unfold Out in H7. spliter. induction H9. assert(HH:= per23_preserves_bet O P Q U V). repeat split; auto. left. apply(per23_preserves_bet O P Q U V); auto. Perp. Perp. repeat split; auto. right. apply(per23_preserves_bet O Q P V U); Col. Perp. Perp. intro. unfold Out in H7. spliter. repeat split. intro. subst P. apply l8_8 in H3. contradiction. intro. subst Q. apply l8_8 in H4. contradiction. induction H9. left. apply(per23_preserves_bet_inv O P Q U V); Perp. right. apply(per23_preserves_bet_inv O Q P V U); Perp. Col. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel