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
alias or /Coq/Init/Logic/or.ind#1/1

!x:R.
(Rlt (Rmult(Ropp x)R1)
R0)
->(Rlt R0 x)

// test 3x4 -> 35''
!x:R.!y:R.!z:R.
(Rge
(Rplus
 (Rmult (Ropp (Rplus R1 R1)) x) (Rplus 
   (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) y) (Rplus 
     (Rmult (Rplus R1 (Rplus R1 R1)) z) R1)
)) R0)
->  
(Rge
(Rplus
 (Rmult (Ropp (Rplus R1 (Rplus R1 R1))) x) (Rplus 
   (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) y) (Rplus 
      R1 (Rplus R1 R1))
)) R0)
->  
(Rgt
(Rplus
  x (Rplus 
   (Rmult (Rplus R1 R1) y) (Ropp z) )
) R0)
-> 
(Rgt
(Rplus
 (Rmult (Rplus R1 (Rplus R1 R1)) x) (Rplus 
   z (Ropp R1))
) R0)

-> (Rlt z R1)

// test 6x6 -> 

!x:R.!y:R.!z:R.!t:R.!u:R.!v:R.
(Rgt
(Rplus (Ropp x) (Rplus y (Rplus z (Rplus t (Rplus u (Rplus v (Rplus R1 R1)))))))
  R0)
->
(Rgt
(Rplus x (Rplus (Ropp y) (Rplus (Ropp z) (Rplus (Ropp t) (Rplus (Ropp u) (Rplus R1 R1))))))
  R0)
->
(Rgt
(Rplus y (Rplus (Ropp z) (Rplus t (Rplus u (Rplus R1 R1)))))
  R0)
->
(Rgt
(Rplus y (Rplus z (Rplus (Ropp t) (Rplus (Ropp (Rmult (Rplus R1 R1)v)) (Rplus R1 R1)))))
  R0)
->
(Rgt
(Rplus y (Rplus z (Rplus t (Rplus (Ropp u) (Rplus R1 R1)))))
  R0)
->
(Rlt
(Rplus (Rmult (Rplus R1 R1) x) (Rplus v y))
  R0)
-> (Rlt (Rmult (Rplus R1 R1) x) R0)






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

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