fourier

The conclusion of the current sequent must be a linear inequation over real numbers taken from standard library of Coq. Moreover the inequations in the hypotheses must imply the inequation in the conclusion of the current sequent.

It closes the current sequent by applying the Fourier method.

None.