proposition: Lemma sams_nos__nts : forall A B C J, SAMS A B C C B J -> ~ OS B C A J -> ~ TS A B C J.
proof: Proof. intros A B C J HIsi HNOS HTS. destruct HIsi as [_ [HUn [J' [HConga [HNOS' [HNTS HCop]]]]]]. assert (Coplanar C B J J'). apply coplanar_trans_1 with A; Cop. apply two_sides_not_col in HTS; Col. destruct (conga_cop__or_out_ts C B J J') as [HOut|HTS1]; CongA. - apply HNTS. apply l9_2, l9_8_2 with J; Side. apply invert_one_side, out_one_side; trivial. destruct HTS as [_ []]; Col. - destruct HTS as [HNCol1 [HNCol2 _]]. assert_diffs. absurd (OS B C J J'); Side. destruct HTS1 as [HNCol _]. assert (~ Col C B J') by (apply (ncol_conga_ncol C B J); Col; CongA). exists A; split; apply cop_nos__ts; Col; Side. apply coplanar_trans_1 with J'; Col; Cop. Cop. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles