proposition: Lemma conga3_suma__suma : forall A B C D E F G H I A' B' C' D' E' F' G' H' I', SumA A B C D E F G H I -> CongA A B C A' B' C' -> CongA D E F D' E' F' -> CongA G H I 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' G' H' I' Hsuma HCongaB HCongaE HCongaH. assert (Hsuma' : SumA D' E' F' A B C G' H' I'). { apply suma_sym. destruct Hsuma as [J [HJ1 [HJ2 [HJ3 HCop]]]]. exists J. split. apply (conga_trans C B J D E F); auto. split; auto. split; auto. apply (conga_trans A B J G H I); auto. } apply suma_sym. destruct Hsuma' as [J [HJ1 [HJ2 [HJ3 HCop]]]]. exists J. split. apply (conga_trans F' E' J A B C); auto. repeat (split; trivial). Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles