Ajout d'une syntaxe pour Reals.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@937 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 36 insertions, 0 deletions

diff --git a/theories/Reals/Rdefinitions.v b/theories/Reals/Rdefinitions.v
new file mode 100644
index 000000000..ecaa7b4ca
--- /dev/null
+++ b/theories/Reals/Rdefinitions.v
@@ -0,0 +1,36 @@
+(* $Id$ *)
+
+
+(*********************************************************)
+(*           Definitions for the axiomatization          *)
+(*                                                       *)
+(*********************************************************)
+
+Require Export ZArith.
+Require Export TypeSyntax.
+
+Parameter R:Type.
+Parameter R0:R.
+Parameter R1:R.
+Parameter Rplus:R->R->R.
+Parameter Rmult:R->R->R.
+Parameter Ropp:R->R.
+Parameter Rinv:R->R. 
+Parameter Rlt:R->R->Prop.    
+Parameter up:R->Z.
+(*********************************************************)
+
+(**********)
+Definition Rgt:R->R->Prop:=[r1,r2:R](Rlt r2 r1).
+
+(**********)
+Definition Rle:R->R->Prop:=[r1,r2:R]((Rlt r1 r2)\/(r1==r2)).
+
+(**********)
+Definition Rge:R->R->Prop:=[r1,r2:R]((Rgt r1 r2)\/(r1==r2)).
+
+(**********)
+Definition Rminus:R->R->R:=[r1,r2:R](Rplus r1 (Ropp r2)).
+
+(**********)
+Definition Rdiv:R->R->R:=[r1,r2:R](Rmult r1 (Rinv r2)).