proposition: Lemma two_sides_cases : forall O P A B, ~ Col O A B -> OS O P A B -> TS O A P B \/ TS O B P A.
proof: Proof. intros. assert(TS O A P B \/ OS O A P B). { apply(cop__one_or_two_sides O A P B); Col. Cop. unfold OS in H0. ex_and H0 R. unfold TS in H0. spliter. Col. } induction H1. left; auto. right. apply l9_31; Side. Qed.
imports: GeoCoq.Meta_theory.Dimension_axioms.upper_dim_2 GeoCoq.Tarski_dev.Ch10_line_reflexivity