∀ {M : Type u_2} {R : Type u_6} [inst : Semiring R] [inst_1 : AddZeroClass M],
  AddMonoidAlgebra.nonAssocSemiring =
    { toNonUnitalNonAssocSemiring := AddMonoidAlgebra.nonUnitalNonAssocSemiring, toOne := AddMonoidAlgebra.zero,
      one_mul := ⋯, mul_one := ⋯, natCast := fun n => AddMonoidAlgebra.single 0 ↑n, natCast_zero := ⋯,
      natCast_succ := ⋯ }