+++ /dev/null
-alias Rge /Coq/Reals/Rdefinitions/Rge.con
-alias Rle /Coq/Reals/Rdefinitions/Rle.con
-alias Rgt /Coq/Reals/Rdefinitions/Rgt.con
-alias Rlt /Coq/Reals/Rdefinitions/Rlt.con
-alias Ropp /Coq/Reals/Rdefinitions/Ropp.con
-alias Rinv /Coq/Reals/Rdefinitions/Rinv.con
-alias Rplus /Coq/Reals/Rdefinitions/Rplus.con
-alias Rminus /Coq/Reals/Rdefinitions/Rminus.con
-alias R1 /Coq/Reals/Rdefinitions/R1.con
-alias R0 /Coq/Reals/Rdefinitions/R0.con
-alias R /Coq/Reals/Rdefinitions/R.con
-alias Eq /Coq/Init/Logic_Type/eqT.ind#1/1
-
-//test base1 ok
-!x:R.!y:R.(Rle x y) -> (Rge (Rplus y R1) (Rminus x R1))
-
-//test base2 ok
-!x:R.!y:R.(Rlt x y) -> (Rgt (Rplus y R1) (Rminus x R1))
-
-//test base3 (unification fails)
-!x:R.!y:R.(Rge x y) -> (Rlt (Rplus y R1) (Rplus x (Rplus R1 R1)))
-
-//test base4 ok
-!x:R.!y:R.(Rgt x y) -> (Rle (Rminus y R1) (Rplus x R1))
-
-//test base5 ok
-!x:R.!y:R.(Rlt x ( Rplus y R1 ) ) -> (Rge (Rplus y (Rplus R1 R1)) (Rminus x R0))
-
-//test base6 (unification fails)
-!x:R.!y:R.(Eq R x y) -> (Rgt (Rplus y R1) (Rminus x R1))
-
-//test base7 (should fail) ok
-!x:R.!y:R.(Rlt x y) -> (Rlt (Rplus y R1) (Rminus x R1))
-
-