This paper presents a theory of non-linear integer/real arithmetic and
algorithms for reasoning about this theory. The theory can be conceived of as an
extension of linear integer/real arithmetic with a weakly-axiomatized
multiplication symbol, which retains many of the desirable algorithmic
properties of linear arithmetic. In particular, we show that the
\textit{conjunctive} fragment of the theory can be effectively manipulated
(analogously to the usual operations on convex polyhedra, the conjunctive
fragment of linear arithmetic). As a result, we can solve the following
consequence-finding problem: \textit{given a ground formula $F$, find the strongest
conjunctive formula that is entailed by $F$}. As an application of
consequence-finding, we give a loop invariant generation algorithm that is
monotone with respect to the theory and (in a sense) complete. Experiments show that the invariants
generated from the consequences are effective for proving safety properties of
programs that require non-linear reasoning.