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