proposition: Lemma bet_suma__suppa : forall A B C D E F G H I, SumA A B C D E F G H I -> Bet G H I -> SuppA A B C D E F.
proof: Proof. intros A B C D E F G H I [A' [HConga1 [_ [_ HConga2]]]] HBet. assert_diffs. split; auto. exists A'. split; CongA. apply (bet_conga__bet G H I); CongA. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles