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