proposition: Lemma par_strict_one_side : forall A B C D P, Par_strict A B C D -> Col C D P -> OS A B C P.
proof: Proof. intros A B C D P HPar HCol. destruct (eq_dec_points C P). subst P; apply par_strict_not_col_1 in HPar; apply one_side_reflexivity; Col. apply l12_6, par_strict_col_par_strict with D; trivial. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles