proposition: Lemma all_one_side_par_strict : forall A B C D, C <> D -> (forall P, Col C D P -> OS A B C P) -> Par_strict A B C D.
proof: Proof. intros. split. apply os__coplanar, H0; Col. intro. ex_and H1 X. assert(HH:= H0 X (col_permutation_1 _ _ _ H2) ). ex_and HH M. unfold TS in H4. spliter. contradiction. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles