proposition: Lemma obtuse__nsams : forall A B C, Obtuse A B C -> ~ SAMS A B C A B C.
proof: Proof. intros A B C Hobtuse. assert(HA' := symmetric_point_construction A B). destruct HA' as [A']. assert_diffs. intro. apply (nlta A B C). apply (lea123456_lta__lta _ _ _ A' B C). - apply lea_right_comm. apply (sams_chara A); Between. - apply acute_obtuse__lta; auto. apply (bet_obtuse__acute A); Between. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles