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