1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
19 (*#***********************************************************************)
21 (* v * The Coq Proof Assistant / The Coq Development Team *)
23 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
25 (* \VV/ **************************************************************)
27 (* // * This file is distributed under the terms of the *)
29 (* * GNU Lesser General Public License Version 2.1 *)
31 (*#***********************************************************************)
33 (*i $Id: Rdefinitions.v,v 1.14.2.1 2004/07/16 19:31:12 herbelin Exp $ i*)
35 (*#********************************************************)
37 (*#* Definitions for the axiomatization *)
41 (*#********************************************************)
43 include "ZArith/ZArith_base.ma".
45 inline procedural "cic:/Coq/Reals/Rdefinitions/R.con".
47 (* Declare Scope positive_scope with Key R *)
50 Delimit Scope R_scope with R.
53 (* Automatically open scope R_scope for arguments of type R *)
56 Bind Scope R_scope with R.
59 inline procedural "cic:/Coq/Reals/Rdefinitions/R0.con".
61 inline procedural "cic:/Coq/Reals/Rdefinitions/R1.con".
63 inline procedural "cic:/Coq/Reals/Rdefinitions/Rplus.con".
65 inline procedural "cic:/Coq/Reals/Rdefinitions/Rmult.con".
67 inline procedural "cic:/Coq/Reals/Rdefinitions/Ropp.con".
69 inline procedural "cic:/Coq/Reals/Rdefinitions/Rinv.con".
71 inline procedural "cic:/Coq/Reals/Rdefinitions/Rlt.con".
73 inline procedural "cic:/Coq/Reals/Rdefinitions/up.con".
76 Infix "+" := Rplus : R_scope.
80 Infix "*" := Rmult : R_scope.
84 Notation "- x" := (Ropp x) : R_scope.
88 Notation "/ x" := (Rinv x) : R_scope.
92 Infix "<" := Rlt : R_scope.
95 (*i*******************************************************i*)
99 inline procedural "cic:/Coq/Reals/Rdefinitions/Rgt.con" as definition.
103 inline procedural "cic:/Coq/Reals/Rdefinitions/Rle.con" as definition.
107 inline procedural "cic:/Coq/Reals/Rdefinitions/Rge.con" as definition.
111 inline procedural "cic:/Coq/Reals/Rdefinitions/Rminus.con" as definition.
115 inline procedural "cic:/Coq/Reals/Rdefinitions/Rdiv.con" as definition.
118 Infix "-" := Rminus : R_scope.
122 Infix "/" := Rdiv : R_scope.
126 Infix "<=" := Rle : R_scope.
130 Infix ">=" := Rge : R_scope.
134 Infix ">" := Rgt : R_scope.
138 Notation "x <= y <= z" := ((x <= y)%R /\ (y <= z)%R) : R_scope.
142 Notation "x <= y < z" := ((x <= y)%R /\ (y < z)%R) : R_scope.
146 Notation "x < y < z" := ((x < y)%R /\ (y < z)%R) : R_scope.
150 Notation "x < y <= z" := ((x < y)%R /\ (y <= z)%R) : R_scope.