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))