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: Raxioms.v,v 1.20.2.1 2004/07/16 19:31:12 herbelin Exp $ i*)
35 (*#********************************************************)
37 (*#* Axiomatisation of the classical reals *)
39 (*#********************************************************)
41 include "ZArith/ZArith_base.ma".
43 include "Reals/Rdefinitions.ma".
46 Open Local Scope R_scope.
49 (*#********************************************************)
53 (*#********************************************************)
55 (*#********************************************************)
59 (*#********************************************************)
63 inline procedural "cic:/Coq/Reals/Raxioms/Rplus_comm.con".
66 Hint Resolve Rplus_comm: real.
71 inline procedural "cic:/Coq/Reals/Raxioms/Rplus_assoc.con".
74 Hint Resolve Rplus_assoc: real.
79 inline procedural "cic:/Coq/Reals/Raxioms/Rplus_opp_r.con".
82 Hint Resolve Rplus_opp_r: real v62.
87 inline procedural "cic:/Coq/Reals/Raxioms/Rplus_0_l.con".
90 Hint Resolve Rplus_0_l: real.
93 (*#**********************************************************)
95 (*#* Multiplication *)
97 (*#**********************************************************)
101 inline procedural "cic:/Coq/Reals/Raxioms/Rmult_comm.con".
104 Hint Resolve Rmult_comm: real v62.
109 inline procedural "cic:/Coq/Reals/Raxioms/Rmult_assoc.con".
112 Hint Resolve Rmult_assoc: real v62.
117 inline procedural "cic:/Coq/Reals/Raxioms/Rinv_l.con".
120 Hint Resolve Rinv_l: real.
125 inline procedural "cic:/Coq/Reals/Raxioms/Rmult_1_l.con".
128 Hint Resolve Rmult_1_l: real.
133 inline procedural "cic:/Coq/Reals/Raxioms/R1_neq_R0.con".
136 Hint Resolve R1_neq_R0: real.
139 (*#********************************************************)
141 (*#* Distributivity *)
143 (*#********************************************************)
147 inline procedural "cic:/Coq/Reals/Raxioms/Rmult_plus_distr_l.con".
150 Hint Resolve Rmult_plus_distr_l: real v62.
153 (*#********************************************************)
157 (*#********************************************************)
159 (*#********************************************************)
163 (*#********************************************************)
167 inline procedural "cic:/Coq/Reals/Raxioms/total_order_T.con".
169 (*#********************************************************)
173 (*#********************************************************)
177 inline procedural "cic:/Coq/Reals/Raxioms/Rlt_asym.con".
181 inline procedural "cic:/Coq/Reals/Raxioms/Rlt_trans.con".
185 inline procedural "cic:/Coq/Reals/Raxioms/Rplus_lt_compat_l.con".
189 inline procedural "cic:/Coq/Reals/Raxioms/Rmult_lt_compat_l.con".
192 Hint Resolve Rlt_asym Rplus_lt_compat_l Rmult_lt_compat_l: real.
195 (*#*********************************************************)
197 (*#* Injection from N to R *)
199 (*#*********************************************************)
203 inline procedural "cic:/Coq/Reals/Raxioms/INR.con" as definition.
206 Arguments Scope INR [nat_scope].
209 (*#*********************************************************)
211 (*#* Injection from [Z] to [R] *)
213 (*#*********************************************************)
217 inline procedural "cic:/Coq/Reals/Raxioms/IZR.con" as definition.
220 Arguments Scope IZR [Z_scope].
223 (*#*********************************************************)
225 (*#* [R] Archimedian *)
227 (*#*********************************************************)
231 inline procedural "cic:/Coq/Reals/Raxioms/archimed.con".
233 (*#*********************************************************)
237 (*#*********************************************************)
241 inline procedural "cic:/Coq/Reals/Raxioms/is_upper_bound.con" as definition.
245 inline procedural "cic:/Coq/Reals/Raxioms/bound.con" as definition.
249 inline procedural "cic:/Coq/Reals/Raxioms/is_lub.con" as definition.
253 inline procedural "cic:/Coq/Reals/Raxioms/completeness.con".