∀ {G : Type u_1} {G' : Type u_2} {G'' : Type u_3} [inst : Group G] [inst_1 : Group G'] [inst_2 : Group G'']
  {f : G →* G'} {f' : G' →* G''} [Finite G] [IsZGroup G] [IsZGroup G''],
  f'.ker ≤ f.range → (Nat.card G).Coprime (Nat.card G'') → IsZGroup G'