proposition: Lemma os_ts__sams : forall A B C P, TS B P A C -> OS A B P C -> SAMS A B P P B C.
proof: Proof. intros A B C P HTS HOS. assert_diffs. repeat split; auto. right; intro; apply (one_side_not_col123 A B P C); Col. exists C. split; CongA. repeat split; Side; Cop. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles