∀ {A B : Type u} [inst : AddCommGroup A] [inst_1 : AddCommGroup B] (f : A →+ B) (g : B →+ A) (n : ℤ),
  QuotientAddGroup.homQuotientZSMulOfHom (f.comp g) n =
    (QuotientAddGroup.homQuotientZSMulOfHom f n).comp (QuotientAddGroup.homQuotientZSMulOfHom g n)