proposition: Lemma nsams__obtuse : forall A B C, A <> B -> B <> C -> ~ SAMS A B C A B C -> Obtuse A B C.
proof: Proof. intros A B C HAB HBC HNIsi. elim(angle_partition A B C); auto. - intro. exfalso. apply HNIsi. apply acute__sams; auto. - intro HUn. destruct HUn; auto. exfalso. apply HNIsi. assert(HA' := symmetric_point_construction A B). assert(HNCol : ~ Col A B C) by (apply per_not_col; auto). destruct HA' as [A']. assert_diffs. repeat split; auto. right; intro; Col. exists A'. split. apply conga_right_comm; apply conga_sym; apply l11_18_1; Between; Perp. split. { apply l9_9. apply bet__ts; Between; Col. } split; Cop. intros [_ [HNCol']]; apply HNCol'; Col. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles