proposition: Lemma bet_per_suma__per123 : forall A B C D E F G H I, Per D E F -> Bet G H I -> SumA A B C D E F G H I -> Per A B C.
proof: Proof. intros A B C D E F G H I HPer HBet HSuma. apply (bet_per_suma__per456 D E F _ _ _ G H I); SumA. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles