proposition: Lemma acute_per_suma__nbet : forall A B C D E F G H I, A <> B -> B <> C -> Per A B C -> Acute D E F -> SumA A B C D E F G H I -> ~ Bet G H I.
proof: Proof. intros A B C D E F G H I HAB HBC HPer HAcute HSuma HBet. assert_diffs. apply (nlta G H I). apply sams_lea_lta456_suma2__lta with A B C D E F A B C A B C; Lea. apply per2__sams; auto. apply bet_per2__suma; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles