proposition: Lemma nbet_sams_suma__acute : forall A B C D E F, ~ Bet D E F -> SAMS A B C A B C -> SumA A B C A B C D E F -> Acute A B C.
proof: Proof. intros A B C D E F HNBet HIsi HSuma. assert_diffs. elim(angle_partition A B C); auto. intro HUn. exfalso. destruct HUn. - apply HNBet. apply (per2_suma__bet A B C A B C); auto. - assert(~ SAMS A B C A B C); auto. apply obtuse__nsams; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles