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