{M : Type u} →
  [toAddSemigroup : AddSemigroup M] →
    [toZero : Zero M] →
      (∀ (a : M), 0 + a = a) →
        (∀ (a : M), a + 0 = a) →
          (nsmul : ℕ → M → M) →
            autoParam (∀ (x : M), nsmul 0 x = 0) AddMonoid.nsmul_zero._autoParam →
              autoParam (∀ (n : ℕ) (x : M), nsmul (n + 1) x = nsmul n x + x) AddMonoid.nsmul_succ._autoParam →
                AddMonoid M