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
8 !x:R.!y:R.(Rle x y) -> (Rge (Rplus y R1) (Rminus x R1))