proposition: Lemma suma_suppa2__suma : forall A B C D E F G H I A' B' C' D' E' F', SuppA A B C A' B' C' -> SuppA D E F D' E' F' -> SumA A B C D E F G H I -> SumA A' B' C' D' E' F' G H I.
proof: Proof. intros A B C D E F G H I A' B' C' D' E' F' [_ [A0 []]] [_ [D0 []]] HSuma. assert_diffs. apply (conga3_suma__suma A0 B C D0 E F G H I); CongA. apply bet2_suma__suma with A D; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles