∀ {M₁ : Type u_2} {M₂ : Type u_1} [inst : Add M₂] [inst_1 : Zero M₂] [inst_2 : SMul ℕ M₂] [inst_3 : Neg M₂]
  [inst_4 : Sub M₂] [inst_5 : SubNegMonoid M₁] (f : M₁ → M₂) (hf : Function.Surjective f) (zero : f 0 = 0)
  (add : ∀ (x y : M₁), f (x + y) = f x + f y),
  (∀ (x : M₁), f (-x) = -f x) →
    (∀ (x y : M₁), f (x - y) = f x - f y) →
      ∀ (nsmul : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x) (x y : M₁), f x - f y = f x + -f y