--- /dev/null
+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))