proposition: Lemma l12_6 : forall A B C D, Par_strict A B C D -> OS A B C D.
proof: Proof. intros. unfold Par_strict in H. spliter. assert(HH:= cop_nts__os A B C D). apply HH. assumption. intro. apply H0. exists C;Col. intro. apply H0. exists D;Col. intro. apply H0. unfold TS in H1. spliter. ex_and H3 T. exists T. split; Col. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles