proposition: Lemma acute2_suma__nbet : forall A B C D E F G H I, Acute A B C -> Acute D E F -> SumA A B C D E F G H I -> ~ Bet G H I.
proof: Proof. assert (Haux : forall A B C D E F G H I, Acute A B C -> LeA D E F A B C -> SumA A B C D E F G H I -> ~ Bet G H I). { intros A B C D E F G H I HAcute HLea HSuma HBet. assert_diffs. destruct (ex_suma A B C A B C) as [A' [B' [C']]]; auto. apply (acute_suma__nbet A B C A' B' C'); trivial. apply (bet_lea__bet G H I); [apply HBet|]. apply sams_lea2_suma2__lea with A B C D E F A B C A B C; trivial. apply lea_refl; auto. apply acute__sams, HAcute. } intros A B C D E F G H I HAcute1 HAcute2 HSuma. assert_diffs. destruct (lea_total A B C D E F); auto. apply suma_sym in HSuma; apply (Haux D E F A B C); assumption. apply (Haux A B C D E F); assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles