{M : Type u} →
  (mul : M → M → M) →
    (∀ (a b c : M), a * b * c = a * (b * c)) →
      (one : M) →
        (∀ (a : M), 1 * a = a) →
          (∀ (a : M), a * 1 = a) →
            (npow : ℕ → M → M) →
              autoParam (∀ (x : M), npow 0 x = 1) Monoid.npow_zero._autoParam →
                autoParam (∀ (n : ℕ) (x : M), npow (n + 1) x = npow n x * x) Monoid.npow_succ._autoParam → Monoid M