validsdp

Proving multivariate inequalities in Coq using SDP solvers and floating-point arithmetic