∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddMonoid M] {p : AddMonoidAlgebra R M → Prop}
  (x : AddMonoidAlgebra R M),
  (∀ (m : M), p ((AddMonoidAlgebra.of R M) (Multiplicative.ofAdd m))) →
    (∀ (x y : AddMonoidAlgebra R M), p x → p y → p (x + y)) →
      (∀ (r : R) (x : AddMonoidAlgebra R M), p x → p (r • x)) → p x