proposition: Lemma conga_sams_nos__nts : forall A B C D E F J, SAMS A B C D E F -> CongA C B J D E F -> ~ OS B C A J -> ~ TS A B C J.
proof: Proof. intros A B C D E F J HIsi HConga. apply sams_nos__nts. assert_diffs. apply (conga2_sams__sams A B C D E F); CongA. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles