+
+//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
+
+intros
+
+/Coq/Init/Logic/False.ind#1/1
+
+(not (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))
+
+(t1-t2)=(Rminus
+(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)))
+
+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)))
+
+change=(not (or
+(Rlt R0 (Rmult (Ropp R1) (Rinv R1)))
+(eqT R R0 (Rmult (Ropp R1) (Rinv R1)))
+))
+
+tac2
+/Coq/fourier/Fourier_util/Rnot_lt0.con
+
+//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))
+
+