proposition: Lemma bet_suma__sams : forall A B C D E F G H I, SumA A B C D E F G H I -> Bet G H I -> SAMS A B C D E F.
proof: Proof. intros A B C D E F G H I HSuma HBet. destruct HSuma as [A' [HConga1 [HNOS [HCop HConga2]]]]. apply (bet_conga__bet _ _ _ A B A') in HBet; CongA. assert_diffs. repeat split; auto. - elim (bet_dec A B C). { intro HBet'; left. apply (l11_21_a C B A'); trivial. apply l6_2 with A; Between. } intro HNBet; auto. - exists A'; repeat (split; trivial). intros [_ [HNCol _]]; apply HNCol; Col. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles