proposition: Lemma par_strict_all_one_side : forall A B C D, Par_strict A B C D -> (forall P, Col C D P -> OS A B C P).
proof: Proof. intros. eapply par_strict_one_side. apply H. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles