X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2Fesempi%2Ffourier.cic;fp=helm%2FgTopLevel%2Fesempi%2Ffourier.cic;h=cae3925a7102fc58a1539f7c2a72e6994ff76374;hb=273ed08112cf9470644498dc495d9e60519e5eaa;hp=0000000000000000000000000000000000000000;hpb=50d48fe8a3c70e70bf2f06b60dfa3a6b8c121b6b;p=helm.git

diff --git a/helm/gTopLevel/esempi/fourier.cic b/helm/gTopLevel/esempi/fourier.cic
new file mode 100644
index 000000000..cae3925a7
--- /dev/null
+++ b/helm/gTopLevel/esempi/fourier.cic
@@ -0,0 +1,8 @@
+alias Rge       /Coq/Reals/Rdefinitions/Rge.con
+alias Rle       /Coq/Reals/Rdefinitions/Rle.con
+alias Rplus     /Coq/Reals/Rdefinitions/Rplus.con
+alias Rminus    /Coq/Reals/Rdefinitions/Rminus.con
+alias R1        /Coq/Reals/Rdefinitions/R1.con
+alias R        /Coq/Reals/Rdefinitions/R.con
+
+!x:R.!y:R.(Rle x y) -> (Rge (Rplus y R1) (Rminus x R1))