  We present a proof-producing integration of ACL2 and Imandra for proving
nonlinear inequalities. This leverages a new Imandra interface exposing its
nonlinear decision procedures. The reasoning takes place over the reals, but
the proofs produced are valid over the rationals and may be run in both ACL2
and ACL2(r). The ACL2 proofs Imandra constructs are extracted from
Positivstellensatz refutations, a real algebraic analogue of the
Nullstellensatz, and are found using convex optimization.
