proposition: Lemma sams_lea2_suma2__conga123 : forall A B C D E F G H I A' B' C' D' E' F', LeA A B C A' B' C' -> LeA D E F D' E' F' -> 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 -> CongA A B C A' B' C'.
proof: Proof. intros A B C D E F G H I A' B' C' D' E' F' HleaB HleaE Hisi' Hsuma Hsuma'. assert_diffs. apply (sams2_suma2__conga123 _ _ _ _ _ _ D E F G H I); auto. apply (sams_lea2__sams _ _ _ _ _ _ A' B' C' D' E' F'); auto. apply (sams_lea2__sams _ _ _ _ _ _ A' B' C' D' E' F'); Lea. assert (Haux := ex_suma A' B' C' D E F). destruct Haux as [G' [H' [I']]]; auto. apply (conga3_suma__suma A' B' C' D E F G' H' I'); try (apply conga_refl); auto. apply lea_asym. apply (sams_lea456_suma2__lea A' B' C' D E F _ _ _ D' E' F'); auto. apply (sams_lea123_suma2__lea A B C D E F _ _ _ A' B' C'); auto. apply (sams_lea2__sams _ _ _ _ _ _ A' B' C' D' E' F'); Lea. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles