X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Fmatita%2Fdocs%2Fmanual%2Ftac_fourier.html;h=506295b4601a3a28bff5d527435471f282548f20;hb=f64e7e9e24f63a926191f08c6e36ef6763718127;hp=10f29a1e238fc25dfb70a3d937cc1dc1cfe72df2;hpb=7e374b23b0990d58217467b73e518e59781cb67d;p=helm.git diff --git a/helm/www/matita/docs/manual/tac_fourier.html b/helm/www/matita/docs/manual/tac_fourier.html index 10f29a1e2..506295b46 100644 --- a/helm/www/matita/docs/manual/tac_fourier.html +++ b/helm/www/matita/docs/manual/tac_fourier.html @@ -1,6 +1,6 @@ -fourier

fourier

fourier

+fourier

fourier

fourier

Pre-conditions:

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