∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddMonoid M],
  AddMonoidAlgebra.semiring =
    { toNonUnitalSemiring := AddMonoidAlgebra.nonUnitalSemiring, toOne := AddMonoidAlgebra.nonAssocSemiring.toOne,
      one_mul := ⋯, mul_one := ⋯, toNatCast := AddMonoidAlgebra.nonAssocSemiring.toNatCast, natCast_zero := ⋯,
      natCast_succ := ⋯, npow := npowRecAuto, npow_zero := ⋯, npow_succ := ⋯ }