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