helm/gTopLevel/esempi/fourier.cic

   1 alias Rge       /Coq/Reals/Rdefinitions/Rge.con
   2 alias Rle       /Coq/Reals/Rdefinitions/Rle.con
   3 alias Rplus     /Coq/Reals/Rdefinitions/Rplus.con
   4 alias Rminus    /Coq/Reals/Rdefinitions/Rminus.con
   5 alias R1        /Coq/Reals/Rdefinitions/R1.con
   6 alias R        /Coq/Reals/Rdefinitions/R.con
   7
   8 !x:R.!y:R.(Rle x y) -> (Rge (Rplus y R1) (Rminus x R1))