proposition: Lemma sams_lea123_suma2__lea : forall A B C D E F G H I A' B' C' G' H' I', LeA A B C A' B' C' -> SAMS A' B' C' D E F -> SumA A B C D E F G H I -> SumA A' B' C' D E F G' H' I' -> LeA G H I G' H' I'.
proof: Proof. intros A B C D E F G H I A' B' C'. intros. apply (sams_lea456_suma2__lea D E F A B C _ _ _ A' B' C'); SumA. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles