Module Micromega_plugin.CertificateSource

q_cert_of_pos prf converts a Sos proof into a rational Coq proof

z_cert_of_pos prf converts a Sos proof into an integer Coq proof

lia depth sys generates an unsat proof for the linear constraints in sys.

nlia depth sys generates an unsat proof for the non-linear constraints in sys. The solver is incomplete -- the problem is undecidable

linear_prover_with_cert depth sys generates an unsat proof for the linear constraints in sys. Over the rationals, the solver is complete.

nlinear depth sys generates an unsat proof for the non-linear constraints in sys. The solver is incompete -- the problem is decidable.