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
+
+(*test real*)
+!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 base1 ok
!x:R.!y:R.(Rle x y) -> (Rge (Rplus y R1) (Rminus x R1))
/Coq/fourier/Fourier_util/Rfourier_not_ge_lt.con
+intros
+
/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)))
+(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))