proposition: Lemma acute_suma__nbet : forall A B C D E F, Acute A B C -> SumA A B C A B C D E F -> ~ Bet D E F.
proof: Proof. intros A B C D E F Hacute HSuma. assert_diffs. intro. apply (nlta A B C). apply acute_per__lta; auto. apply (bet_suma__per _ _ _ D E F); auto. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles