The nonnegative formal-sum model satisfies induction with inequality

Let $d4c^+$ be the substructure of the formal-sum structure consisting of the nonnegative elements, where nonnegativity is determined by the sign of the sum of the coefficients of the terms having greatest degree in normal form. Here $d4c^+$ is a structure for the language of arithmetic.

Induction-with-inequality hypothesis. The introduced structure $d4c^+$ is a model of $d400(\ne)$.

This gives a proposed model-theoretic property of the formal-sum construction; the supplied text does not indicate whether the assertion has been proved or remains open.