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 Rmult    /Coq/Reals/Rdefinitions/Rmult.con
alias R1        /Coq/Reals/Rdefinitions/R1.con
alias R0        /Coq/Reals/Rdefinitions/R0.con
alias R        /Coq/Reals/Rdefinitions/R.con
alias eqT	/Coq/Init/Logic_Type/eqT.ind#1/1
alias not      /Coq/Init/Logic/not.con


//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 ok
!x:R.!y:R.(Rge x y) -> (Rlt (Rplus y R1) (Rplus x (Rplus R1 R1)))

/Coq/fourier/Fourier_util/Rfourier_not_ge_lt.con

/Coq/Init/Logic/False.ind#1/1

(Rle (Rplus (Rmult (Rmult R1 (Rinv R1)) (Rplus x (Rplus R1 R1))) (Rmult (Rmult R1 (Rinv R1)) y)) (Rplus (Rmult (Rmult R1 (Rinv R1)) (Rplus y R1)) (Rmult (Rmult R1 (Rinv R1)) x)))

/Coq/fourier/Fourier_util/Rnot_le_le.con

t1=(Rplus (Rmult (Rmult R1 (Rinv R1)) (Rplus x (Rplus R1 R1))) (Rmult (Rmult R1 (Rinv R1)) y))
t2=(Rplus (Rmult (Rmult R1 (Rinv R1)) (Rplus y R1)) (Rmult (Rmult R1 (Rinv R1)) x))
tc=(Rmult (Ropp R1) (Rinv R1))

rewrite=(eqT R (Rminus (Rplus (Rmult (Rmult R1 (Rinv R1)) (Rplus y R1)) (Rmult (Rmult R1 (Rinv R1)) x))
 (Rplus (Rmult (Rmult R1 (Rinv R1)) (Rplus x (Rplus R1 R1))) (Rmult (Rmult R1 (Rinv R1)) y))) (Rmult (Ropp R1) (Rinv 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 ok
!x:R.!y:R.(eqT 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))