{K : Type u} →
  (add : K → K → K) →
    (∀ (a b c : K), a + b + c = a + (b + c)) →
      (zero : K) →
        (∀ (a : K), 0 + a = a) →
          (∀ (a : K), a + 0 = a) →
            (nsmul : ℕ → K → K) →
              (∀ (x : K), nsmul 0 x = 0) → (∀ (n : ℕ) (x : K), nsmul (n + 1) x = nsmul n x + x) → (K → K) → K → K → K