proposition: Lemma plgs_one_side : forall A B C D, Parallelogram_strict A B C D -> OS A B C D /\ OS C D A B.
proof: Proof. intros. unfold Parallelogram_strict in H. spliter. induction H0. split. apply l12_6. assumption. apply par_strict_symmetry in H0. apply l12_6. assumption. apply False_ind. spliter. unfold TS in H. spliter. apply H5. Col. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel