1 alias Rge /Coq/Reals/Rdefinitions/Rge.con
2 alias Rle /Coq/Reals/Rdefinitions/Rle.con
3 alias Rgt /Coq/Reals/Rdefinitions/Rgt.con
4 alias Rlt /Coq/Reals/Rdefinitions/Rlt.con
5 alias Ropp /Coq/Reals/Rdefinitions/Ropp.con
6 alias Rinv /Coq/Reals/Rdefinitions/Rinv.con
7 alias Rplus /Coq/Reals/Rdefinitions/Rplus.con
8 alias Rminus /Coq/Reals/Rdefinitions/Rminus.con
9 alias Rmult /Coq/Reals/Rdefinitions/Rmult.con
10 alias R1 /Coq/Reals/Rdefinitions/R1.con
11 alias R0 /Coq/Reals/Rdefinitions/R0.con
12 alias R /Coq/Reals/Rdefinitions/R.con
13 alias eqT /Coq/Init/Logic_Type/eqT.ind#1/1
14 alias not /Coq/Init/Logic/not.con
18 !x:R.!y:R.(Rle x y) -> (Rge (Rplus y R1) (Rminus x R1))
21 !x:R.!y:R.(Rlt x y) -> (Rgt (Rplus y R1) (Rminus x R1))
24 !x:R.!y:R.(Rge x y) -> (Rlt (Rplus y R1) (Rplus x (Rplus R1 R1)))
26 /Coq/fourier/Fourier_util/Rfourier_not_ge_lt.con
28 /Coq/Init/Logic/False.ind#1/1
30 (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)))
32 /Coq/fourier/Fourier_util/Rnot_le_le.con
34 t1=(Rplus (Rmult (Rmult R1 (Rinv R1)) (Rplus x (Rplus R1 R1))) (Rmult (Rmult R1 (Rinv R1)) y))
35 t2=(Rplus (Rmult (Rmult R1 (Rinv R1)) (Rplus y R1)) (Rmult (Rmult R1 (Rinv R1)) x))
36 tc=(Rmult (Ropp R1) (Rinv R1))
38 rewrite=(eqT R (Rminus (Rplus (Rmult (Rmult R1 (Rinv R1)) (Rplus y R1)) (Rmult (Rmult R1 (Rinv R1)) x))
39 (Rplus (Rmult (Rmult R1 (Rinv R1)) (Rplus x (Rplus R1 R1))) (Rmult (Rmult R1 (Rinv R1)) y))) (Rmult (Ropp R1) (Rinv R1)))
42 !x:R.!y:R.(Rgt x y) -> (Rle (Rminus y R1) (Rplus x R1))
45 !x:R.!y:R.(Rlt x ( Rplus y R1 ) ) -> (Rge (Rplus y (Rplus R1 R1)) (Rminus x R0))
48 !x:R.!y:R.(eqT R x y) -> (Rgt (Rplus y R1) (Rminus x R1))
50 //test base7 (should fail) ok
51 !x:R.!y:R.(Rlt x y) -> (Rlt (Rplus y R1) (Rminus x R1))