diff options
| author | desmettr | 2003-01-16 12:48:05 +0000 |
|---|---|---|
| committer | desmettr | 2003-01-16 12:48:05 +0000 |
| commit | 037beacda5dcc3a772ef54570abab6c103931da2 (patch) | |
| tree | 3345cefc0073da54b3be529418aab7a7c70e4a08 | |
| parent | 77a0d61c489dba03cab01ae6b4058cd2ebe7a843 (diff) | |
Renommage de RealsB en Rbase
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3508 85f007b7-540e-0410-9357-904b9bb8a0f7
52 files changed, 245 insertions, 1845 deletions
@@ -38,10 +38,10 @@ kernel/indtypes.cmi: kernel/declarations.cmi kernel/entries.cmi \ kernel/univ.cmi kernel/inductive.cmi: kernel/declarations.cmi kernel/environ.cmi \ kernel/names.cmi kernel/term.cmi kernel/univ.cmi -kernel/mod_typing.cmi: kernel/declarations.cmi kernel/entries.cmi \ - kernel/environ.cmi kernel/modops.cmi: kernel/declarations.cmi kernel/entries.cmi \ kernel/environ.cmi kernel/names.cmi kernel/univ.cmi lib/util.cmi +kernel/mod_typing.cmi: kernel/declarations.cmi kernel/entries.cmi \ + kernel/environ.cmi kernel/names.cmi: lib/pp.cmi lib/predicate.cmi kernel/reduction.cmi: kernel/environ.cmi kernel/sign.cmi kernel/term.cmi \ kernel/univ.cmi @@ -61,9 +61,6 @@ kernel/typeops.cmi: kernel/entries.cmi kernel/environ.cmi kernel/names.cmi \ kernel/univ.cmi: kernel/names.cmi lib/pp.cmi lib/bignat.cmi: lib/pp.cmi lib/pp.cmi: lib/pp_control.cmi -lib/rtree.cmi: lib/pp.cmi -lib/system.cmi: lib/pp.cmi -lib/util.cmi: lib/pp.cmi library/declare.cmi: kernel/cooking.cmi library/decl_kinds.cmo \ kernel/declarations.cmi library/dischargedhypsmap.cmi kernel/entries.cmi \ kernel/indtypes.cmi library/libnames.cmi library/libobject.cmi \ @@ -93,6 +90,9 @@ library/nameops.cmi: kernel/names.cmi lib/pp.cmi library/nametab.cmi: library/libnames.cmi kernel/names.cmi lib/pp.cmi \ kernel/sign.cmi lib/util.cmi library/summary.cmi: library/libnames.cmi kernel/names.cmi +lib/rtree.cmi: lib/pp.cmi +lib/system.cmi: lib/pp.cmi +lib/util.cmi: lib/pp.cmi parsing/ast.cmi: parsing/coqast.cmi lib/dyn.cmi interp/genarg.cmi \ library/libnames.cmi kernel/names.cmi lib/pp.cmi interp/topconstr.cmi \ lib/util.cmi @@ -304,20 +304,20 @@ toplevel/recordobj.cmi: library/libnames.cmi proofs/tacexpr.cmo toplevel/searchisos.cmi: library/libobject.cmi kernel/names.cmi \ kernel/term.cmi toplevel/toplevel.cmi: parsing/pcoq.cmi lib/pp.cmi -toplevel/vernac.cmi: parsing/pcoq.cmi lib/util.cmi toplevel/vernacexpr.cmo toplevel/vernacentries.cmi: kernel/environ.cmi pretyping/evd.cmi \ library/libnames.cmi kernel/names.cmi kernel/term.cmi \ interp/topconstr.cmi toplevel/vernacexpr.cmo toplevel/vernacinterp.cmi toplevel/vernacinterp.cmi: proofs/tacexpr.cmo +toplevel/vernac.cmi: parsing/pcoq.cmi lib/util.cmi toplevel/vernacexpr.cmo contrib/cc/ccalgo.cmi: kernel/names.cmi kernel/term.cmi contrib/cc/ccproof.cmi: contrib/cc/ccalgo.cmi kernel/names.cmi contrib/correctness/past.cmi: kernel/names.cmi contrib/correctness/ptype.cmi \ kernel/term.cmi interp/topconstr.cmi lib/util.cmi -contrib/correctness/pcic.cmi: contrib/correctness/past.cmi \ - pretyping/rawterm.cmi contrib/correctness/pcicenv.cmi: kernel/names.cmi \ contrib/correctness/penv.cmi contrib/correctness/prename.cmi \ kernel/sign.cmi kernel/term.cmi +contrib/correctness/pcic.cmi: contrib/correctness/past.cmi \ + pretyping/rawterm.cmi contrib/correctness/pdb.cmi: kernel/names.cmi contrib/correctness/past.cmi \ contrib/correctness/ptype.cmi contrib/correctness/peffect.cmi: kernel/names.cmi lib/pp.cmi @@ -550,6 +550,12 @@ kernel/inductive.cmo: kernel/declarations.cmi kernel/environ.cmi \ kernel/inductive.cmx: kernel/declarations.cmx kernel/environ.cmx \ kernel/names.cmx kernel/reduction.cmx kernel/sign.cmx kernel/term.cmx \ kernel/type_errors.cmx kernel/univ.cmx lib/util.cmx kernel/inductive.cmi +kernel/modops.cmo: kernel/declarations.cmi kernel/entries.cmi \ + kernel/environ.cmi kernel/names.cmi lib/pp.cmi kernel/term.cmi \ + kernel/univ.cmi lib/util.cmi kernel/modops.cmi +kernel/modops.cmx: kernel/declarations.cmx kernel/entries.cmx \ + kernel/environ.cmx kernel/names.cmx lib/pp.cmx kernel/term.cmx \ + kernel/univ.cmx lib/util.cmx kernel/modops.cmi kernel/mod_typing.cmo: kernel/declarations.cmi kernel/entries.cmi \ kernel/environ.cmi kernel/modops.cmi kernel/names.cmi \ kernel/reduction.cmi kernel/subtyping.cmi kernel/term_typing.cmi \ @@ -558,12 +564,6 @@ kernel/mod_typing.cmx: kernel/declarations.cmx kernel/entries.cmx \ kernel/environ.cmx kernel/modops.cmx kernel/names.cmx \ kernel/reduction.cmx kernel/subtyping.cmx kernel/term_typing.cmx \ kernel/typeops.cmx kernel/univ.cmx lib/util.cmx kernel/mod_typing.cmi -kernel/modops.cmo: kernel/declarations.cmi kernel/entries.cmi \ - kernel/environ.cmi kernel/names.cmi lib/pp.cmi kernel/term.cmi \ - kernel/univ.cmi lib/util.cmi kernel/modops.cmi -kernel/modops.cmx: kernel/declarations.cmx kernel/entries.cmx \ - kernel/environ.cmx kernel/names.cmx lib/pp.cmx kernel/term.cmx \ - kernel/univ.cmx lib/util.cmx kernel/modops.cmi kernel/names.cmo: lib/hashcons.cmi lib/pp.cmi lib/predicate.cmi lib/util.cmi \ kernel/names.cmi kernel/names.cmx: lib/hashcons.cmx lib/pp.cmx lib/predicate.cmx lib/util.cmx \ @@ -646,34 +646,24 @@ lib/edit.cmo: lib/bstack.cmi lib/pp.cmi lib/util.cmi lib/edit.cmi lib/edit.cmx: lib/bstack.cmx lib/pp.cmx lib/util.cmx lib/edit.cmi lib/explore.cmo: lib/explore.cmi lib/explore.cmx: lib/explore.cmi -lib/gmap.cmo: lib/gmap.cmi -lib/gmap.cmx: lib/gmap.cmi lib/gmapl.cmo: lib/gmap.cmi lib/util.cmi lib/gmapl.cmi lib/gmapl.cmx: lib/gmap.cmx lib/util.cmx lib/gmapl.cmi +lib/gmap.cmo: lib/gmap.cmi +lib/gmap.cmx: lib/gmap.cmi lib/gset.cmo: lib/gset.cmi lib/gset.cmx: lib/gset.cmi lib/hashcons.cmo: lib/hashcons.cmi lib/hashcons.cmx: lib/hashcons.cmi lib/options.cmo: lib/util.cmi lib/options.cmi lib/options.cmx: lib/util.cmx lib/options.cmi -lib/pp.cmo: lib/pp_control.cmi lib/pp.cmi -lib/pp.cmx: lib/pp_control.cmx lib/pp.cmi lib/pp_control.cmo: lib/pp_control.cmi lib/pp_control.cmx: lib/pp_control.cmi +lib/pp.cmo: lib/pp_control.cmi lib/pp.cmi +lib/pp.cmx: lib/pp_control.cmx lib/pp.cmi lib/predicate.cmo: lib/predicate.cmi lib/predicate.cmx: lib/predicate.cmi lib/profile.cmo: lib/profile.cmi lib/profile.cmx: lib/profile.cmi -lib/rtree.cmo: lib/pp.cmi lib/util.cmi lib/rtree.cmi -lib/rtree.cmx: lib/pp.cmx lib/util.cmx lib/rtree.cmi -lib/stamps.cmo: lib/stamps.cmi -lib/stamps.cmx: lib/stamps.cmi -lib/system.cmo: config/coq_config.cmi lib/pp.cmi lib/util.cmi lib/system.cmi -lib/system.cmx: config/coq_config.cmx lib/pp.cmx lib/util.cmx lib/system.cmi -lib/tlm.cmo: lib/gmap.cmi lib/gset.cmi lib/tlm.cmi -lib/tlm.cmx: lib/gmap.cmx lib/gset.cmx lib/tlm.cmi -lib/util.cmo: lib/pp.cmi lib/util.cmi -lib/util.cmx: lib/pp.cmx lib/util.cmi library/declare.cmo: library/decl_kinds.cmo kernel/declarations.cmi \ library/dischargedhypsmap.cmi kernel/entries.cmi kernel/environ.cmi \ library/global.cmi library/impargs.cmi kernel/indtypes.cmi \ @@ -778,6 +768,16 @@ library/states.cmx: library/lib.cmx library/library.cmx library/summary.cmx \ lib/system.cmx library/states.cmi library/summary.cmo: lib/dyn.cmi lib/pp.cmi lib/util.cmi library/summary.cmi library/summary.cmx: lib/dyn.cmx lib/pp.cmx lib/util.cmx library/summary.cmi +lib/rtree.cmo: lib/pp.cmi lib/util.cmi lib/rtree.cmi +lib/rtree.cmx: lib/pp.cmx lib/util.cmx lib/rtree.cmi +lib/stamps.cmo: lib/stamps.cmi +lib/stamps.cmx: lib/stamps.cmi +lib/system.cmo: config/coq_config.cmi lib/pp.cmi lib/util.cmi lib/system.cmi +lib/system.cmx: config/coq_config.cmx lib/pp.cmx lib/util.cmx lib/system.cmi +lib/tlm.cmo: lib/gmap.cmi lib/gset.cmi lib/tlm.cmi +lib/tlm.cmx: lib/gmap.cmx lib/gset.cmx lib/tlm.cmi +lib/util.cmo: lib/pp.cmi lib/util.cmi +lib/util.cmx: lib/pp.cmx lib/util.cmi parsing/argextend.cmo: parsing/ast.cmi interp/genarg.cmi parsing/pcoq.cmi \ parsing/q_coqast.cmo parsing/q_util.cmi lib/util.cmi \ toplevel/vernacexpr.cmo @@ -1764,10 +1764,10 @@ tactics/wcclausenv.cmx: proofs/clenv.cmx kernel/environ.cmx \ pretyping/reductionops.cmx proofs/refiner.cmx kernel/sign.cmx \ proofs/tacmach.cmx kernel/term.cmx pretyping/termops.cmx lib/util.cmx \ tactics/wcclausenv.cmi -tools/coq_vo2xml.cmo: config/coq_config.cmi toplevel/usage.cmi -tools/coq_vo2xml.cmx: config/coq_config.cmx toplevel/usage.cmx tools/coqdep.cmo: config/coq_config.cmi tools/coqdep_lexer.cmo tools/coqdep.cmx: config/coq_config.cmx tools/coqdep_lexer.cmx +tools/coq_vo2xml.cmo: config/coq_config.cmi toplevel/usage.cmi +tools/coq_vo2xml.cmx: config/coq_config.cmx toplevel/usage.cmx tools/gallina.cmo: tools/gallina_lexer.cmo tools/gallina.cmx: tools/gallina_lexer.cmx toplevel/cerrors.cmo: parsing/ast.cmi pretyping/cases.cmi toplevel/himsg.cmi \ @@ -1970,14 +1970,6 @@ toplevel/toplevel.cmx: toplevel/cerrors.cmx library/lib.cmx \ toplevel/vernac.cmx toplevel/vernacexpr.cmx toplevel/toplevel.cmi toplevel/usage.cmo: config/coq_config.cmi toplevel/usage.cmi toplevel/usage.cmx: config/coq_config.cmx toplevel/usage.cmi -toplevel/vernac.cmo: parsing/coqast.cmi library/lib.cmi library/library.cmi \ - kernel/names.cmi lib/options.cmi parsing/pcoq.cmi lib/pp.cmi \ - library/states.cmi lib/system.cmi lib/util.cmi toplevel/vernacentries.cmi \ - toplevel/vernacexpr.cmo toplevel/vernacinterp.cmi toplevel/vernac.cmi -toplevel/vernac.cmx: parsing/coqast.cmx library/lib.cmx library/library.cmx \ - kernel/names.cmx lib/options.cmx parsing/pcoq.cmx lib/pp.cmx \ - library/states.cmx lib/system.cmx lib/util.cmx toplevel/vernacentries.cmx \ - toplevel/vernacexpr.cmx toplevel/vernacinterp.cmx toplevel/vernac.cmi toplevel/vernacentries.cmo: tactics/auto.cmi toplevel/class.cmi \ pretyping/classops.cmi toplevel/command.cmi interp/constrextern.cmi \ interp/constrintern.cmi library/decl_kinds.cmo library/declaremods.cmi \ @@ -2038,6 +2030,14 @@ toplevel/vernacinterp.cmx: parsing/ast.cmx parsing/coqast.cmx \ kernel/names.cmx lib/options.cmx lib/pp.cmx proofs/proof_type.cmx \ proofs/tacexpr.cmx tactics/tacinterp.cmx lib/util.cmx \ toplevel/vernacexpr.cmx toplevel/vernacinterp.cmi +toplevel/vernac.cmo: parsing/coqast.cmi library/lib.cmi library/library.cmi \ + kernel/names.cmi lib/options.cmi parsing/pcoq.cmi lib/pp.cmi \ + library/states.cmi lib/system.cmi lib/util.cmi toplevel/vernacentries.cmi \ + toplevel/vernacexpr.cmo toplevel/vernacinterp.cmi toplevel/vernac.cmi +toplevel/vernac.cmx: parsing/coqast.cmx library/lib.cmx library/library.cmx \ + kernel/names.cmx lib/options.cmx parsing/pcoq.cmx lib/pp.cmx \ + library/states.cmx lib/system.cmx lib/util.cmx toplevel/vernacentries.cmx \ + toplevel/vernacexpr.cmx toplevel/vernacinterp.cmx toplevel/vernac.cmi contrib/cc/ccalgo.cmo: kernel/names.cmi kernel/term.cmi contrib/cc/ccalgo.cmi contrib/cc/ccalgo.cmx: kernel/names.cmx kernel/term.cmx contrib/cc/ccalgo.cmi contrib/cc/ccproof.cmo: contrib/cc/ccalgo.cmi kernel/names.cmi \ @@ -2058,6 +2058,18 @@ contrib/cc/cctac.cmx: contrib/cc/ccalgo.cmx contrib/cc/ccproof.cmx \ lib/pp.cmx parsing/pptactic.cmx proofs/proof_type.cmx proofs/refiner.cmx \ tactics/tacinterp.cmx proofs/tacmach.cmx tactics/tacticals.cmx \ tactics/tactics.cmx kernel/term.cmx lib/util.cmx +contrib/correctness/pcicenv.cmo: library/global.cmi kernel/names.cmi \ + contrib/correctness/past.cmi contrib/correctness/penv.cmi \ + contrib/correctness/pmisc.cmi contrib/correctness/pmonad.cmi \ + contrib/correctness/prename.cmi contrib/correctness/ptype.cmi \ + contrib/correctness/putil.cmi kernel/sign.cmi kernel/term.cmi \ + kernel/univ.cmi contrib/correctness/pcicenv.cmi +contrib/correctness/pcicenv.cmx: library/global.cmx kernel/names.cmx \ + contrib/correctness/past.cmi contrib/correctness/penv.cmx \ + contrib/correctness/pmisc.cmx contrib/correctness/pmonad.cmx \ + contrib/correctness/prename.cmx contrib/correctness/ptype.cmi \ + contrib/correctness/putil.cmx kernel/sign.cmx kernel/term.cmx \ + kernel/univ.cmx contrib/correctness/pcicenv.cmi contrib/correctness/pcic.cmo: kernel/declarations.cmi library/declare.cmi \ pretyping/detyping.cmi kernel/entries.cmi library/global.cmi \ kernel/indtypes.cmi library/libnames.cmi library/nameops.cmi \ @@ -2074,18 +2086,6 @@ contrib/correctness/pcic.cmx: kernel/declarations.cmx library/declare.cmx \ kernel/sign.cmx kernel/term.cmx pretyping/termops.cmx \ interp/topconstr.cmx kernel/typeops.cmx lib/util.cmx \ toplevel/vernacexpr.cmx contrib/correctness/pcic.cmi -contrib/correctness/pcicenv.cmo: library/global.cmi kernel/names.cmi \ - contrib/correctness/past.cmi contrib/correctness/penv.cmi \ - contrib/correctness/pmisc.cmi contrib/correctness/pmonad.cmi \ - contrib/correctness/prename.cmi contrib/correctness/ptype.cmi \ - contrib/correctness/putil.cmi kernel/sign.cmi kernel/term.cmi \ - kernel/univ.cmi contrib/correctness/pcicenv.cmi -contrib/correctness/pcicenv.cmx: library/global.cmx kernel/names.cmx \ - contrib/correctness/past.cmi contrib/correctness/penv.cmx \ - contrib/correctness/pmisc.cmx contrib/correctness/pmonad.cmx \ - contrib/correctness/prename.cmx contrib/correctness/ptype.cmi \ - contrib/correctness/putil.cmx kernel/sign.cmx kernel/term.cmx \ - kernel/univ.cmx contrib/correctness/pcicenv.cmi contrib/correctness/pdb.cmo: library/declare.cmi library/global.cmi \ kernel/names.cmi library/nametab.cmi contrib/correctness/past.cmi \ contrib/correctness/peffect.cmi contrib/correctness/penv.cmi \ @@ -2626,6 +2626,14 @@ contrib/interface/pbp.cmx: interp/coqlib.cmx contrib/interface/ctast.cmx \ tactics/tacinterp.cmx proofs/tacmach.cmx tactics/tacticals.cmx \ tactics/tactics.cmx kernel/term.cmx interp/topconstr.cmx \ pretyping/typing.cmx lib/util.cmx contrib/interface/pbp.cmi +contrib/interface/showproof_ct.cmo: contrib/interface/ascent.cmi \ + parsing/esyntax.cmi library/global.cmi toplevel/metasyntax.cmi lib/pp.cmi \ + parsing/printer.cmi contrib/interface/translate.cmi \ + contrib/interface/vtp.cmi contrib/interface/xlate.cmi +contrib/interface/showproof_ct.cmx: contrib/interface/ascent.cmi \ + parsing/esyntax.cmx library/global.cmx toplevel/metasyntax.cmx lib/pp.cmx \ + parsing/printer.cmx contrib/interface/translate.cmx \ + contrib/interface/vtp.cmx contrib/interface/xlate.cmx contrib/interface/showproof.cmo: proofs/clenv.cmi interp/constrintern.cmi \ parsing/coqast.cmi kernel/declarations.cmi kernel/environ.cmi \ pretyping/evd.cmi interp/genarg.cmi library/global.cmi \ @@ -2650,14 +2658,6 @@ contrib/interface/showproof.cmx: proofs/clenv.cmx interp/constrintern.cmx \ pretyping/termops.cmx contrib/interface/translate.cmx \ pretyping/typing.cmx lib/util.cmx toplevel/vernacinterp.cmx \ contrib/interface/showproof.cmi -contrib/interface/showproof_ct.cmo: contrib/interface/ascent.cmi \ - parsing/esyntax.cmi library/global.cmi toplevel/metasyntax.cmi lib/pp.cmi \ - parsing/printer.cmi contrib/interface/translate.cmi \ - contrib/interface/vtp.cmi contrib/interface/xlate.cmi -contrib/interface/showproof_ct.cmx: contrib/interface/ascent.cmi \ - parsing/esyntax.cmx library/global.cmx toplevel/metasyntax.cmx lib/pp.cmx \ - parsing/printer.cmx contrib/interface/translate.cmx \ - contrib/interface/vtp.cmx contrib/interface/xlate.cmx contrib/interface/translate.cmo: contrib/interface/ascent.cmi parsing/ast.cmi \ contrib/interface/ctast.cmo kernel/environ.cmi pretyping/evarutil.cmi \ pretyping/evd.cmi library/libobject.cmi library/library.cmi \ @@ -2828,12 +2828,12 @@ contrib/romega/refl_omega.cmx: parsing/ast.cmx tactics/auto.cmx \ proofs/proof_type.cmx kernel/reduction.cmx kernel/sign.cmx \ proofs/tacmach.cmx tactics/tacticals.cmx tactics/tactics.cmx \ kernel/term.cmx lib/util.cmx -contrib/xml/acic.cmo: kernel/names.cmi kernel/term.cmi -contrib/xml/acic.cmx: kernel/names.cmx kernel/term.cmx contrib/xml/acic2Xml.cmo: contrib/xml/acic.cmo contrib/xml/cic2acic.cmo \ kernel/names.cmi kernel/term.cmi lib/util.cmi contrib/xml/xml.cmi contrib/xml/acic2Xml.cmx: contrib/xml/acic.cmx contrib/xml/cic2acic.cmx \ kernel/names.cmx kernel/term.cmx lib/util.cmx contrib/xml/xml.cmx +contrib/xml/acic.cmo: kernel/names.cmi kernel/term.cmi +contrib/xml/acic.cmx: kernel/names.cmx kernel/term.cmx contrib/xml/cic2acic.cmo: contrib/xml/acic.cmo library/declare.cmi \ library/dischargedhypsmap.cmi contrib/xml/doubleTypeInference.cmi \ kernel/environ.cmi pretyping/evarutil.cmi pretyping/evd.cmi \ @@ -2888,8 +2888,6 @@ contrib/xml/proofTree2Xml.cmx: contrib/xml/acic.cmx contrib/xml/acic2Xml.cmx \ contrib/xml/xml.cmx contrib/xml/unshare.cmo: contrib/xml/unshare.cmi contrib/xml/unshare.cmx: contrib/xml/unshare.cmi -contrib/xml/xml.cmo: contrib/xml/xml.cmi -contrib/xml/xml.cmx: contrib/xml/xml.cmi contrib/xml/xmlcommand.cmo: contrib/xml/acic.cmo contrib/xml/acic2Xml.cmo \ contrib/xml/cic2acic.cmo library/decl_kinds.cmo kernel/declarations.cmi \ library/declare.cmi kernel/environ.cmi pretyping/evd.cmi \ @@ -2916,6 +2914,8 @@ contrib/xml/xmlentries.cmx: toplevel/cerrors.cmx parsing/egrammar.cmx \ parsing/extend.cmx interp/genarg.cmx parsing/pcoq.cmx lib/pp.cmx \ parsing/pptactic.cmx tactics/tacinterp.cmx lib/util.cmx \ toplevel/vernacinterp.cmx contrib/xml/xmlcommand.cmx +contrib/xml/xml.cmo: contrib/xml/xml.cmi +contrib/xml/xml.cmx: contrib/xml/xml.cmi tactics/tauto.cmo: parsing/grammar.cma tactics/tauto.cmx: parsing/grammar.cma tactics/eqdecide.cmo: parsing/grammar.cma diff --git a/.depend.coq b/.depend.coq index 8f15561207..076eb22739 100644 --- a/.depend.coq +++ b/.depend.coq @@ -2,57 +2,57 @@ theories/Reals/TypeSyntax.vo: theories/Reals/TypeSyntax.v theories/Reals/Rdefinitions.vo: theories/Reals/Rdefinitions.v theories/ZArith/ZArith_base.vo theories/Reals/TypeSyntax.vo theories/Reals/Rsyntax.vo: theories/Reals/Rsyntax.v theories/Reals/Rdefinitions.vo theories/Reals/Raxioms.vo: theories/Reals/Raxioms.v theories/ZArith/ZArith_base.vo theories/Reals/Rsyntax.vo theories/Reals/TypeSyntax.vo -theories/Reals/Rbase.vo: theories/Reals/Rbase.v theories/Reals/Raxioms.vo contrib/ring/ZArithRing.vo contrib/omega/Omega.vo contrib/field/Field.vo -theories/Reals/DiscrR.vo: theories/Reals/DiscrR.v theories/Reals/Rbase.vo -theories/Reals/RealsB.vo: theories/Reals/RealsB.v theories/Reals/Rdefinitions.vo theories/Reals/TypeSyntax.vo theories/Reals/Raxioms.vo theories/Reals/Rbase.vo theories/Reals/DiscrR.vo -theories/Reals/R_Ifp.vo: theories/Reals/R_Ifp.v theories/Reals/RealsB.vo contrib/omega/Omega.vo -theories/Reals/Rbasic_fun.vo: theories/Reals/Rbasic_fun.v theories/Reals/RealsB.vo theories/Reals/R_Ifp.vo contrib/fourier/Fourier.vo -theories/Reals/R_sqr.vo: theories/Reals/R_sqr.v theories/Reals/RealsB.vo theories/Reals/Rbasic_fun.vo +theories/Reals/RIneq.vo: theories/Reals/RIneq.v theories/Reals/Raxioms.vo contrib/ring/ZArithRing.vo contrib/omega/Omega.vo contrib/field/Field.vo +theories/Reals/DiscrR.vo: theories/Reals/DiscrR.v theories/Reals/RIneq.vo +theories/Reals/Rbase.vo: theories/Reals/Rbase.v theories/Reals/Rdefinitions.vo theories/Reals/TypeSyntax.vo theories/Reals/Raxioms.vo theories/Reals/RIneq.vo theories/Reals/DiscrR.vo +theories/Reals/R_Ifp.vo: theories/Reals/R_Ifp.v theories/Reals/Rbase.vo contrib/omega/Omega.vo +theories/Reals/Rbasic_fun.vo: theories/Reals/Rbasic_fun.v theories/Reals/Rbase.vo theories/Reals/R_Ifp.vo contrib/fourier/Fourier.vo +theories/Reals/R_sqr.vo: theories/Reals/R_sqr.v theories/Reals/Rbase.vo theories/Reals/Rbasic_fun.vo theories/Reals/SplitAbsolu.vo: theories/Reals/SplitAbsolu.v theories/Reals/Rbasic_fun.vo -theories/Reals/SplitRmult.vo: theories/Reals/SplitRmult.v theories/Reals/RealsB.vo -theories/Reals/ArithProp.vo: theories/Reals/ArithProp.v theories/Reals/RealsB.vo theories/Reals/Rbasic_fun.vo theories/Arith/Even.vo theories/Arith/Div2.vo -theories/Reals/Rfunctions.vo: theories/Reals/Rfunctions.v theories/Reals/RealsB.vo theories/Reals/R_Ifp.vo theories/Reals/Rbasic_fun.vo theories/Reals/R_sqr.vo theories/Reals/SplitAbsolu.vo theories/Reals/SplitRmult.vo theories/Reals/ArithProp.vo contrib/omega/Omega.vo theories/ZArith/Zpower.vo -theories/Reals/Rseries.vo: theories/Reals/Rseries.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Logic/Classical.vo theories/Arith/Compare.vo -theories/Reals/SeqProp.vo: theories/Reals/SeqProp.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Logic/Classical.vo theories/Arith/Max.vo -theories/Reals/Rcomplet.vo: theories/Reals/Rcomplet.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/SeqProp.vo theories/Arith/Max.vo -theories/Reals/PartSum.vo: theories/Reals/PartSum.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/Rcomplet.vo theories/Arith/Max.vo -theories/Reals/AltSeries.vo: theories/Reals/AltSeries.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/SeqProp.vo theories/Reals/PartSum.vo theories/Arith/Max.vo -theories/Reals/Binome.vo: theories/Reals/Binome.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/PartSum.vo -theories/Reals/Rsigma.vo: theories/Reals/Rsigma.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/PartSum.vo -theories/Reals/Rprod.vo: theories/Reals/Rprod.v theories/Arith/Compare.vo theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/PartSum.vo theories/Reals/Binome.vo -theories/Reals/Cauchy_prod.vo: theories/Reals/Cauchy_prod.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/PartSum.vo -theories/Reals/Alembert.vo: theories/Reals/Alembert.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/SeqProp.vo theories/Reals/PartSum.vo theories/Arith/Max.vo -theories/Reals/SeqSeries.vo: theories/Reals/SeqSeries.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/SeqProp.vo theories/Reals/Rcomplet.vo theories/Reals/PartSum.vo theories/Reals/AltSeries.vo theories/Reals/Binome.vo theories/Reals/Rsigma.vo theories/Reals/Rprod.vo theories/Reals/Cauchy_prod.vo theories/Reals/Alembert.vo -theories/Reals/Rtrigo_fun.vo: theories/Reals/Rtrigo_fun.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo -theories/Reals/Rtrigo_def.vo: theories/Reals/Rtrigo_def.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo_fun.vo theories/Arith/Max.vo -theories/Reals/Rtrigo_alt.vo: theories/Reals/Rtrigo_alt.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo_def.vo -theories/Reals/Cos_rel.vo: theories/Reals/Cos_rel.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo_def.vo -theories/Reals/Cos_plus.vo: theories/Reals/Cos_plus.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo_def.vo theories/Reals/Cos_rel.vo theories/Arith/Max.vo -theories/Reals/Rtrigo.vo: theories/Reals/Rtrigo.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo_fun.vo theories/Reals/Rtrigo_def.vo theories/Reals/Rtrigo_alt.vo theories/Reals/Cos_rel.vo theories/Reals/Cos_plus.vo theories/ZArith/ZArith_base.vo theories/ZArith/Zcomplements.vo theories/Logic/Classical_Prop.vo -theories/Reals/Rlimit.vo: theories/Reals/Rlimit.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Logic/Classical_Prop.vo contrib/fourier/Fourier.vo -theories/Reals/Rderiv.vo: theories/Reals/Rderiv.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/Rlimit.vo contrib/fourier/Fourier.vo theories/Logic/Classical_Prop.vo theories/Logic/Classical_Pred_Type.vo contrib/omega/Omega.vo -theories/Reals/RList.vo: theories/Reals/RList.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo -theories/Reals/Ranalysis1.vo: theories/Reals/Ranalysis1.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/Rlimit.vo theories/Reals/Rderiv.vo -theories/Reals/Ranalysis2.vo: theories/Reals/Ranalysis2.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/Ranalysis1.vo contrib/omega/Omega.vo -theories/Reals/Ranalysis3.vo: theories/Reals/Ranalysis3.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/Ranalysis1.vo theories/Reals/Ranalysis2.vo -theories/Reals/Rtopology.vo: theories/Reals/Rtopology.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/Ranalysis1.vo theories/Reals/RList.vo theories/Logic/Classical_Prop.vo theories/Logic/Classical_Pred_Type.vo -theories/Reals/TAF.vo: theories/Reals/TAF.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/Ranalysis1.vo theories/Reals/Rtopology.vo -theories/Reals/PSeries_reg.vo: theories/Reals/PSeries_reg.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Ranalysis1.vo theories/Arith/Max.vo theories/Arith/Even.vo -theories/Reals/Exp_prop.vo: theories/Reals/Exp_prop.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis1.vo theories/Reals/PSeries_reg.vo theories/Arith/Div2.vo theories/Arith/Even.vo theories/Arith/Max.vo -theories/Reals/Rtrigo_reg.vo: theories/Reals/Rtrigo_reg.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis1.vo theories/Reals/PSeries_reg.vo -theories/Reals/Rsqrt_def.vo: theories/Reals/Rsqrt_def.v theories/Bool/Sumbool.vo theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Ranalysis1.vo -theories/Reals/R_sqrt.vo: theories/Reals/R_sqrt.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/Rsqrt_def.vo -theories/Reals/Rtrigo_calc.vo: theories/Reals/Rtrigo_calc.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/R_sqrt.vo -theories/Reals/Rgeom.vo: theories/Reals/Rgeom.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/R_sqrt.vo -theories/Reals/Sqrt_reg.vo: theories/Reals/Sqrt_reg.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/Ranalysis1.vo theories/Reals/R_sqrt.vo -theories/Reals/Ranalysis4.vo: theories/Reals/Ranalysis4.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis1.vo theories/Reals/Ranalysis3.vo theories/Reals/Exp_prop.vo -theories/Reals/Rpower.vo: theories/Reals/Rpower.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis1.vo theories/Reals/Exp_prop.vo theories/Reals/Rsqrt_def.vo theories/Reals/R_sqrt.vo theories/Reals/TAF.vo theories/Reals/Ranalysis4.vo -theories/Reals/Ranalysis.vo: theories/Reals/Ranalysis.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/Rtrigo.vo theories/Reals/SeqSeries.vo theories/Reals/Ranalysis1.vo theories/Reals/Ranalysis2.vo theories/Reals/Ranalysis3.vo theories/Reals/Rtopology.vo theories/Reals/TAF.vo theories/Reals/PSeries_reg.vo theories/Reals/Exp_prop.vo theories/Reals/Rtrigo_reg.vo theories/Reals/Rsqrt_def.vo theories/Reals/R_sqrt.vo theories/Reals/Rtrigo_calc.vo theories/Reals/Rgeom.vo theories/Reals/RList.vo theories/Reals/Sqrt_reg.vo theories/Reals/Ranalysis4.vo theories/Reals/Rpower.vo -theories/Reals/NewtonInt.vo: theories/Reals/NewtonInt.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis.vo -theories/Reals/RiemannInt_SF.vo: theories/Reals/RiemannInt_SF.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/Ranalysis.vo theories/Logic/Classical_Prop.vo -theories/Reals/RiemannInt.vo: theories/Reals/RiemannInt.v theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Ranalysis.vo theories/Reals/RealsB.vo theories/Reals/RiemannInt_SF.vo theories/Logic/Classical_Prop.vo theories/Logic/Classical_Pred_Type.vo theories/Arith/Max.vo +theories/Reals/SplitRmult.vo: theories/Reals/SplitRmult.v theories/Reals/Rbase.vo +theories/Reals/ArithProp.vo: theories/Reals/ArithProp.v theories/Reals/Rbase.vo theories/Reals/Rbasic_fun.vo theories/Arith/Even.vo theories/Arith/Div2.vo +theories/Reals/Rfunctions.vo: theories/Reals/Rfunctions.v theories/Reals/Rbase.vo theories/Reals/R_Ifp.vo theories/Reals/Rbasic_fun.vo theories/Reals/R_sqr.vo theories/Reals/SplitAbsolu.vo theories/Reals/SplitRmult.vo theories/Reals/ArithProp.vo contrib/omega/Omega.vo theories/ZArith/Zpower.vo +theories/Reals/Rseries.vo: theories/Reals/Rseries.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Logic/Classical.vo theories/Arith/Compare.vo +theories/Reals/SeqProp.vo: theories/Reals/SeqProp.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Logic/Classical.vo theories/Arith/Max.vo +theories/Reals/Rcomplet.vo: theories/Reals/Rcomplet.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/SeqProp.vo theories/Arith/Max.vo +theories/Reals/PartSum.vo: theories/Reals/PartSum.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/Rcomplet.vo theories/Arith/Max.vo +theories/Reals/AltSeries.vo: theories/Reals/AltSeries.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/SeqProp.vo theories/Reals/PartSum.vo theories/Arith/Max.vo +theories/Reals/Binome.vo: theories/Reals/Binome.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/PartSum.vo +theories/Reals/Rsigma.vo: theories/Reals/Rsigma.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/PartSum.vo +theories/Reals/Rprod.vo: theories/Reals/Rprod.v theories/Arith/Compare.vo theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/PartSum.vo theories/Reals/Binome.vo +theories/Reals/Cauchy_prod.vo: theories/Reals/Cauchy_prod.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/PartSum.vo +theories/Reals/Alembert.vo: theories/Reals/Alembert.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/SeqProp.vo theories/Reals/PartSum.vo theories/Arith/Max.vo +theories/Reals/SeqSeries.vo: theories/Reals/SeqSeries.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/SeqProp.vo theories/Reals/Rcomplet.vo theories/Reals/PartSum.vo theories/Reals/AltSeries.vo theories/Reals/Binome.vo theories/Reals/Rsigma.vo theories/Reals/Rprod.vo theories/Reals/Cauchy_prod.vo theories/Reals/Alembert.vo +theories/Reals/Rtrigo_fun.vo: theories/Reals/Rtrigo_fun.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo +theories/Reals/Rtrigo_def.vo: theories/Reals/Rtrigo_def.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo_fun.vo theories/Arith/Max.vo +theories/Reals/Rtrigo_alt.vo: theories/Reals/Rtrigo_alt.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo_def.vo +theories/Reals/Cos_rel.vo: theories/Reals/Cos_rel.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo_def.vo +theories/Reals/Cos_plus.vo: theories/Reals/Cos_plus.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo_def.vo theories/Reals/Cos_rel.vo theories/Arith/Max.vo +theories/Reals/Rtrigo.vo: theories/Reals/Rtrigo.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo_fun.vo theories/Reals/Rtrigo_def.vo theories/Reals/Rtrigo_alt.vo theories/Reals/Cos_rel.vo theories/Reals/Cos_plus.vo theories/ZArith/ZArith_base.vo theories/ZArith/Zcomplements.vo theories/Logic/Classical_Prop.vo +theories/Reals/Rlimit.vo: theories/Reals/Rlimit.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Logic/Classical_Prop.vo contrib/fourier/Fourier.vo +theories/Reals/Rderiv.vo: theories/Reals/Rderiv.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rlimit.vo contrib/fourier/Fourier.vo theories/Logic/Classical_Prop.vo theories/Logic/Classical_Pred_Type.vo contrib/omega/Omega.vo +theories/Reals/RList.vo: theories/Reals/RList.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo +theories/Reals/Ranalysis1.vo: theories/Reals/Ranalysis1.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rlimit.vo theories/Reals/Rderiv.vo +theories/Reals/Ranalysis2.vo: theories/Reals/Ranalysis2.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Ranalysis1.vo contrib/omega/Omega.vo +theories/Reals/Ranalysis3.vo: theories/Reals/Ranalysis3.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Ranalysis1.vo theories/Reals/Ranalysis2.vo +theories/Reals/Rtopology.vo: theories/Reals/Rtopology.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Ranalysis1.vo theories/Reals/RList.vo theories/Logic/Classical_Prop.vo theories/Logic/Classical_Pred_Type.vo +theories/Reals/TAF.vo: theories/Reals/TAF.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Ranalysis1.vo theories/Reals/Rtopology.vo +theories/Reals/PSeries_reg.vo: theories/Reals/PSeries_reg.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Ranalysis1.vo theories/Arith/Max.vo theories/Arith/Even.vo +theories/Reals/Exp_prop.vo: theories/Reals/Exp_prop.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis1.vo theories/Reals/PSeries_reg.vo theories/Arith/Div2.vo theories/Arith/Even.vo theories/Arith/Max.vo +theories/Reals/Rtrigo_reg.vo: theories/Reals/Rtrigo_reg.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis1.vo theories/Reals/PSeries_reg.vo +theories/Reals/Rsqrt_def.vo: theories/Reals/Rsqrt_def.v theories/Bool/Sumbool.vo theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Ranalysis1.vo +theories/Reals/R_sqrt.vo: theories/Reals/R_sqrt.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rsqrt_def.vo +theories/Reals/Rtrigo_calc.vo: theories/Reals/Rtrigo_calc.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/R_sqrt.vo +theories/Reals/Rgeom.vo: theories/Reals/Rgeom.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/R_sqrt.vo +theories/Reals/Sqrt_reg.vo: theories/Reals/Sqrt_reg.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Ranalysis1.vo theories/Reals/R_sqrt.vo +theories/Reals/Ranalysis4.vo: theories/Reals/Ranalysis4.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis1.vo theories/Reals/Ranalysis3.vo theories/Reals/Exp_prop.vo +theories/Reals/Rpower.vo: theories/Reals/Rpower.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis1.vo theories/Reals/Exp_prop.vo theories/Reals/Rsqrt_def.vo theories/Reals/R_sqrt.vo theories/Reals/TAF.vo theories/Reals/Ranalysis4.vo +theories/Reals/Ranalysis.vo: theories/Reals/Ranalysis.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rtrigo.vo theories/Reals/SeqSeries.vo theories/Reals/Ranalysis1.vo theories/Reals/Ranalysis2.vo theories/Reals/Ranalysis3.vo theories/Reals/Rtopology.vo theories/Reals/TAF.vo theories/Reals/PSeries_reg.vo theories/Reals/Exp_prop.vo theories/Reals/Rtrigo_reg.vo theories/Reals/Rsqrt_def.vo theories/Reals/R_sqrt.vo theories/Reals/Rtrigo_calc.vo theories/Reals/Rgeom.vo theories/Reals/RList.vo theories/Reals/Sqrt_reg.vo theories/Reals/Ranalysis4.vo theories/Reals/Rpower.vo +theories/Reals/NewtonInt.vo: theories/Reals/NewtonInt.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis.vo +theories/Reals/RiemannInt_SF.vo: theories/Reals/RiemannInt_SF.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Ranalysis.vo theories/Logic/Classical_Prop.vo +theories/Reals/RiemannInt.vo: theories/Reals/RiemannInt.v theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Ranalysis.vo theories/Reals/Rbase.vo theories/Reals/RiemannInt_SF.vo theories/Logic/Classical_Prop.vo theories/Logic/Classical_Pred_Type.vo theories/Arith/Max.vo theories/Reals/Integration.vo: theories/Reals/Integration.v theories/Reals/NewtonInt.vo theories/Reals/RiemannInt_SF.vo theories/Reals/RiemannInt.vo -theories/Reals/Reals.vo: theories/Reals/Reals.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis.vo theories/Reals/Integration.vo +theories/Reals/Reals.vo: theories/Reals/Reals.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis.vo theories/Reals/Integration.vo theories/Init/Datatypes.vo: theories/Init/Datatypes.v theories/Init/DatatypesSyntax.vo: theories/Init/DatatypesSyntax.v theories/Init/Datatypes.vo theories/Init/Peano.vo: theories/Init/Peano.v theories/Init/Logic.vo theories/Init/LogicSyntax.vo theories/Init/Datatypes.vo @@ -185,57 +185,57 @@ theories/Reals/TypeSyntax.vo: theories/Reals/TypeSyntax.v theories/Reals/Rdefinitions.vo: theories/Reals/Rdefinitions.v theories/ZArith/ZArith_base.vo theories/Reals/TypeSyntax.vo theories/Reals/Rsyntax.vo: theories/Reals/Rsyntax.v theories/Reals/Rdefinitions.vo theories/Reals/Raxioms.vo: theories/Reals/Raxioms.v theories/ZArith/ZArith_base.vo theories/Reals/Rsyntax.vo theories/Reals/TypeSyntax.vo -theories/Reals/Rbase.vo: theories/Reals/Rbase.v theories/Reals/Raxioms.vo contrib/ring/ZArithRing.vo contrib/omega/Omega.vo contrib/field/Field.vo -theories/Reals/DiscrR.vo: theories/Reals/DiscrR.v theories/Reals/Rbase.vo -theories/Reals/RealsB.vo: theories/Reals/RealsB.v theories/Reals/Rdefinitions.vo theories/Reals/TypeSyntax.vo theories/Reals/Raxioms.vo theories/Reals/Rbase.vo theories/Reals/DiscrR.vo -theories/Reals/R_Ifp.vo: theories/Reals/R_Ifp.v theories/Reals/RealsB.vo contrib/omega/Omega.vo -theories/Reals/Rbasic_fun.vo: theories/Reals/Rbasic_fun.v theories/Reals/RealsB.vo theories/Reals/R_Ifp.vo contrib/fourier/Fourier.vo -theories/Reals/R_sqr.vo: theories/Reals/R_sqr.v theories/Reals/RealsB.vo theories/Reals/Rbasic_fun.vo +theories/Reals/RIneq.vo: theories/Reals/RIneq.v theories/Reals/Raxioms.vo contrib/ring/ZArithRing.vo contrib/omega/Omega.vo contrib/field/Field.vo +theories/Reals/DiscrR.vo: theories/Reals/DiscrR.v theories/Reals/RIneq.vo +theories/Reals/Rbase.vo: theories/Reals/Rbase.v theories/Reals/Rdefinitions.vo theories/Reals/TypeSyntax.vo theories/Reals/Raxioms.vo theories/Reals/RIneq.vo theories/Reals/DiscrR.vo +theories/Reals/R_Ifp.vo: theories/Reals/R_Ifp.v theories/Reals/Rbase.vo contrib/omega/Omega.vo +theories/Reals/Rbasic_fun.vo: theories/Reals/Rbasic_fun.v theories/Reals/Rbase.vo theories/Reals/R_Ifp.vo contrib/fourier/Fourier.vo +theories/Reals/R_sqr.vo: theories/Reals/R_sqr.v theories/Reals/Rbase.vo theories/Reals/Rbasic_fun.vo theories/Reals/SplitAbsolu.vo: theories/Reals/SplitAbsolu.v theories/Reals/Rbasic_fun.vo -theories/Reals/SplitRmult.vo: theories/Reals/SplitRmult.v theories/Reals/RealsB.vo -theories/Reals/ArithProp.vo: theories/Reals/ArithProp.v theories/Reals/RealsB.vo theories/Reals/Rbasic_fun.vo theories/Arith/Even.vo theories/Arith/Div2.vo -theories/Reals/Rfunctions.vo: theories/Reals/Rfunctions.v theories/Reals/RealsB.vo theories/Reals/R_Ifp.vo theories/Reals/Rbasic_fun.vo theories/Reals/R_sqr.vo theories/Reals/SplitAbsolu.vo theories/Reals/SplitRmult.vo theories/Reals/ArithProp.vo contrib/omega/Omega.vo theories/ZArith/Zpower.vo -theories/Reals/Rseries.vo: theories/Reals/Rseries.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Logic/Classical.vo theories/Arith/Compare.vo -theories/Reals/SeqProp.vo: theories/Reals/SeqProp.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Logic/Classical.vo theories/Arith/Max.vo -theories/Reals/Rcomplet.vo: theories/Reals/Rcomplet.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/SeqProp.vo theories/Arith/Max.vo -theories/Reals/PartSum.vo: theories/Reals/PartSum.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/Rcomplet.vo theories/Arith/Max.vo -theories/Reals/AltSeries.vo: theories/Reals/AltSeries.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/SeqProp.vo theories/Reals/PartSum.vo theories/Arith/Max.vo -theories/Reals/Binome.vo: theories/Reals/Binome.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/PartSum.vo -theories/Reals/Rsigma.vo: theories/Reals/Rsigma.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/PartSum.vo -theories/Reals/Rprod.vo: theories/Reals/Rprod.v theories/Arith/Compare.vo theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/PartSum.vo theories/Reals/Binome.vo -theories/Reals/Cauchy_prod.vo: theories/Reals/Cauchy_prod.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/PartSum.vo -theories/Reals/Alembert.vo: theories/Reals/Alembert.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/SeqProp.vo theories/Reals/PartSum.vo theories/Arith/Max.vo -theories/Reals/SeqSeries.vo: theories/Reals/SeqSeries.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/SeqProp.vo theories/Reals/Rcomplet.vo theories/Reals/PartSum.vo theories/Reals/AltSeries.vo theories/Reals/Binome.vo theories/Reals/Rsigma.vo theories/Reals/Rprod.vo theories/Reals/Cauchy_prod.vo theories/Reals/Alembert.vo -theories/Reals/Rtrigo_fun.vo: theories/Reals/Rtrigo_fun.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo -theories/Reals/Rtrigo_def.vo: theories/Reals/Rtrigo_def.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo_fun.vo theories/Arith/Max.vo -theories/Reals/Rtrigo_alt.vo: theories/Reals/Rtrigo_alt.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo_def.vo -theories/Reals/Cos_rel.vo: theories/Reals/Cos_rel.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo_def.vo -theories/Reals/Cos_plus.vo: theories/Reals/Cos_plus.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo_def.vo theories/Reals/Cos_rel.vo theories/Arith/Max.vo -theories/Reals/Rtrigo.vo: theories/Reals/Rtrigo.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo_fun.vo theories/Reals/Rtrigo_def.vo theories/Reals/Rtrigo_alt.vo theories/Reals/Cos_rel.vo theories/Reals/Cos_plus.vo theories/ZArith/ZArith_base.vo theories/ZArith/Zcomplements.vo theories/Logic/Classical_Prop.vo -theories/Reals/Rlimit.vo: theories/Reals/Rlimit.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Logic/Classical_Prop.vo contrib/fourier/Fourier.vo -theories/Reals/Rderiv.vo: theories/Reals/Rderiv.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/Rlimit.vo contrib/fourier/Fourier.vo theories/Logic/Classical_Prop.vo theories/Logic/Classical_Pred_Type.vo contrib/omega/Omega.vo -theories/Reals/RList.vo: theories/Reals/RList.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo -theories/Reals/Ranalysis1.vo: theories/Reals/Ranalysis1.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/Rlimit.vo theories/Reals/Rderiv.vo -theories/Reals/Ranalysis2.vo: theories/Reals/Ranalysis2.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/Ranalysis1.vo contrib/omega/Omega.vo -theories/Reals/Ranalysis3.vo: theories/Reals/Ranalysis3.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/Ranalysis1.vo theories/Reals/Ranalysis2.vo -theories/Reals/Rtopology.vo: theories/Reals/Rtopology.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/Ranalysis1.vo theories/Reals/RList.vo theories/Logic/Classical_Prop.vo theories/Logic/Classical_Pred_Type.vo -theories/Reals/TAF.vo: theories/Reals/TAF.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/Ranalysis1.vo theories/Reals/Rtopology.vo -theories/Reals/PSeries_reg.vo: theories/Reals/PSeries_reg.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Ranalysis1.vo theories/Arith/Max.vo theories/Arith/Even.vo -theories/Reals/Exp_prop.vo: theories/Reals/Exp_prop.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis1.vo theories/Reals/PSeries_reg.vo theories/Arith/Div2.vo theories/Arith/Even.vo theories/Arith/Max.vo -theories/Reals/Rtrigo_reg.vo: theories/Reals/Rtrigo_reg.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis1.vo theories/Reals/PSeries_reg.vo -theories/Reals/Rsqrt_def.vo: theories/Reals/Rsqrt_def.v theories/Bool/Sumbool.vo theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Ranalysis1.vo -theories/Reals/R_sqrt.vo: theories/Reals/R_sqrt.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/Rsqrt_def.vo -theories/Reals/Rtrigo_calc.vo: theories/Reals/Rtrigo_calc.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/R_sqrt.vo -theories/Reals/Rgeom.vo: theories/Reals/Rgeom.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/R_sqrt.vo -theories/Reals/Sqrt_reg.vo: theories/Reals/Sqrt_reg.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/Ranalysis1.vo theories/Reals/R_sqrt.vo -theories/Reals/Ranalysis4.vo: theories/Reals/Ranalysis4.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis1.vo theories/Reals/Ranalysis3.vo theories/Reals/Exp_prop.vo -theories/Reals/Rpower.vo: theories/Reals/Rpower.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis1.vo theories/Reals/Exp_prop.vo theories/Reals/Rsqrt_def.vo theories/Reals/R_sqrt.vo theories/Reals/TAF.vo theories/Reals/Ranalysis4.vo -theories/Reals/Ranalysis.vo: theories/Reals/Ranalysis.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/Rtrigo.vo theories/Reals/SeqSeries.vo theories/Reals/Ranalysis1.vo theories/Reals/Ranalysis2.vo theories/Reals/Ranalysis3.vo theories/Reals/Rtopology.vo theories/Reals/TAF.vo theories/Reals/PSeries_reg.vo theories/Reals/Exp_prop.vo theories/Reals/Rtrigo_reg.vo theories/Reals/Rsqrt_def.vo theories/Reals/R_sqrt.vo theories/Reals/Rtrigo_calc.vo theories/Reals/Rgeom.vo theories/Reals/RList.vo theories/Reals/Sqrt_reg.vo theories/Reals/Ranalysis4.vo theories/Reals/Rpower.vo -theories/Reals/NewtonInt.vo: theories/Reals/NewtonInt.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis.vo -theories/Reals/RiemannInt_SF.vo: theories/Reals/RiemannInt_SF.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/Ranalysis.vo theories/Logic/Classical_Prop.vo -theories/Reals/RiemannInt.vo: theories/Reals/RiemannInt.v theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Ranalysis.vo theories/Reals/RealsB.vo theories/Reals/RiemannInt_SF.vo theories/Logic/Classical_Prop.vo theories/Logic/Classical_Pred_Type.vo theories/Arith/Max.vo +theories/Reals/SplitRmult.vo: theories/Reals/SplitRmult.v theories/Reals/Rbase.vo +theories/Reals/ArithProp.vo: theories/Reals/ArithProp.v theories/Reals/Rbase.vo theories/Reals/Rbasic_fun.vo theories/Arith/Even.vo theories/Arith/Div2.vo +theories/Reals/Rfunctions.vo: theories/Reals/Rfunctions.v theories/Reals/Rbase.vo theories/Reals/R_Ifp.vo theories/Reals/Rbasic_fun.vo theories/Reals/R_sqr.vo theories/Reals/SplitAbsolu.vo theories/Reals/SplitRmult.vo theories/Reals/ArithProp.vo contrib/omega/Omega.vo theories/ZArith/Zpower.vo +theories/Reals/Rseries.vo: theories/Reals/Rseries.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Logic/Classical.vo theories/Arith/Compare.vo +theories/Reals/SeqProp.vo: theories/Reals/SeqProp.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Logic/Classical.vo theories/Arith/Max.vo +theories/Reals/Rcomplet.vo: theories/Reals/Rcomplet.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/SeqProp.vo theories/Arith/Max.vo +theories/Reals/PartSum.vo: theories/Reals/PartSum.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/Rcomplet.vo theories/Arith/Max.vo +theories/Reals/AltSeries.vo: theories/Reals/AltSeries.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/SeqProp.vo theories/Reals/PartSum.vo theories/Arith/Max.vo +theories/Reals/Binome.vo: theories/Reals/Binome.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/PartSum.vo +theories/Reals/Rsigma.vo: theories/Reals/Rsigma.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/PartSum.vo +theories/Reals/Rprod.vo: theories/Reals/Rprod.v theories/Arith/Compare.vo theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/PartSum.vo theories/Reals/Binome.vo +theories/Reals/Cauchy_prod.vo: theories/Reals/Cauchy_prod.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/PartSum.vo +theories/Reals/Alembert.vo: theories/Reals/Alembert.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/SeqProp.vo theories/Reals/PartSum.vo theories/Arith/Max.vo +theories/Reals/SeqSeries.vo: theories/Reals/SeqSeries.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rseries.vo theories/Reals/SeqProp.vo theories/Reals/Rcomplet.vo theories/Reals/PartSum.vo theories/Reals/AltSeries.vo theories/Reals/Binome.vo theories/Reals/Rsigma.vo theories/Reals/Rprod.vo theories/Reals/Cauchy_prod.vo theories/Reals/Alembert.vo +theories/Reals/Rtrigo_fun.vo: theories/Reals/Rtrigo_fun.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo +theories/Reals/Rtrigo_def.vo: theories/Reals/Rtrigo_def.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo_fun.vo theories/Arith/Max.vo +theories/Reals/Rtrigo_alt.vo: theories/Reals/Rtrigo_alt.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo_def.vo +theories/Reals/Cos_rel.vo: theories/Reals/Cos_rel.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo_def.vo +theories/Reals/Cos_plus.vo: theories/Reals/Cos_plus.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo_def.vo theories/Reals/Cos_rel.vo theories/Arith/Max.vo +theories/Reals/Rtrigo.vo: theories/Reals/Rtrigo.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo_fun.vo theories/Reals/Rtrigo_def.vo theories/Reals/Rtrigo_alt.vo theories/Reals/Cos_rel.vo theories/Reals/Cos_plus.vo theories/ZArith/ZArith_base.vo theories/ZArith/Zcomplements.vo theories/Logic/Classical_Prop.vo +theories/Reals/Rlimit.vo: theories/Reals/Rlimit.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Logic/Classical_Prop.vo contrib/fourier/Fourier.vo +theories/Reals/Rderiv.vo: theories/Reals/Rderiv.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rlimit.vo contrib/fourier/Fourier.vo theories/Logic/Classical_Prop.vo theories/Logic/Classical_Pred_Type.vo contrib/omega/Omega.vo +theories/Reals/RList.vo: theories/Reals/RList.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo +theories/Reals/Ranalysis1.vo: theories/Reals/Ranalysis1.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rlimit.vo theories/Reals/Rderiv.vo +theories/Reals/Ranalysis2.vo: theories/Reals/Ranalysis2.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Ranalysis1.vo contrib/omega/Omega.vo +theories/Reals/Ranalysis3.vo: theories/Reals/Ranalysis3.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Ranalysis1.vo theories/Reals/Ranalysis2.vo +theories/Reals/Rtopology.vo: theories/Reals/Rtopology.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Ranalysis1.vo theories/Reals/RList.vo theories/Logic/Classical_Prop.vo theories/Logic/Classical_Pred_Type.vo +theories/Reals/TAF.vo: theories/Reals/TAF.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Ranalysis1.vo theories/Reals/Rtopology.vo +theories/Reals/PSeries_reg.vo: theories/Reals/PSeries_reg.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Ranalysis1.vo theories/Arith/Max.vo theories/Arith/Even.vo +theories/Reals/Exp_prop.vo: theories/Reals/Exp_prop.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis1.vo theories/Reals/PSeries_reg.vo theories/Arith/Div2.vo theories/Arith/Even.vo theories/Arith/Max.vo +theories/Reals/Rtrigo_reg.vo: theories/Reals/Rtrigo_reg.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis1.vo theories/Reals/PSeries_reg.vo +theories/Reals/Rsqrt_def.vo: theories/Reals/Rsqrt_def.v theories/Bool/Sumbool.vo theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Ranalysis1.vo +theories/Reals/R_sqrt.vo: theories/Reals/R_sqrt.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rsqrt_def.vo +theories/Reals/Rtrigo_calc.vo: theories/Reals/Rtrigo_calc.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/R_sqrt.vo +theories/Reals/Rgeom.vo: theories/Reals/Rgeom.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/R_sqrt.vo +theories/Reals/Sqrt_reg.vo: theories/Reals/Sqrt_reg.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Ranalysis1.vo theories/Reals/R_sqrt.vo +theories/Reals/Ranalysis4.vo: theories/Reals/Ranalysis4.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis1.vo theories/Reals/Ranalysis3.vo theories/Reals/Exp_prop.vo +theories/Reals/Rpower.vo: theories/Reals/Rpower.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis1.vo theories/Reals/Exp_prop.vo theories/Reals/Rsqrt_def.vo theories/Reals/R_sqrt.vo theories/Reals/TAF.vo theories/Reals/Ranalysis4.vo +theories/Reals/Ranalysis.vo: theories/Reals/Ranalysis.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Rtrigo.vo theories/Reals/SeqSeries.vo theories/Reals/Ranalysis1.vo theories/Reals/Ranalysis2.vo theories/Reals/Ranalysis3.vo theories/Reals/Rtopology.vo theories/Reals/TAF.vo theories/Reals/PSeries_reg.vo theories/Reals/Exp_prop.vo theories/Reals/Rtrigo_reg.vo theories/Reals/Rsqrt_def.vo theories/Reals/R_sqrt.vo theories/Reals/Rtrigo_calc.vo theories/Reals/Rgeom.vo theories/Reals/RList.vo theories/Reals/Sqrt_reg.vo theories/Reals/Ranalysis4.vo theories/Reals/Rpower.vo +theories/Reals/NewtonInt.vo: theories/Reals/NewtonInt.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis.vo +theories/Reals/RiemannInt_SF.vo: theories/Reals/RiemannInt_SF.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/Ranalysis.vo theories/Logic/Classical_Prop.vo +theories/Reals/RiemannInt.vo: theories/Reals/RiemannInt.v theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Ranalysis.vo theories/Reals/Rbase.vo theories/Reals/RiemannInt_SF.vo theories/Logic/Classical_Prop.vo theories/Logic/Classical_Pred_Type.vo theories/Arith/Max.vo theories/Reals/Integration.vo: theories/Reals/Integration.v theories/Reals/NewtonInt.vo theories/Reals/RiemannInt_SF.vo theories/Reals/RiemannInt.vo -theories/Reals/Reals.vo: theories/Reals/Reals.v theories/Reals/RealsB.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis.vo theories/Reals/Integration.vo +theories/Reals/Reals.vo: theories/Reals/Reals.v theories/Reals/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis.vo theories/Reals/Integration.vo theories/Setoids/Setoid.vo: theories/Setoids/Setoid.v theories/Sorting/Heap.vo: theories/Sorting/Heap.v theories/Lists/PolyList.vo theories/Sets/Multiset.vo theories/Sorting/Permutation.vo theories/Relations/Relations.vo theories/Sorting/Sorting.vo theories/Sorting/Permutation.vo: theories/Sorting/Permutation.v theories/Relations/Relations.vo theories/Lists/PolyList.vo theories/Sets/Multiset.vo @@ -559,8 +559,8 @@ WELLFOUNDEDVO=theories/Wellfounded/Disjoint_Union.vo \ REALSBASEVO=theories/Reals/TypeSyntax.vo \ theories/Reals/Rdefinitions.vo theories/Reals/Rsyntax.vo \ - theories/Reals/Raxioms.vo theories/Reals/Rbase.vo \ - theories/Reals/DiscrR.vo theories/Reals/RealsB.vo \ + theories/Reals/Raxioms.vo theories/Reals/RIneq.vo \ + theories/Reals/DiscrR.vo theories/Reals/Rbase.vo \ REALS_basic= diff --git a/theories/Reals/Alembert.v b/theories/Reals/Alembert.v index d3414317a9..49f55cc559 100644 --- a/theories/Reals/Alembert.v +++ b/theories/Reals/Alembert.v @@ -8,7 +8,7 @@ (*i $Id$ i*) -Require RealsB. +Require Rbase. Require Rfunctions. Require Rseries. Require SeqProp. diff --git a/theories/Reals/AltSeries.v b/theories/Reals/AltSeries.v index 3bf7249b33..c5c4ec38a1 100644 --- a/theories/Reals/AltSeries.v +++ b/theories/Reals/AltSeries.v @@ -8,7 +8,7 @@ (*i $Id$ i*) -Require RealsB. +Require Rbase. Require Rfunctions. Require Rseries. Require SeqProp. @@ -145,7 +145,7 @@ Apply H7; Assumption. Unfold Rdiv; Apply Rlt_monotony_contra with ``2``. Sup0. Rewrite (Rmult_sym ``2``); Rewrite Rmult_assoc; Rewrite <- Rinv_l_sym; [Rewrite Rmult_1r | DiscrR]. -Rewrite Rbase.double. +Rewrite RIneq.double. Pattern 1 eps; Rewrite <- (Rplus_Or eps); Apply Rlt_compatibility; Assumption. Elim H10; Intro; Apply le_double. Rewrite <- H11; Apply le_trans with N. diff --git a/theories/Reals/ArithProp.v b/theories/Reals/ArithProp.v index f768c7b7a5..1d467a1113 100644 --- a/theories/Reals/ArithProp.v +++ b/theories/Reals/ArithProp.v @@ -8,7 +8,7 @@ (*i $Id$ i*) -Require RealsB. +Require Rbase. Require Rbasic_fun. Require Even. Require Div2. diff --git a/theories/Reals/Binome.v b/theories/Reals/Binome.v index 8f5ee9f46b..8b5406ee78 100644 --- a/theories/Reals/Binome.v +++ b/theories/Reals/Binome.v @@ -8,7 +8,7 @@ (*i $Id$ i*) -Require RealsB. +Require Rbase. Require Rfunctions. Require PartSum. @@ -177,4 +177,4 @@ Intro; Unfold C. Replace (minus p p) with O; [Idtac | Apply minus_n_n]. Replace (INR (fact O)) with R1; [Idtac | Reflexivity]. Rewrite Rmult_1r; Unfold Rdiv; Rewrite <- Rinv_r_sym; [Reflexivity | Apply INR_fact_neq_0]. -Qed.
\ No newline at end of file +Qed. diff --git a/theories/Reals/Cauchy_prod.v b/theories/Reals/Cauchy_prod.v index 4c29ea626a..cf962a0e2c 100644 --- a/theories/Reals/Cauchy_prod.v +++ b/theories/Reals/Cauchy_prod.v @@ -8,7 +8,7 @@ (*i $Id$ i*) -Require RealsB. +Require Rbase. Require Rfunctions. Require Rseries. Require PartSum. diff --git a/theories/Reals/Cos_plus.v b/theories/Reals/Cos_plus.v index 29e8cbe002..d1c167c568 100644 --- a/theories/Reals/Cos_plus.v +++ b/theories/Reals/Cos_plus.v @@ -8,7 +8,7 @@ (*i $Id$ i*) -Require RealsB. +Require Rbase. Require Rfunctions. Require SeqSeries. Require Rtrigo_def. @@ -1012,4 +1012,4 @@ Intro. Apply S_pred with O; Assumption. Apply lt_le_trans with N; Assumption. Unfold N; Apply lt_O_Sn. -Qed.
\ No newline at end of file +Qed. diff --git a/theories/Reals/Cos_rel.v b/theories/Reals/Cos_rel.v index 7640a9bf28..46f6b1abbd 100644 --- a/theories/Reals/Cos_rel.v +++ b/theories/Reals/Cos_rel.v @@ -8,7 +8,7 @@ (*i $Id$ i*) -Require RealsB. +Require Rbase. Require Rfunctions. Require SeqSeries. Require Rtrigo_def. @@ -355,4 +355,4 @@ Unfold sin_in in p_i. Unfold sin_in in s. Assert H1 := (unicite_sum [i:nat]``(sin_n i)*(pow (x*x) i)`` x0 x1 p_i s). Rewrite H1; Reflexivity. -Qed.
\ No newline at end of file +Qed. diff --git a/theories/Reals/DiscrR.v b/theories/Reals/DiscrR.v index 494a7d6856..4e917ddbf2 100644 --- a/theories/Reals/DiscrR.v +++ b/theories/Reals/DiscrR.v @@ -8,7 +8,7 @@ (*i $Id$ i*) -Require Rbase. +Require RIneq. Recursive Tactic Definition Isrealint trm:= Match trm With diff --git a/theories/Reals/Exp_prop.v b/theories/Reals/Exp_prop.v index 3c2b16f10e..d5c851f8e2 100644 --- a/theories/Reals/Exp_prop.v +++ b/theories/Reals/Exp_prop.v @@ -8,7 +8,7 @@ (*i $Id$ i*) -Require RealsB. +Require Rbase. Require Rfunctions. Require SeqSeries. Require Rtrigo. diff --git a/theories/Reals/NewtonInt.v b/theories/Reals/NewtonInt.v index 031870b931..6346fc2eec 100644 --- a/theories/Reals/NewtonInt.v +++ b/theories/Reals/NewtonInt.v @@ -8,7 +8,7 @@ (*i $Id$ i*) -Require RealsB. +Require Rbase. Require Rfunctions. Require SeqSeries. Require Rtrigo. @@ -198,7 +198,7 @@ Symmetry; Assumption. Assert H8 := (derive_pt_eq_1 F0 x (f x) x0 H7); Unfold derivable_pt_lim in H8; Intros; Elim (H8 ? H9); Intros; Pose D := (Rmin x1 ``b-x``). Assert H11 : ``0<D``. Unfold D; Unfold Rmin; Case (total_order_Rle x1 ``b-x``); Intro. -Apply (Rbase.cond_pos x1). +Apply (cond_pos x1). Apply Rlt_Rminus; Assumption. Exists (mkposreal ? H11); Intros; Case (total_order_Rle x b); Intro. Case (total_order_Rle ``x+h`` b); Intro. @@ -225,8 +225,8 @@ Symmetry; Assumption. Assert H11 := (derive_pt_eq_1 F0 x (f x) x1 H9); Assert H12 := (derive_pt_eq_1 F1 x (f x) x0 H10); Assert H13 : (derivable_pt_lim [x:R]Cases (total_order_Rle x b) of (leftT _) => (F0 x) | (rightT _) => ``(F1 x)+((F0 b)-(F1 b))`` end x (f x)). Unfold derivable_pt_lim; Unfold derivable_pt_lim in H11 H12; Intros; Elim (H11 ? H13); Elim (H12 ? H13); Intros; Pose D := (Rmin x2 x3); Assert H16 : ``0<D``. Unfold D; Unfold Rmin; Case (total_order_Rle x2 x3); Intro. -Apply (Rbase.cond_pos x2). -Apply (Rbase.cond_pos x3). +Apply (cond_pos x2). +Apply (cond_pos x3). Exists (mkposreal ? H16); Intros; Case (total_order_Rle x b); Intro. Case (total_order_Rle ``x+h`` b); Intro. Apply H15. @@ -248,7 +248,7 @@ Unfold derivable_pt_lim; Assert H7 : ``(derive_pt F1 x x0)==(f x)``. Symmetry; Assumption. Assert H8 := (derive_pt_eq_1 F1 x (f x) x0 H7); Unfold derivable_pt_lim in H8; Intros; Elim (H8 ? H9); Intros; Pose D := (Rmin x1 ``x-b``); Assert H11 : ``0<D``. Unfold D; Unfold Rmin; Case (total_order_Rle x1 ``x-b``); Intro. -Apply (Rbase.cond_pos x1). +Apply (cond_pos x1). Apply Rlt_Rminus; Assumption. Exists (mkposreal ? H11); Intros; Case (total_order_Rle x b); Intro. Elim (Rlt_antirefl ? (Rle_lt_trans ? ? ? r0 r)). diff --git a/theories/Reals/PSeries_reg.v b/theories/Reals/PSeries_reg.v index d056387f41..d519b10598 100644 --- a/theories/Reals/PSeries_reg.v +++ b/theories/Reals/PSeries_reg.v @@ -8,7 +8,7 @@ (*i $Id$ i*) -Require RealsB. +Require Rbase. Require Rfunctions. Require SeqSeries. Require Ranalysis1. diff --git a/theories/Reals/PartSum.v b/theories/Reals/PartSum.v index 24d145392b..a072485081 100644 --- a/theories/Reals/PartSum.v +++ b/theories/Reals/PartSum.v @@ -8,7 +8,7 @@ (*i $Id$ i*) -Require RealsB. +Require Rbase. Require Rfunctions. Require Rseries. Require Rcomplet. diff --git a/theories/Reals/RList.v b/theories/Reals/RList.v index 1d2b6c23b4..7f8a92d085 100644 --- a/theories/Reals/RList.v +++ b/theories/Reals/RList.v @@ -8,7 +8,7 @@ (*i $Id$ i*) -Require RealsB. +Require Rbase. Require Rfunctions. Inductive Rlist : Type := @@ -423,4 +423,4 @@ Repeat Rewrite RList_P23; Simpl; Rewrite RList_P23 in H1; Rewrite plus_sym in H1 Rewrite RList_P23; Rewrite plus_sym; Reflexivity. Change (S (minus m (longueur l1)))=(minus (S m) (longueur l1)); Apply minus_Sn_m; Assumption. Replace (cons r r0) with (cons_Rlist (cons r nil) r0); [Symmetry; Apply RList_P27 | Reflexivity]. -Qed.
\ No newline at end of file +Qed. diff --git a/theories/Reals/R_Ifp.v b/theories/Reals/R_Ifp.v index 33e60448a9..44e35a6d97 100644 --- a/theories/Reals/R_Ifp.v +++ b/theories/Reals/R_Ifp.v @@ -13,7 +13,7 @@ (* *) (**********************************************************) -Require RealsB. +Require Rbase. Require Omega. (*********************************************************) diff --git a/theories/Reals/R_sqr.v b/theories/Reals/R_sqr.v index 8a711809e7..0da625bab9 100644 --- a/theories/Reals/R_sqr.v +++ b/theories/Reals/R_sqr.v @@ -8,7 +8,7 @@ (*i $Id$ i*) -Require RealsB. +Require Rbase. Require Rbasic_fun. (****************************************************) diff --git a/theories/Reals/R_sqrt.v b/theories/Reals/R_sqrt.v index b830f213a9..19e3d26023 100644 --- a/theories/Reals/R_sqrt.v +++ b/theories/Reals/R_sqrt.v @@ -8,7 +8,7 @@ (*i $Id$ i*) -Require RealsB. +Require Rbase. Require Rfunctions. Require Rsqrt_def. @@ -247,4 +247,4 @@ Unfold Rdiv; Rewrite <- Ropp_mul1. Rewrite Ropp_distr2. Reflexivity. Reflexivity. -Qed.
\ No newline at end of file +Qed. diff --git a/theories/Reals/Ranalysis.v b/theories/Reals/Ranalysis.v index 6727222339..ec2cd0c464 100644 --- a/theories/Reals/Ranalysis.v +++ b/theories/Reals/Ranalysis.v @@ -8,7 +8,7 @@ (*i $Id$ i*) -Require RealsB. +Require Rbase. Require Rfunctions. Require Rtrigo. Require SeqSeries. @@ -476,4 +476,4 @@ Let aux = (RewTerm trm) In IntroHypL aux ?2; Let aux2 = (ConsProof aux ?2) In Try (Replace (derive_pt ?1 ?2 ?3) with (derive_pt aux ?2 aux2); [SimplifyDerive aux ?2; Try Unfold plus_fct minus_fct mult_fct div_fct id fct_cte inv_fct opp_fct; Try Ring | Try Apply pr_nu]) Orelse IsDiff_pt. (**********) -Tactic Definition Reg () := Regularity ().
\ No newline at end of file +Tactic Definition Reg () := Regularity (). diff --git a/theories/Reals/Ranalysis1.v b/theories/Reals/Ranalysis1.v index 8ba7c1e22c..0c1515d9ff 100644 --- a/theories/Reals/Ranalysis1.v +++ b/theories/Reals/Ranalysis1.v @@ -8,7 +8,7 @@ (*i $Id$ i*) -Require RealsB. +Require Rbase. Require Rfunctions. Require Export Rlimit. Require Export Rderiv. diff --git a/theories/Reals/Ranalysis2.v b/theories/Reals/Ranalysis2.v index 5af07f40fc..69671c5513 100644 --- a/theories/Reals/Ranalysis2.v +++ b/theories/Reals/Ranalysis2.v @@ -8,7 +8,7 @@ (*i $Id$ i*) -Require RealsB. +Require Rbase. Require Rfunctions. Require Ranalysis1. Require Omega. diff --git a/theories/Reals/Ranalysis3.v b/theories/Reals/Ranalysis3.v index 5ef28ab37b..20c02f3602 100644 --- a/theories/Reals/Ranalysis3.v +++ b/theories/Reals/Ranalysis3.v @@ -8,7 +8,7 @@ (*i $Id$ i*) -Require RealsB. +Require Rbase. Require Rfunctions. Require Ranalysis1. Require Ranalysis2. diff --git a/theories/Reals/Ranalysis4.v b/theories/Reals/Ranalysis4.v index 63611eea47..5c81a076e7 100644 --- a/theories/Reals/Ranalysis4.v +++ b/theories/Reals/Ranalysis4.v @@ -8,7 +8,7 @@ (*i $Id$ i*) -Require RealsB. +Require Rbase. Require Rfunctions. Require SeqSeries. Require Rtrigo. @@ -309,4 +309,4 @@ Qed. Lemma derive_pt_sinh : (x:R) (derive_pt sinh x (derivable_pt_sinh x))==(cosh x). Intro; Apply derive_pt_eq_0. Apply derivable_pt_lim_sinh. -Qed.
\ No newline at end of file +Qed. diff --git a/theories/Reals/Rbase.v b/theories/Reals/Rbase.v index 09dadee90e..d0c8e1f308 100644 --- a/theories/Reals/Rbase.v +++ b/theories/Reals/Rbase.v @@ -8,1593 +8,8 @@ (*i $Id$ i*) -(***************************************************************************) -(** Basic lemmas for the classical reals numbers *) -(***************************************************************************) - +Require Export Rdefinitions. +Require Export TypeSyntax. Require Export Raxioms. -Require Export ZArithRing. -Require Omega. -Require Export Field. - -(***************************************************************************) -(** Instantiating Ring tactic on reals *) -(***************************************************************************) - -Lemma RTheory : (Ring_Theory Rplus Rmult R1 R0 Ropp [x,y:R]false). - Split. - Exact Rplus_sym. - Symmetry; Apply Rplus_assoc. - Exact Rmult_sym. - Symmetry; Apply Rmult_assoc. - Intro; Apply Rplus_Ol. - Intro; Apply Rmult_1l. - Exact Rplus_Ropp_r. - Intros. - Rewrite Rmult_sym. - Rewrite (Rmult_sym n p). - Rewrite (Rmult_sym m p). - Apply Rmult_Rplus_distr. - Intros; Contradiction. -Defined. - -Add Field R Rplus Rmult R1 R0 Ropp [x,y:R]false Rinv RTheory Rinv_l - with minus:=Rminus div:=Rdiv. - -(**************************************************************************) -(** Relation between orders and equality *) -(**************************************************************************) - -(**********) -Lemma Rlt_antirefl:(r:R)~``r<r``. - Generalize Rlt_antisym. Intuition EAuto. -Qed. -Hints Resolve Rlt_antirefl : real. - -Lemma Rlt_not_eq:(r1,r2:R)``r1<r2``->``r1<>r2``. - Red; Intros r1 r2 H H0; Apply (Rlt_antirefl r1). - Pattern 2 r1; Rewrite H0; Trivial. -Qed. - -Lemma Rgt_not_eq:(r1,r2:R)``r1>r2``->``r1<>r2``. -Intros; Apply sym_not_eqT; Apply Rlt_not_eq; Auto with real. -Qed. - -(**********) -Lemma imp_not_Req:(r1,r2:R)(``r1<r2``\/ ``r1>r2``) -> ``r1<>r2``. -Generalize Rlt_not_eq Rgt_not_eq. Intuition EAuto. -Qed. -Hints Resolve imp_not_Req : real. - -(** Reasoning by case on equalities and order *) - -(**********) -Lemma Req_EM:(r1,r2:R)(r1==r2)\/``r1<>r2``. -Intros ; Generalize (total_order_T r1 r2) imp_not_Req ; Intuition EAuto 3. -Qed. -Hints Resolve Req_EM : real. - -(**********) -Lemma total_order:(r1,r2:R)``r1<r2``\/(r1==r2)\/``r1>r2``. -Intros;Generalize (total_order_T r1 r2);Tauto. -Qed. - -(**********) -Lemma not_Req:(r1,r2:R)``r1<>r2``->(``r1<r2``\/``r1>r2``). -Intros; Generalize (total_order_T r1 r2) ; Tauto. -Qed. - - -(*********************************************************************************) -(** Order Lemma : relating [<], [>], [<=] and [>=] *) -(*********************************************************************************) - -(**********) -Lemma Rlt_le:(r1,r2:R)``r1<r2``-> ``r1<=r2``. -Intros ; Red ; Tauto. -Qed. -Hints Resolve Rlt_le : real. - -(**********) -Lemma Rle_ge : (r1,r2:R)``r1<=r2`` -> ``r2>=r1``. -NewDestruct 1; Red; Auto with real. -Qed. - -(**********) -Lemma Rge_le : (r1,r2:R)``r1>=r2`` -> ``r2<=r1``. -NewDestruct 1; Red; Auto with real. -Qed. - -(**********) -Lemma not_Rle:(r1,r2:R)~(``r1<=r2``)->``r1>r2``. -Intros r1 r2 ; Generalize (total_order r1 r2) ; Unfold Rle; Tauto. -Qed. - -Hints Immediate Rle_ge Rge_le not_Rle : real. - -(**********) -Lemma Rlt_le_not:(r1,r2:R)``r2<r1``->~(``r1<=r2``). -Generalize Rlt_antisym imp_not_Req ; Unfold Rle. -Intuition EAuto 3. -Qed. - -Lemma Rle_not:(r1,r2:R)``r1>r2`` -> ~(``r1<=r2``). -Proof Rlt_le_not. - -Hints Immediate Rlt_le_not : real. - -Lemma Rle_not_lt: (r1, r2:R) ``r2 <= r1`` ->~ (``r1<r2``). -Intros r1 r2. Generalize (Rlt_antisym r1 r2) (imp_not_Req r1 r2). -Unfold Rle; Intuition. -Qed. - -(**********) -Lemma Rlt_ge_not:(r1,r2:R)``r1<r2``->~(``r1>=r2``). -Generalize Rlt_le_not. Unfold Rle Rge. Intuition EAuto 3. -Qed. - -Hints Immediate Rlt_ge_not : real. - -(**********) -Lemma eq_Rle:(r1,r2:R)r1==r2->``r1<=r2``. -Unfold Rle; Tauto. -Qed. -Hints Immediate eq_Rle : real. - -Lemma eq_Rge:(r1,r2:R)r1==r2->``r1>=r2``. -Unfold Rge; Tauto. -Qed. -Hints Immediate eq_Rge : real. - -Lemma eq_Rle_sym:(r1,r2:R)r2==r1->``r1<=r2``. -Unfold Rle; Auto. -Qed. -Hints Immediate eq_Rle_sym : real. - -Lemma eq_Rge_sym:(r1,r2:R)r2==r1->``r1>=r2``. -Unfold Rge; Auto. -Qed. -Hints Immediate eq_Rge_sym : real. - -Lemma Rle_antisym : (r1,r2:R)``r1<=r2`` -> ``r2<=r1``-> r1==r2. -Intros r1 r2; Generalize (Rlt_antisym r1 r2) ; Unfold Rle ; Intuition. -Qed. -Hints Resolve Rle_antisym : real. - -(**********) -Lemma Rle_le_eq:(r1,r2:R)(``r1<=r2``/\``r2<=r1``)<->(r1==r2). -Intuition. -Qed. - -Lemma Rlt_rew : (x,x',y,y':R)``x==x'``->``x'<y'`` -> `` y' == y`` -> ``x < y``. -Intros; Replace x with x'; Replace y with y'; Assumption. -Qed. - -(**********) -Lemma Rle_trans:(r1,r2,r3:R) ``r1<=r2``->``r2<=r3``->``r1<=r3``. -Generalize trans_eqT Rlt_trans Rlt_rew. -Unfold Rle. -Intuition EAuto 2. -Qed. - -(**********) -Lemma Rle_lt_trans:(r1,r2,r3:R)``r1<=r2``->``r2<r3``->``r1<r3``. -Generalize Rlt_trans Rlt_rew. -Unfold Rle. -Intuition EAuto 2. -Qed. - -(**********) -Lemma Rlt_le_trans:(r1,r2,r3:R)``r1<r2``->``r2<=r3``->``r1<r3``. -Generalize Rlt_trans Rlt_rew; Unfold Rle; Intuition EAuto 2. -Qed. - - -(** Decidability of the order *) -Lemma total_order_Rlt:(r1,r2:R)(sumboolT ``r1<r2`` ~(``r1<r2``)). -Intros;Generalize (total_order_T r1 r2) (imp_not_Req r1 r2) ; Intuition. -Qed. - -(**********) -Lemma total_order_Rle:(r1,r2:R)(sumboolT ``r1<=r2`` ~(``r1<=r2``)). -Intros r1 r2. -Generalize (total_order_T r1 r2) (imp_not_Req r1 r2). -Intuition EAuto 4 with real. -Qed. - -(**********) -Lemma total_order_Rgt:(r1,r2:R)(sumboolT ``r1>r2`` ~(``r1>r2``)). -Intros;Unfold Rgt;Intros;Apply total_order_Rlt. -Qed. - -(**********) -Lemma total_order_Rge:(r1,r2:R)(sumboolT (``r1>=r2``) ~(``r1>=r2``)). -Intros;Generalize (total_order_Rle r2 r1);Intuition. -Qed. - -Lemma total_order_Rlt_Rle:(r1,r2:R)(sumboolT ``r1<r2`` ``r2<=r1``). -Intros;Generalize (total_order_T r1 r2); Intuition. -Qed. - -Lemma Rle_or_lt: (n, m:R)(Rle n m) \/ (Rlt m n). -Intros n m; Elim (total_order_Rlt_Rle m n);Auto with real. -Qed. - -Lemma total_order_Rle_Rlt_eq :(r1,r2:R)``r1<=r2``-> - (sumboolT ``r1<r2`` ``r1==r2``). -Intros r1 r2 H;Generalize (total_order_T r1 r2); Intuition. -Qed. - -(**********) -Lemma inser_trans_R:(n,m,p,q:R)``n<=m<p``-> (sumboolT ``n<=m<q`` ``q<=m<p``). -Intros; Generalize (total_order_Rlt_Rle m q); Intuition. -Qed. - -(****************************************************************) -(** Field Lemmas *) -(* This part contains lemma involving the Fields operations *) -(****************************************************************) -(*********************************************************) -(** Addition *) -(*********************************************************) - -Lemma Rplus_ne:(r:R)``r+0==r``/\``0+r==r``. -Intro;Split;Ring. -Qed. -Hints Resolve Rplus_ne : real v62. - -Lemma Rplus_Or:(r:R)``r+0==r``. -Intro; Ring. -Qed. -Hints Resolve Rplus_Or : real. - -(**********) -Lemma Rplus_Ropp_l:(r:R)``(-r)+r==0``. - Intro; Ring. -Qed. -Hints Resolve Rplus_Ropp_l : real. - - -(**********) -Lemma Rplus_Ropp:(x,y:R)``x+y==0``->``y== -x``. - Intros; Replace y with ``(-x+x)+y``; - [ Rewrite -> Rplus_assoc; Rewrite -> H; Ring - | Ring ]. -Qed. - -(*i New i*) -Hint eqT_R_congr : real := Resolve (congr_eqT R). - -Lemma Rplus_plus_r:(r,r1,r2:R)(r1==r2)->``r+r1==r+r2``. - Auto with real. -Qed. - -(*i Old i*)Hints Resolve Rplus_plus_r : v62. - -(**********) -Lemma r_Rplus_plus:(r,r1,r2:R)``r+r1==r+r2``->r1==r2. - Intros; Transitivity ``(-r+r)+r1``. - Ring. - Transitivity ``(-r+r)+r2``. - Repeat Rewrite -> Rplus_assoc; Rewrite <- H; Reflexivity. - Ring. -Qed. -Hints Resolve r_Rplus_plus : real. - -(**********) -Lemma Rplus_ne_i:(r,b:R)``r+b==r`` -> ``b==0``. - Intros r b; Pattern 2 r; Replace r with ``r+0``; - EAuto with real. -Qed. - -(***********************************************************) -(** Multiplication *) -(***********************************************************) - -(**********) -Lemma Rinv_r:(r:R)``r<>0``->``r* (/r)==1``. - Intros; Rewrite -> Rmult_sym; Auto with real. -Qed. -Hints Resolve Rinv_r : real. - -Lemma Rinv_l_sym:(r:R)``r<>0``->``1==(/r) * r``. - Symmetry; Auto with real. -Qed. - -Lemma Rinv_r_sym:(r:R)``r<>0``->``1==r* (/r)``. - Symmetry; Auto with real. -Qed. -Hints Resolve Rinv_l_sym Rinv_r_sym : real. - - -(**********) -Lemma Rmult_Or :(r:R) ``r*0==0``. -Intro; Ring. -Qed. -Hints Resolve Rmult_Or : real v62. - -(**********) -Lemma Rmult_Ol:(r:R)(``0*r==0``). -Intro; Ring. -Qed. -Hints Resolve Rmult_Ol : real v62. - -(**********) -Lemma Rmult_ne:(r:R)``r*1==r``/\``1*r==r``. -Intro;Split;Ring. -Qed. -Hints Resolve Rmult_ne : real v62. - -(**********) -Lemma Rmult_1r:(r:R)(``r*1==r``). -Intro; Ring. -Qed. -Hints Resolve Rmult_1r : real. - -(**********) -Lemma Rmult_mult_r:(r,r1,r2:R)r1==r2->``r*r1==r*r2``. - Auto with real. -Qed. - -(*i OLD i*)Hints Resolve Rmult_mult_r : v62. - -(**********) -Lemma r_Rmult_mult:(r,r1,r2:R)(``r*r1==r*r2``)->``r<>0``->(r1==r2). - Intros; Transitivity ``(/r * r)*r1``. - Rewrite Rinv_l; Auto with real. - Transitivity ``(/r * r)*r2``. - Repeat Rewrite Rmult_assoc; Rewrite H; Trivial. - Rewrite Rinv_l; Auto with real. -Qed. - -(**********) -Lemma without_div_Od:(r1,r2:R)``r1*r2==0`` -> ``r1==0`` \/ ``r2==0``. - Intros; Case (Req_EM r1 ``0``); [Intro Hz | Intro Hnotz]. - Auto. - Right; Apply r_Rmult_mult with r1; Trivial. - Rewrite H; Auto with real. -Qed. - -(**********) -Lemma without_div_Oi:(r1,r2:R) ``r1==0``\/``r2==0`` -> ``r1*r2==0``. - Intros r1 r2 [H | H]; Rewrite H; Auto with real. -Qed. - -Hints Resolve without_div_Oi : real. - -(**********) -Lemma without_div_Oi1:(r1,r2:R) ``r1==0`` -> ``r1*r2==0``. - Auto with real. -Qed. - -(**********) -Lemma without_div_Oi2:(r1,r2:R) ``r2==0`` -> ``r1*r2==0``. - Auto with real. -Qed. - - -(**********) -Lemma without_div_O_contr:(r1,r2:R)``r1*r2<>0`` -> ``r1<>0`` /\ ``r2<>0``. -Intros r1 r2 H; Split; Red; Intro; Apply H; Auto with real. -Qed. - -(**********) -Lemma mult_non_zero :(r1,r2:R)``r1<>0`` /\ ``r2<>0`` -> ``r1*r2<>0``. -Red; Intros r1 r2 (H1,H2) H. -Case (without_div_Od r1 r2); Auto with real. -Qed. -Hints Resolve mult_non_zero : real. - -(**********) -Lemma Rmult_Rplus_distrl: - (r1,r2,r3:R) ``(r1+r2)*r3 == (r1*r3)+(r2*r3)``. -Intros; Ring. -Qed. - -(** Square function *) - -(***********) -Definition Rsqr:R->R:=[r:R]``r*r``. - -(***********) -Lemma Rsqr_O:(Rsqr ``0``)==``0``. - Unfold Rsqr; Auto with real. -Qed. - -(***********) -Lemma Rsqr_r_R0:(r:R)(Rsqr r)==``0``->``r==0``. -Unfold Rsqr;Intros;Elim (without_div_Od r r H);Trivial. -Qed. - -(*********************************************************) -(** Opposite *) -(*********************************************************) - -(**********) -Lemma eq_Ropp:(r1,r2:R)(r1==r2)->``-r1 == -r2``. - Auto with real. -Qed. -Hints Resolve eq_Ropp : real. - -(**********) -Lemma Ropp_O:``-0==0``. - Ring. -Qed. -Hints Resolve Ropp_O : real v62. - -(**********) -Lemma eq_RoppO:(r:R)``r==0``-> ``-r==0``. - Intros; Rewrite -> H; Auto with real. -Qed. -Hints Resolve eq_RoppO : real. - -(**********) -Lemma Ropp_Ropp:(r:R)``-(-r)==r``. - Intro; Ring. -Qed. -Hints Resolve Ropp_Ropp : real. - -(*********) -Lemma Ropp_neq:(r:R)``r<>0``->``-r<>0``. -Red;Intros r H H0. -Apply H. -Transitivity ``-(-r)``; Auto with real. -Qed. -Hints Resolve Ropp_neq : real. - -(**********) -Lemma Ropp_distr1:(r1,r2:R)``-(r1+r2)==(-r1 + -r2)``. - Intros; Ring. -Qed. -Hints Resolve Ropp_distr1 : real. - -(** Opposite and multiplication *) - -Lemma Ropp_mul1:(r1,r2:R)``(-r1)*r2 == -(r1*r2)``. - Intros; Ring. -Qed. -Hints Resolve Ropp_mul1 : real. - -(**********) -Lemma Ropp_mul2:(r1,r2:R)``(-r1)*(-r2)==r1*r2``. - Intros; Ring. -Qed. -Hints Resolve Ropp_mul2 : real. - -Lemma Ropp_mul3 : (r1,r2:R) ``r1*(-r2) == -(r1*r2)``. -Intros; Rewrite <- Ropp_mul1; Ring. -Qed. - -(** Substraction *) - -Lemma minus_R0:(r:R)``r-0==r``. -Intro;Ring. -Qed. -Hints Resolve minus_R0 : real. - -Lemma Rminus_Ropp:(r:R)``0-r==-r``. -Intro;Ring. -Qed. -Hints Resolve Rminus_Ropp : real. - -(**********) -Lemma Ropp_distr2:(r1,r2:R)``-(r1-r2)==r2-r1``. - Intros; Ring. -Qed. -Hints Resolve Ropp_distr2 : real. - -Lemma Ropp_distr3:(r1,r2:R)``-(r2-r1)==r1-r2``. -Intros; Ring. -Qed. -Hints Resolve Ropp_distr3 : real. - -(**********) -Lemma eq_Rminus:(r1,r2:R)(r1==r2)->``r1-r2==0``. - Intros; Rewrite H; Ring. -Qed. -Hints Resolve eq_Rminus : real. - -(**********) -Lemma Rminus_eq:(r1,r2:R)``r1-r2==0`` -> r1==r2. - Intros r1 r2; Unfold Rminus; Rewrite -> Rplus_sym; Intro. - Rewrite <- (Ropp_Ropp r2); Apply (Rplus_Ropp (Ropp r2) r1 H). -Qed. -Hints Immediate Rminus_eq : real. - -Lemma Rminus_eq_right:(r1,r2:R)``r2-r1==0`` -> r1==r2. -Intros;Generalize (Rminus_eq r2 r1 H);Clear H;Intro H;Rewrite H;Ring. -Qed. -Hints Immediate Rminus_eq_right : real. - -Lemma Rplus_Rminus: (p,q:R)``p+(q-p)``==q. -Intros; Ring. -Qed. -Hints Resolve Rplus_Rminus:real. - -(**********) -Lemma Rminus_eq_contra:(r1,r2:R)``r1<>r2``->``r1-r2<>0``. -Red; Intros r1 r2 H H0. -Apply H; Auto with real. -Qed. -Hints Resolve Rminus_eq_contra : real. - -Lemma Rminus_not_eq:(r1,r2:R)``r1-r2<>0``->``r1<>r2``. -Red; Intros; Elim H; Apply eq_Rminus; Auto. -Qed. -Hints Resolve Rminus_not_eq : real. - -Lemma Rminus_not_eq_right:(r1,r2:R)``r2-r1<>0`` -> ``r1<>r2``. -Red; Intros;Elim H;Rewrite H0; Ring. -Qed. -Hints Resolve Rminus_not_eq_right : real. - -Lemma not_sym : (r1,r2:R) ``r1<>r2`` -> ``r2<>r1``. -Intros; Red; Intro H0; Rewrite H0 in H; Elim H; Reflexivity. -Qed. - -(**********) -Lemma Rminus_distr: (x,y,z:R) ``x*(y-z)==(x*y) - (x*z)``. -Intros; Ring. -Qed. - -(** Inverse *) -Lemma Rinv_R1:``/1==1``. -Field;Auto with real. -Qed. -Hints Resolve Rinv_R1 : real. - -(*********) -Lemma Rinv_neq_R0:(r:R)``r<>0``->``(/r)<>0``. -Red; Intros; Apply R1_neq_R0. -Replace ``1`` with ``(/r) * r``; Auto with real. -Qed. -Hints Resolve Rinv_neq_R0 : real. - -(*********) -Lemma Rinv_Rinv:(r:R)``r<>0``->``/(/r)==r``. -Intros;Field;Auto with real. -Qed. -Hints Resolve Rinv_Rinv : real. - -(*********) -Lemma Rinv_Rmult:(r1,r2:R)``r1<>0``->``r2<>0``->``/(r1*r2)==(/r1)*(/r2)``. -Intros;Field;Auto with real. -Qed. - -(*********) -Lemma Ropp_Rinv:(r:R)``r<>0``->``-(/r)==/(-r)``. -Intros;Field;Auto with real. -Qed. - -Lemma Rinv_r_simpl_r : (r1,r2:R)``r1<>0``->``r1*(/r1)*r2==r2``. -Intros; Transitivity ``1*r2``; Auto with real. -Rewrite Rinv_r; Auto with real. -Qed. - -Lemma Rinv_r_simpl_l : (r1,r2:R)``r1<>0``->``r2*r1*(/r1)==r2``. -Intros; Transitivity ``r2*1``; Auto with real. -Transitivity ``r2*(r1*/r1)``; Auto with real. -Qed. - -Lemma Rinv_r_simpl_m : (r1,r2:R)``r1<>0``->``r1*r2*(/r1)==r2``. -Intros; Transitivity ``r2*1``; Auto with real. -Transitivity ``r2*(r1*/r1)``; Auto with real. -Ring. -Qed. -Hints Resolve Rinv_r_simpl_l Rinv_r_simpl_r Rinv_r_simpl_m : real. - -(*********) -Lemma Rinv_Rmult_simpl:(a,b,c:R)``a<>0``->``(a*(/b))*(c*(/a))==c*(/b)``. -Intros. -Transitivity ``(a*/a)*(c*(/b))``; Auto with real. -Ring. -Qed. - -(** Order and addition *) - -Lemma Rlt_compatibility_r:(r,r1,r2:R)``r1<r2``->``r1+r<r2+r``. -Intros. -Rewrite (Rplus_sym r1 r); Rewrite (Rplus_sym r2 r); Auto with real. -Qed. - -Hints Resolve Rlt_compatibility_r : real. - -(**********) -Lemma Rlt_anti_compatibility: (r,r1,r2:R)``r+r1 < r+r2`` -> ``r1<r2``. -Intros; Cut ``(-r+r)+r1 < (-r+r)+r2``. -Rewrite -> Rplus_Ropp_l. -Elim (Rplus_ne r1); Elim (Rplus_ne r2); Intros; Rewrite <- H3; - Rewrite <- H1; Auto with zarith real. -Rewrite -> Rplus_assoc; Rewrite -> Rplus_assoc; - Apply (Rlt_compatibility ``-r`` ``r+r1`` ``r+r2`` H). -Qed. - -(**********) -Lemma Rle_compatibility:(r,r1,r2:R)``r1<=r2`` -> ``r+r1 <= r+r2 ``. -Unfold Rle; Intros; Elim H; Intro. -Left; Apply (Rlt_compatibility r r1 r2 H0). -Right; Rewrite <- H0; Auto with zarith real. -Qed. - -(**********) -Lemma Rle_compatibility_r:(r,r1,r2:R)``r1<=r2`` -> ``r1+r<=r2+r``. -Unfold Rle; Intros; Elim H; Intro. -Left; Apply (Rlt_compatibility_r r r1 r2 H0). -Right; Rewrite <- H0; Auto with real. -Qed. - -Hints Resolve Rle_compatibility Rle_compatibility_r : real. - -(**********) -Lemma Rle_anti_compatibility: (r,r1,r2:R)``r+r1<=r+r2`` -> ``r1<=r2``. -Unfold Rle; Intros; Elim H; Intro. -Left; Apply (Rlt_anti_compatibility r r1 r2 H0). -Right; Apply (r_Rplus_plus r r1 r2 H0). -Qed. - -(**********) -Lemma sum_inequa_Rle_lt:(a,x,b,c,y,d:R)``a<=x`` -> ``x<b`` -> - ``c<y`` -> ``y<=d`` -> ``a+c < x+y < b+d``. -Intros;Split. -Apply Rlt_le_trans with ``a+y``; Auto with real. -Apply Rlt_le_trans with ``b+y``; Auto with real. -Qed. - -(*********) -Lemma Rplus_lt:(r1,r2,r3,r4:R)``r1<r2`` -> ``r3<r4`` -> ``r1+r3 < r2+r4``. -Intros; Apply Rlt_trans with ``r2+r3``; Auto with real. -Qed. - -Lemma Rplus_le:(r1,r2,r3,r4:R)``r1<=r2`` -> ``r3<=r4`` -> ``r1+r3 <= r2+r4``. -Intros; Apply Rle_trans with ``r2+r3``; Auto with real. -Qed. - -(*********) -Lemma Rplus_lt_le_lt:(r1,r2,r3,r4:R)``r1<r2`` -> ``r3<=r4`` -> - ``r1+r3 < r2+r4``. -Intros; Apply Rlt_le_trans with ``r2+r3``; Auto with real. -Qed. - -(*********) -Lemma Rplus_le_lt_lt:(r1,r2,r3,r4:R)``r1<=r2`` -> ``r3<r4`` -> - ``r1+r3 < r2+r4``. -Intros; Apply Rle_lt_trans with ``r2+r3``; Auto with real. -Qed. - -Hints Immediate Rplus_lt Rplus_le Rplus_lt_le_lt Rplus_le_lt_lt : real. - -(** Order and Opposite *) - -(**********) -Lemma Rgt_Ropp:(r1,r2:R) ``r1 > r2`` -> ``-r1 < -r2``. -Unfold Rgt; Intros. -Apply (Rlt_anti_compatibility ``r2+r1``). -Replace ``r2+r1+(-r1)`` with r2. -Replace ``r2+r1+(-r2)`` with r1. -Trivial. -Ring. -Ring. -Qed. -Hints Resolve Rgt_Ropp. - -(**********) -Lemma Rlt_Ropp:(r1,r2:R) ``r1 < r2`` -> ``-r1 > -r2``. -Unfold Rgt; Auto with real. -Qed. -Hints Resolve Rlt_Ropp : real. - -Lemma Ropp_Rlt: (x,y:R) ``-y < -x`` ->``x<y``. -Intros x y H'. -Rewrite <- (Ropp_Ropp x); Rewrite <- (Ropp_Ropp y); Auto with real. -Qed. -Hints Resolve Ropp_Rlt : real. - -Lemma Rlt_Ropp1:(r1,r2:R) ``r2 < r1`` -> ``-r1 < -r2``. -Auto with real. -Qed. -Hints Resolve Rlt_Ropp1 : real. - -(**********) -Lemma Rle_Ropp:(r1,r2:R) ``r1 <= r2`` -> ``-r1 >= -r2``. -Unfold Rge; Intros r1 r2 [H|H]; Auto with real. -Qed. -Hints Resolve Rle_Ropp : real. - -Lemma Ropp_Rle: (x,y:R) ``-y <= -x`` ->``x <= y``. -Intros x y H. -Elim H;Auto with real. -Intro H1;Rewrite <-(Ropp_Ropp x);Rewrite <-(Ropp_Ropp y);Rewrite H1; - Auto with real. -Qed. -Hints Resolve Ropp_Rle : real. - -Lemma Rle_Ropp1:(r1,r2:R) ``r2 <= r1`` -> ``-r1 <= -r2``. -Intros r1 r2 H;Elim H;Auto with real. -Intro H1;Rewrite H1;Auto with real. -Qed. -Hints Resolve Rle_Ropp1 : real. - -(**********) -Lemma Rge_Ropp:(r1,r2:R) ``r1 >= r2`` -> ``-r1 <= -r2``. -Unfold Rge; Intros r1 r2 [H|H]; Auto with real. -Qed. -Hints Resolve Rge_Ropp : real. - -(**********) -Lemma Rlt_RO_Ropp:(r:R) ``0 < r`` -> ``0 > -r``. -Intros; Replace ``0`` with ``-0``; Auto with real. -Qed. -Hints Resolve Rlt_RO_Ropp : real. - -(**********) -Lemma Rgt_RO_Ropp:(r:R) ``0 > r`` -> ``0 < -r``. -Intros; Replace ``0`` with ``-0``; Auto with real. -Qed. -Hints Resolve Rgt_RO_Ropp : real. - -(**********) -Lemma Rle_RO_Ropp:(r:R) ``0 <= r`` -> ``0 >= -r``. -Intros; Replace ``0`` with ``-0``; Auto with real. -Qed. -Hints Resolve Rle_RO_Ropp : real. - -(**********) -Lemma Rge_RO_Ropp:(r:R) ``0 >= r`` -> ``0 <= -r``. -Intros; Replace ``0`` with ``-0``; Auto with real. -Qed. -Hints Resolve Rge_RO_Ropp : real. - -(** Order and multiplication *) - -Lemma Rlt_monotony_r:(r,r1,r2:R)``0<r`` -> ``r1 < r2`` -> ``r1*r < r2*r``. -Intros; Rewrite (Rmult_sym r1 r); Rewrite (Rmult_sym r2 r); Auto with real. -Qed. -Hints Resolve Rlt_monotony_r. - -Lemma Rlt_monotony_contra: - (x, y, z:R) ``0<z`` ->``z*x<z*y`` ->``x<y``. -Intros x y z H H0. -Case (total_order x y); Intros Eq0; Auto; Elim Eq0; Clear Eq0; Intros Eq0. - Rewrite Eq0 in H0;ElimType False;Apply (Rlt_antirefl ``z*y``);Auto. -Generalize (Rlt_monotony z y x H Eq0);Intro;ElimType False; - Generalize (Rlt_trans ``z*x`` ``z*y`` ``z*x`` H0 H1);Intro; - Apply (Rlt_antirefl ``z*x``);Auto. -Qed. - -Lemma Rlt_anti_monotony:(r,r1,r2:R)``r < 0`` -> ``r1 < r2`` -> ``r*r1 > r*r2``. -Intros; Replace r with ``-(-r)``; Auto with real. -Rewrite (Ropp_mul1 ``-r``); Rewrite (Ropp_mul1 ``-r``). -Apply Rlt_Ropp; Auto with real. -Qed. - -(**********) -Lemma Rle_monotony: - (r,r1,r2:R)``0 <= r`` -> ``r1 <= r2`` -> ``r*r1 <= r*r2``. -Intros r r1 r2;Unfold Rle;Intros H H0;Elim H;Elim H0;Intros; Auto with real. -Right;Rewrite <- H2;Ring. -Qed. -Hints Resolve Rle_monotony : real. - -Lemma Rle_monotony_r: - (r,r1,r2:R)``0 <= r`` -> ``r1 <= r2`` -> ``r1*r <= r2*r``. -Intros r r1 r2 H; -Rewrite (Rmult_sym r1 r); Rewrite (Rmult_sym r2 r); Auto with real. -Qed. -Hints Resolve Rle_monotony_r : real. - -Lemma Rle_monotony_contra: - (x, y, z:R) ``0<z`` ->``z*x<=z*y`` ->``x<=y``. -Intros x y z H H0;Case H0; Auto with real. -Intros H1; Apply Rlt_le. -Apply Rlt_monotony_contra with z := z;Auto. -Intros H1;Replace x with (Rmult (Rinv z) (Rmult z x)); Auto with real. -Replace y with (Rmult (Rinv z) (Rmult z y)). - Rewrite H1;Auto with real. -Rewrite <- Rmult_assoc; Rewrite Rinv_l; Auto with real. -Rewrite <- Rmult_assoc; Rewrite Rinv_l; Auto with real. -Qed. - -Lemma Rle_anti_monotony - :(r,r1,r2:R)``r <= 0`` -> ``r1 <= r2`` -> ``r*r1 >= r*r2``. -Intros; Replace r with ``-(-r)``; Auto with real. -Rewrite (Ropp_mul1 ``-r``); Rewrite (Ropp_mul1 ``-r``). -Apply Rle_Ropp; Auto with real. -Qed. -Hints Resolve Rle_anti_monotony : real. - -Lemma Rle_Rmult_comp: - (x, y, z, t:R) ``0 <= x`` -> ``0 <= z`` -> ``x <= y`` -> ``z <= t`` -> - ``x*z <= y*t``. -Intros x y z t H' H'0 H'1 H'2. -Apply Rle_trans with r2 := ``x*t``; Auto with real. -Repeat Rewrite [x:?](Rmult_sym x t). -Apply Rle_monotony; Auto. -Apply Rle_trans with z; Auto. -Qed. -Hints Resolve Rle_Rmult_comp :real. - -Lemma Rmult_lt:(r1,r2,r3,r4:R)``r3>0`` -> ``r2>0`` -> - `` r1 < r2`` -> ``r3 < r4`` -> ``r1*r3 < r2*r4``. -Intros; Apply Rlt_trans with ``r2*r3``; Auto with real. -Qed. - -(** Order and Substractions *) -Lemma Rlt_minus:(r1,r2:R)``r1 < r2`` -> ``r1-r2 < 0``. -Intros; Apply (Rlt_anti_compatibility ``r2``). -Replace ``r2+(r1-r2)`` with r1. -Replace ``r2+0`` with r2; Auto with real. -Ring. -Qed. -Hints Resolve Rlt_minus : real. - -(**********) -Lemma Rle_minus:(r1,r2:R)``r1 <= r2`` -> ``r1-r2 <= 0``. -Unfold Rle; Intros; Elim H; Auto with real. -Qed. - -(**********) -Lemma Rminus_lt:(r1,r2:R)``r1-r2 < 0`` -> ``r1 < r2``. -Intros; Replace r1 with ``r1-r2+r2``. -Pattern 3 r2; Replace r2 with ``0+r2``; Auto with real. -Ring. -Qed. - -(**********) -Lemma Rminus_le:(r1,r2:R)``r1-r2 <= 0`` -> ``r1 <= r2``. -Intros; Replace r1 with ``r1-r2+r2``. -Pattern 3 r2; Replace r2 with ``0+r2``; Auto with real. -Ring. -Qed. - -(**********) -Lemma tech_Rplus:(r,s:R)``0<=r`` -> ``0<s`` -> ``r+s<>0``. -Intros; Apply sym_not_eqT; Apply Rlt_not_eq. -Rewrite Rplus_sym; Replace ``0`` with ``0+0``; Auto with real. -Qed. -Hints Immediate tech_Rplus : real. - -(** Order and the square function *) -Lemma pos_Rsqr:(r:R)``0<=(Rsqr r)``. -Intro; Case (total_order_Rlt_Rle r ``0``); Unfold Rsqr; Intro. -Replace ``r*r`` with ``(-r)*(-r)``; Auto with real. -Replace ``0`` with ``-r*0``; Auto with real. -Replace ``0`` with ``0*r``; Auto with real. -Qed. - -(***********) -Lemma pos_Rsqr1:(r:R)``r<>0``->``0<(Rsqr r)``. -Intros; Case (not_Req r ``0``); Trivial; Unfold Rsqr; Intro. -Replace ``r*r`` with ``(-r)*(-r)``; Auto with real. -Replace ``0`` with ``-r*0``; Auto with real. -Replace ``0`` with ``0*r``; Auto with real. -Qed. -Hints Resolve pos_Rsqr pos_Rsqr1 : real. - -(** Zero is less than one *) -Lemma Rlt_R0_R1:``0<1``. -Replace ``1`` with ``(Rsqr 1)``; Auto with real. -Unfold Rsqr; Auto with real. -Qed. -Hints Resolve Rlt_R0_R1 : real. - -(** Order and inverse *) -Lemma Rlt_Rinv:(r:R)``0<r``->``0</r``. -Intros; Change ``/r>0``; Apply not_Rle; Red; Intros. -Absurd ``1<=0``; Auto with real. -Replace ``1`` with ``r*(/r)``; Auto with real. -Replace ``0`` with ``r*0``; Auto with real. -Qed. -Hints Resolve Rlt_Rinv : real. - -(*********) -Lemma Rlt_Rinv2:(r:R)``r < 0``->``/r < 0``. -Intros; Change ``0>/r``; Apply not_Rle; Red; Intros. -Absurd ``1<=0``; Auto with real. -Replace ``1`` with ``r*(/r)``; Auto with real. -Replace ``0`` with ``r*0``; Auto with real. -Qed. -Hints Resolve Rlt_Rinv2 : real. - -(**********) -Lemma Rlt_monotony_rev: - (r,r1,r2:R)``0<r`` -> ``r*r1 < r*r2`` -> ``r1 < r2``. -Intros; Replace r1 with ``/r*(r*r1)``. -Replace r2 with ``/r*(r*r2)``; Auto with real. -Transitivity ``r*/r*r2``; Auto with real. -Ring. -Transitivity ``r*/r*r1``; Auto with real. -Ring. -Qed. - -(*********) -Lemma Rinv_lt:(r1,r2:R)``0 < r1*r2`` -> ``r1 < r2`` -> ``/r2 < /r1``. -Intros; Apply Rlt_monotony_rev with ``r1*r2``; Auto with real. -Case (without_div_O_contr r1 r2 ); Intros; Auto with real. -Replace ``r1*r2*/r2`` with r1. -Replace ``r1*r2*/r1`` with r2; Trivial. -Symmetry; Auto with real. -Symmetry; Auto with real. -Qed. - -Lemma Rlt_Rinv_R1: (x, y:R) ``1 <= x`` -> ``x<y`` ->``/y< /x``. -Intros x y H' H'0. -Cut (Rlt R0 x); [Intros Lt0 | Apply Rlt_le_trans with r2 := R1]; - Auto with real. -Apply Rlt_monotony_contra with z := x; Auto with real. -Rewrite (Rmult_sym x (Rinv x)); Rewrite Rinv_l; Auto with real. -Apply Rlt_monotony_contra with z := y; Auto with real. -Apply Rlt_trans with r2:=x;Auto. -Cut ``y*(x*/y)==x``. -Intro H1;Rewrite H1;Rewrite (Rmult_1r y);Auto. -Rewrite (Rmult_sym x); Rewrite <- Rmult_assoc; Rewrite (Rmult_sym y (Rinv y)); - Rewrite Rinv_l; Auto with real. -Apply imp_not_Req; Right. -Red; Apply Rlt_trans with r2 := x; Auto with real. -Qed. -Hints Resolve Rlt_Rinv_R1 :real. - -(*********************************************************) -(** Greater *) -(*********************************************************) - -(**********) -Lemma Rge_ge_eq:(r1,r2:R)``r1 >= r2`` -> ``r2 >= r1`` -> r1==r2. -Intros; Apply Rle_antisym; Auto with real. -Qed. - -(**********) -Lemma Rlt_not_ge:(r1,r2:R)~(``r1<r2``)->``r1>=r2``. -Intros; Unfold Rge; Elim (total_order r1 r2); Intro. -Absurd ``r1<r2``; Trivial. -Case H0; Auto. -Qed. - -(**********) -Lemma Rgt_not_le:(r1,r2:R)~(``r1>r2``)->``r1<=r2``. -Intros r1 r2 H; Apply Rge_le. -Exact (Rlt_not_ge r2 r1 H). -Qed. - -(**********) -Lemma Rgt_ge:(r1,r2:R)``r1>r2`` -> ``r1 >= r2``. -Red; Auto with real. -Qed. - -(**********) -Lemma Rlt_sym:(r1,r2:R)``r1<r2`` <-> ``r2>r1``. -Split; Unfold Rgt; Auto with real. -Qed. - -(**********) -Lemma Rle_sym1:(r1,r2:R)``r1<=r2``->``r2>=r1``. -Proof Rle_ge. - -(**********) -Lemma Rle_sym2:(r1,r2:R)``r2>=r1`` -> ``r1<=r2``. -Proof [r1,r2](Rge_le r2 r1). - -(**********) -Lemma Rle_sym:(r1,r2:R)``r1<=r2``<->``r2>=r1``. -Split; Auto with real. -Qed. - -(**********) -Lemma Rge_gt_trans:(r1,r2,r3:R)``r1>=r2``->``r2>r3``->``r1>r3``. -Unfold Rgt; Intros; Apply Rlt_le_trans with r2; Auto with real. -Qed. - -(**********) -Lemma Rgt_ge_trans:(r1,r2,r3:R)``r1>r2`` -> ``r2>=r3`` -> ``r1>r3``. -Unfold Rgt; Intros; Apply Rle_lt_trans with r2; Auto with real. -Qed. - -(**********) -Lemma Rgt_trans:(r1,r2,r3:R)``r1>r2`` -> ``r2>r3`` -> ``r1>r3``. -Unfold Rgt; Intros; Apply Rlt_trans with r2; Auto with real. -Qed. - -(**********) -Lemma Rge_trans:(r1,r2,r3:R)``r1>=r2`` -> ``r2>=r3`` -> ``r1>=r3``. -Intros; Apply Rle_ge. -Apply Rle_trans with r2; Auto with real. -Qed. - -(**********) -Lemma Rgt_RoppO:(r:R)``r>0``->``(-r)<0``. -Intros; Rewrite <- Ropp_O; Auto with real. -Qed. - -(**********) -Lemma Rlt_RoppO:(r:R)``r<0``->``-r>0``. -Intros; Rewrite <- Ropp_O; Auto with real. -Qed. -Hints Resolve Rgt_RoppO Rlt_RoppO: real. - -(**********) -Lemma Rlt_r_plus_R1:(r:R)``0<=r`` -> ``0<r+1``. -Intros. -Apply Rlt_le_trans with ``1``; Auto with real. -Pattern 1 ``1``; Replace ``1`` with ``0+1``; Auto with real. -Qed. -Hints Resolve Rlt_r_plus_R1: real. - -(**********) -Lemma Rlt_r_r_plus_R1:(r:R)``r<r+1``. -Intros. -Pattern 1 r; Replace r with ``r+0``; Auto with real. -Qed. -Hints Resolve Rlt_r_r_plus_R1: real. - -(**********) -Lemma tech_Rgt_minus:(r1,r2:R)``0<r2``->``r1>r1-r2``. -Red; Unfold Rminus; Intros. -Pattern 2 r1; Replace r1 with ``r1+0``; Auto with real. -Qed. - -(***********) -Lemma Rgt_plus_plus_r:(r,r1,r2:R)``r1>r2``->``r+r1 > r+r2``. -Unfold Rgt; Auto with real. -Qed. -Hints Resolve Rgt_plus_plus_r : real. - -(***********) -Lemma Rgt_r_plus_plus:(r,r1,r2:R)``r+r1 > r+r2`` -> ``r1 > r2``. -Unfold Rgt; Intros; Apply (Rlt_anti_compatibility r r2 r1 H). -Qed. - -(***********) -Lemma Rge_plus_plus_r:(r,r1,r2:R)``r1>=r2`` -> ``r+r1 >= r+r2``. -Intros; Apply Rle_ge; Auto with real. -Qed. -Hints Resolve Rge_plus_plus_r : real. - -(***********) -Lemma Rge_r_plus_plus:(r,r1,r2:R)``r+r1 >= r+r2`` -> ``r1>=r2``. -Intros; Apply Rle_ge; Apply Rle_anti_compatibility with r; Auto with real. -Qed. - -(***********) -Lemma Rge_monotony: - (x,y,z:R) ``z>=0`` -> ``x>=y`` -> ``x*z >= y*z``. -Intros; Apply Rle_ge; Auto with real. -Qed. - -(***********) -Lemma Rgt_minus:(r1,r2:R)``r1>r2`` -> ``r1-r2 > 0``. -Intros; Replace ``0`` with ``r2-r2``; Auto with real. -Unfold Rgt Rminus; Auto with real. -Qed. - -(*********) -Lemma minus_Rgt:(r1,r2:R)``r1-r2 > 0`` -> ``r1>r2``. -Intros; Replace r2 with ``r2+0``; Auto with real. -Intros; Replace r1 with ``r2+(r1-r2)``; Auto with real. -Qed. - -(**********) -Lemma Rge_minus:(r1,r2:R)``r1>=r2`` -> ``r1-r2 >= 0``. -Unfold Rge; Intros; Elim H; Intro. -Left; Apply (Rgt_minus r1 r2 H0). -Right; Apply (eq_Rminus r1 r2 H0). -Qed. - -(*********) -Lemma minus_Rge:(r1,r2:R)``r1-r2 >= 0`` -> ``r1>=r2``. -Intros; Replace r2 with ``r2+0``; Auto with real. -Intros; Replace r1 with ``r2+(r1-r2)``; Auto with real. -Qed. - - -(*********) -Lemma Rmult_gt:(r1,r2:R)``r1>0`` -> ``r2>0`` -> ``r1*r2>0``. -Unfold Rgt;Intros. -Replace ``0`` with ``0*r2``; Auto with real. -Qed. - -(*********) -Lemma Rmult_lt_0 - :(r1,r2,r3,r4:R)``r3>=0``->``r2>0``->``r1<r2``->``r3<r4``->``r1*r3<r2*r4``. -Intros; Apply Rle_lt_trans with ``r2*r3``; Auto with real. -Qed. - -(*********) -Lemma Rmult_lt_pos:(x,y:R)``0<x`` -> ``0<y`` -> ``0<x*y``. -Proof Rmult_gt. - -(***********) -Lemma Rplus_eq_R0_l:(a,b:R)``0<=a`` -> ``0<=b`` -> ``a+b==0`` -> ``a==0``. -Intros a b [H|H] H0 H1; Auto with real. -Absurd ``0<a+b``. -Rewrite H1; Auto with real. -Replace ``0`` with ``0+0``; Auto with real. -Qed. - - -Lemma Rplus_eq_R0 - :(a,b:R)``0<=a`` -> ``0<=b`` -> ``a+b==0`` -> ``a==0``/\``b==0``. -Split. -Apply Rplus_eq_R0_l with b; Auto with real. -Apply Rplus_eq_R0_l with a; Auto with real. -Rewrite Rplus_sym; Auto with real. -Qed. - - -(***********) -Lemma Rplus_Rsr_eq_R0_l:(a,b:R)``(Rsqr a)+(Rsqr b)==0``->``a==0``. -Intros; Apply Rsqr_r_R0; Apply Rplus_eq_R0_l with (Rsqr b); Auto with real. -Qed. - -Lemma Rplus_Rsr_eq_R0:(a,b:R)``(Rsqr a)+(Rsqr b)==0``->``a==0``/\``b==0``. -Split. -Apply Rplus_Rsr_eq_R0_l with b; Auto with real. -Apply Rplus_Rsr_eq_R0_l with a; Auto with real. -Rewrite Rplus_sym; Auto with real. -Qed. - - -(**********************************************************) -(** Injection from [N] to [R] *) -(**********************************************************) - -(**********) -Lemma S_INR:(n:nat)(INR (S n))==``(INR n)+1``. -Intro; Case n; Auto with real. -Qed. - -(**********) -Lemma S_O_plus_INR:(n:nat) - (INR (plus (S O) n))==``(INR (S O))+(INR n)``. -Intro; Simpl; Case n; Intros; Auto with real. -Qed. - -(**********) -Lemma plus_INR:(n,m:nat)(INR (plus n m))==``(INR n)+(INR m)``. -Intros n m; Induction n. -Simpl; Auto with real. -Replace (plus (S n) m) with (S (plus n m)); Auto with arith. -Repeat Rewrite S_INR. -Rewrite Hrecn; Ring. -Qed. - -(**********) -Lemma minus_INR:(n,m:nat)(le m n)->(INR (minus n m))==``(INR n)-(INR m)``. -Intros n m le; Pattern m n; Apply le_elim_rel; Auto with real. -Intros; Rewrite <- minus_n_O; Auto with real. -Intros; Repeat Rewrite S_INR; Simpl. -Rewrite H0; Ring. -Qed. - -(*********) -Lemma mult_INR:(n,m:nat)(INR (mult n m))==(Rmult (INR n) (INR m)). -Intros n m; Induction n. -Simpl; Auto with real. -Intros; Repeat Rewrite S_INR; Simpl. -Rewrite plus_INR; Rewrite Hrecn; Ring. -Qed. - -Hints Resolve plus_INR minus_INR mult_INR : real. - -(*********) -Lemma lt_INR_0:(n:nat)(lt O n)->``0 < (INR n)``. -Induction 1; Intros; Auto with real. -Rewrite S_INR; Auto with real. -Qed. -Hints Resolve lt_INR_0: real. - -Lemma lt_INR:(n,m:nat)(lt n m)->``(INR n) < (INR m)``. -Induction 1; Intros; Auto with real. -Rewrite S_INR; Auto with real. -Rewrite S_INR; Apply Rlt_trans with (INR m0); Auto with real. -Qed. -Hints Resolve lt_INR: real. - -Lemma INR_lt_1:(n:nat)(lt (S O) n)->``1 < (INR n)``. -Intros;Replace ``1`` with (INR (S O));Auto with real. -Qed. -Hints Resolve INR_lt_1: real. - -(**********) -Lemma INR_pos : (p:positive)``0<(INR (convert p))``. -Intro; Apply lt_INR_0. -Simpl; Auto with real. -Apply compare_convert_O. -Qed. -Hints Resolve INR_pos : real. - -(**********) -Lemma pos_INR:(n:nat)``0 <= (INR n)``. -Intro n; Case n. -Simpl; Auto with real. -Auto with arith real. -Qed. -Hints Resolve pos_INR: real. - -Lemma INR_lt:(n,m:nat)``(INR n) < (INR m)``->(lt n m). -Double Induction n m;Intros. -Simpl;ElimType False;Apply (Rlt_antirefl R0);Auto. -Auto with arith. -Generalize (pos_INR (S n0));Intro;Cut (INR O)==R0; - [Intro H2;Rewrite H2 in H0;Idtac|Simpl;Trivial]. -Generalize (Rle_lt_trans ``0`` (INR (S n0)) ``0`` H1 H0);Intro; - ElimType False;Apply (Rlt_antirefl R0);Auto. -Do 2 Rewrite S_INR in H1;Cut ``(INR n1) < (INR n0)``. -Intro H2;Generalize (H0 n0 H2);Intro;Auto with arith. -Apply (Rlt_anti_compatibility ``1`` (INR n1) (INR n0)). -Rewrite Rplus_sym;Rewrite (Rplus_sym ``1`` (INR n0));Trivial. -Qed. -Hints Resolve INR_lt: real. - -(*********) -Lemma le_INR:(n,m:nat)(le n m)->``(INR n)<=(INR m)``. -Induction 1; Intros; Auto with real. -Rewrite S_INR. -Apply Rle_trans with (INR m0); Auto with real. -Qed. -Hints Resolve le_INR: real. - -(**********) -Lemma not_INR_O:(n:nat)``(INR n)<>0``->~n=O. -Red; Intros n H H1. -Apply H. -Rewrite H1; Trivial. -Qed. -Hints Immediate not_INR_O : real. - -(**********) -Lemma not_O_INR:(n:nat)~n=O->``(INR n)<>0``. -Intro n; Case n. -Intro; Absurd (0)=(0); Trivial. -Intros; Rewrite S_INR. -Apply Rgt_not_eq; Red; Auto with real. -Qed. -Hints Resolve not_O_INR : real. - -Lemma not_nm_INR:(n,m:nat)~n=m->``(INR n)<>(INR m)``. -Intros n m H; Case (le_or_lt n m); Intros H1. -Case (le_lt_or_eq ? ? H1); Intros H2. -Apply imp_not_Req; Auto with real. -ElimType False;Auto. -Apply sym_not_eqT; Apply imp_not_Req; Auto with real. -Qed. -Hints Resolve not_nm_INR : real. - -Lemma INR_eq: (n,m:nat)(INR n)==(INR m)->n=m. -Intros;Case (le_or_lt n m); Intros H1. -Case (le_lt_or_eq ? ? H1); Intros H2;Auto. -Cut ~n=m. -Intro H3;Generalize (not_nm_INR n m H3);Intro H4; - ElimType False;Auto. -Omega. -Symmetry;Cut ~m=n. -Intro H3;Generalize (not_nm_INR m n H3);Intro H4; - ElimType False;Auto. -Omega. -Qed. -Hints Resolve INR_eq : real. - -Lemma INR_le: (n, m : nat) (Rle (INR n) (INR m)) -> (le n m). -Intros;Elim H;Intro. -Generalize (INR_lt n m H0);Intro;Auto with arith. -Generalize (INR_eq n m H0);Intro;Rewrite H1;Auto. -Qed. -Hints Resolve INR_le : real. - -Lemma not_1_INR:(n:nat)~n=(S O)->``(INR n)<>1``. -Replace ``1`` with (INR (S O)); Auto with real. -Qed. -Hints Resolve not_1_INR : real. - -(**********************************************************) -(** Injection from [Z] to [R] *) -(**********************************************************) - -(**********) -Definition INZ:=inject_nat. - -(**********) -Lemma IZN:(z:Z)(`0<=z`)->(Ex [n:nat] z=(INZ n)). -Unfold INZ;Intros;Apply inject_nat_complete;Assumption. -Qed. - -(**********) -Lemma INR_IZR_INZ:(n:nat)(INR n)==(IZR (INZ n)). -Induction n; Auto with real. -Intros; Simpl; Rewrite bij1; Auto with real. -Qed. - -Lemma plus_IZR_NEG_POS : - (p,q:positive)(IZR `(POS p)+(NEG q)`)==``(IZR (POS p))+(IZR (NEG q))``. -Intros. -Case (lt_eq_lt_dec (convert p) (convert q)). -Intros [H | H]; Simpl. -Rewrite convert_compare_INFERIEUR; Simpl; Trivial. -Rewrite (true_sub_convert q p). -Rewrite minus_INR; Auto with arith; Ring. -Apply ZC2; Apply convert_compare_INFERIEUR; Trivial. -Rewrite (convert_intro p q); Trivial. -Rewrite convert_compare_EGAL; Simpl; Auto with real. -Intro H; Simpl. -Rewrite convert_compare_SUPERIEUR; Simpl; Auto with arith. -Rewrite (true_sub_convert p q). -Rewrite minus_INR; Auto with arith; Ring. -Apply ZC2; Apply convert_compare_INFERIEUR; Trivial. -Qed. - -(**********) -Lemma plus_IZR:(z,t:Z)(IZR `z+t`)==``(IZR z)+(IZR t)``. -NewDestruct z; NewDestruct t; Intros; Auto with real. -Simpl; Intros; Rewrite convert_add; Auto with real. -Apply plus_IZR_NEG_POS. -Rewrite Zplus_sym; Rewrite Rplus_sym; Apply plus_IZR_NEG_POS. -Simpl; Intros; Rewrite convert_add; Rewrite plus_INR; Auto with real. -Qed. - -(**********) -Lemma mult_IZR:(z,t:Z)(IZR `z*t`)==``(IZR z)*(IZR t)``. -Intros z t; Case z; Case t; Simpl; Auto with real. -Intros t1 z1; Rewrite times_convert; Auto with real. -Intros t1 z1; Rewrite times_convert; Auto with real. -Rewrite Rmult_sym. -Rewrite Ropp_mul1; Auto with real. -Apply eq_Ropp; Rewrite mult_sym; Auto with real. -Intros t1 z1; Rewrite times_convert; Auto with real. -Rewrite Ropp_mul1; Auto with real. -Intros t1 z1; Rewrite times_convert; Auto with real. -Rewrite Ropp_mul2; Auto with real. -Qed. - -(**********) -Lemma Ropp_Ropp_IZR:(z:Z)(IZR (`-z`))==``-(IZR z)``. -Intro z; Case z; Simpl; Auto with real. -Qed. - -(**********) -Lemma Z_R_minus:(z1,z2:Z)``(IZR z1)-(IZR z2)``==(IZR `z1-z2`). -Intros; Unfold Rminus; Unfold Zminus. -Rewrite <-(Ropp_Ropp_IZR z2); Symmetry; Apply plus_IZR. -Qed. - -(**********) -Lemma lt_O_IZR:(z:Z)``0 < (IZR z)``->`0<z`. -Intro z; Case z; Simpl; Intros. -Absurd ``0<0``; Auto with real. -Unfold Zlt; Simpl; Trivial. -Case Rlt_le_not with 1:=H. -Replace ``0`` with ``-0``; Auto with real. -Qed. - -(**********) -Lemma lt_IZR:(z1,z2:Z)``(IZR z1)<(IZR z2)``->`z1<z2`. -Intros; Apply Zlt_O_minus_lt. -Apply lt_O_IZR. -Rewrite <- Z_R_minus. -Exact (Rgt_minus (IZR z2) (IZR z1) H). -Qed. - -(**********) -Lemma eq_IZR_R0:(z:Z)``(IZR z)==0``->`z=0`. -NewDestruct z; Simpl; Intros; Auto with zarith. -Case (Rlt_not_eq ``0`` (INR (convert p))); Auto with real. -Case (Rlt_not_eq ``-(INR (convert p))`` ``0`` ); Auto with real. -Qed. - -(**********) -Lemma eq_IZR:(z1,z2:Z)(IZR z1)==(IZR z2)->z1=z2. -Intros;Generalize (eq_Rminus (IZR z1) (IZR z2) H); - Rewrite (Z_R_minus z1 z2);Intro;Generalize (eq_IZR_R0 `z1-z2` H0); - Intro;Omega. -Qed. - -(**********) -Lemma not_O_IZR:(z:Z)`z<>0`->``(IZR z)<>0``. -Intros z H; Red; Intros H0; Case H. -Apply eq_IZR; Auto. -Qed. - -(*********) -Lemma le_O_IZR:(z:Z)``0<= (IZR z)``->`0<=z`. -Unfold Rle; Intros z [H|H]. -Red;Intro;Apply (Zlt_le_weak `0` z (lt_O_IZR z H)); Assumption. -Rewrite (eq_IZR_R0 z); Auto with zarith real. -Qed. - -(**********) -Lemma le_IZR:(z1,z2:Z)``(IZR z1)<=(IZR z2)``->`z1<=z2`. -Unfold Rle; Intros z1 z2 [H|H]. -Apply (Zlt_le_weak z1 z2); Auto with real. -Apply lt_IZR; Trivial. -Rewrite (eq_IZR z1 z2); Auto with zarith real. -Qed. - -(**********) -Lemma le_IZR_R1:(z:Z)``(IZR z)<=1``-> `z<=1`. -Pattern 1 ``1``; Replace ``1`` with (IZR `1`); Intros; Auto. -Apply le_IZR; Trivial. -Qed. - -(**********) -Lemma IZR_ge: (m,n:Z) `m>= n` -> ``(IZR m)>=(IZR n)``. -Intros;Apply Rlt_not_ge;Red;Intro. -Generalize (lt_IZR m n H0); Intro; Omega. -Qed. - -Lemma IZR_le: (m,n:Z) `m<= n` -> ``(IZR m)<=(IZR n)``. -Intros;Apply Rgt_not_le;Red;Intro. -Unfold Rgt in H0;Generalize (lt_IZR n m H0); Intro; Omega. -Qed. - -Lemma IZR_lt: (m,n:Z) `m< n` -> ``(IZR m)<(IZR n)``. -Intros;Cut `m<=n`. -Intro H0;Elim (IZR_le m n H0);Intro;Auto. -Generalize (eq_IZR m n H1);Intro;ElimType False;Omega. -Omega. -Qed. - -Lemma one_IZR_lt1 : (z:Z)``-1<(IZR z)<1``->`z=0`. -Intros z (H1,H2). -Apply Zle_antisym. -Apply Zlt_n_Sm_le; Apply lt_IZR; Trivial. -Replace `0` with (Zs `-1`); Trivial. -Apply Zlt_le_S; Apply lt_IZR; Trivial. -Qed. - -Lemma one_IZR_r_R1 - : (r:R)(z,x:Z)``r<(IZR z)<=r+1``->``r<(IZR x)<=r+1``->z=x. -Intros r z x (H1,H2) (H3,H4). -Cut `z-x=0`; Auto with zarith. -Apply one_IZR_lt1. -Rewrite <- Z_R_minus; Split. -Replace ``-1`` with ``r-(r+1)``. -Unfold Rminus; Apply Rplus_lt_le_lt; Auto with real. -Ring. -Replace ``1`` with ``(r+1)-r``. -Unfold Rminus; Apply Rplus_le_lt_lt; Auto with real. -Ring. -Qed. - - -(**********) -Lemma single_z_r_R1: - (r:R)(z,x:Z)``r<(IZR z)``->``(IZR z)<=r+1``->``r<(IZR x)``-> - ``(IZR x)<=r+1``->z=x. -Intros; Apply one_IZR_r_R1 with r; Auto. -Qed. - -(**********) -Lemma tech_single_z_r_R1 - :(r:R)(z:Z)``r<(IZR z)``->``(IZR z)<=r+1`` - -> (Ex [s:Z] (~s=z/\``r<(IZR s)``/\``(IZR s)<=r+1``))->False. -Intros r z H1 H2 (s, (H3,(H4,H5))). -Apply H3; Apply single_z_r_R1 with r; Trivial. -Qed. - -(*****************************************************************) -(** Definitions of new types *) -(*****************************************************************) - -Record nonnegreal : Type := mknonnegreal { -nonneg :> R; -cond_nonneg : ``0<=nonneg`` }. - -Record posreal : Type := mkposreal { -pos :> R; -cond_pos : ``0<pos`` }. - -Record nonposreal : Type := mknonposreal { -nonpos :> R; -cond_nonpos : ``nonpos<=0`` }. - -Record negreal : Type := mknegreal { -neg :> R; -cond_neg : ``neg<0`` }. - -Record nonzeroreal : Type := mknonzeroreal { -nonzero :> R; -cond_nonzero : ~``nonzero==0`` }. - -(**********) -Lemma prod_neq_R0 : (x,y:R) ~``x==0``->~``y==0``->~``x*y==0``. -Intros; Red; Intro; Generalize (without_div_Od x y H1); Intro; Elim H2; Intro; [Rewrite H3 in H; Elim H | Rewrite H3 in H0; Elim H0]; Reflexivity. -Qed. - -(*********) -Lemma Rmult_le_pos : (x,y:R) ``0<=x`` -> ``0<=y`` -> ``0<=x*y``. -Intros; Rewrite <- (Rmult_Ol x); Rewrite <- (Rmult_sym x); Apply (Rle_monotony x R0 y H H0). -Qed. - -Lemma double : (x:R) ``2*x==x+x``. -Intro; Ring. -Qed. - -Lemma double_var : (x:R) ``x == x/2 + x/2``. -Intro; Rewrite <- double; Unfold Rdiv; Rewrite <- Rmult_assoc; Symmetry; Apply Rinv_r_simpl_m. -Replace ``2`` with (INR (2)); [Apply not_O_INR; Discriminate | Unfold INR; Ring]. -Qed. - -(**********************************************************) -(** Other rules about < and <= *) -(**********************************************************) - -Lemma gt0_plus_gt0_is_gt0 : (x,y:R) ``0<x`` -> ``0<y`` -> ``0<x+y``. -Intros; Apply Rlt_trans with x; [Assumption | Pattern 1 x; Rewrite <- (Rplus_Or x); Apply Rlt_compatibility; Assumption]. -Qed. - -Lemma ge0_plus_gt0_is_gt0 : (x,y:R) ``0<=x`` -> ``0<y`` -> ``0<x+y``. -Intros; Apply Rle_lt_trans with x; [Assumption | Pattern 1 x; Rewrite <- (Rplus_Or x); Apply Rlt_compatibility; Assumption]. -Qed. - -Lemma gt0_plus_ge0_is_gt0 : (x,y:R) ``0<x`` -> ``0<=y`` -> ``0<x+y``. -Intros; Rewrite <- Rplus_sym; Apply ge0_plus_gt0_is_gt0; Assumption. -Qed. - -Lemma ge0_plus_ge0_is_ge0 : (x,y:R) ``0<=x`` -> ``0<=y`` -> ``0<=x+y``. -Intros; Apply Rle_trans with x; [Assumption | Pattern 1 x; Rewrite <- (Rplus_Or x); Apply Rle_compatibility; Assumption]. -Qed. - -Lemma plus_le_is_le : (x,y,z:R) ``0<=y`` -> ``x+y<=z`` -> ``x<=z``. -Intros; Apply Rle_trans with ``x+y``; [Pattern 1 x; Rewrite <- (Rplus_Or x); Apply Rle_compatibility; Assumption | Assumption]. -Qed. - -Lemma plus_lt_is_lt : (x,y,z:R) ``0<=y`` -> ``x+y<z`` -> ``x<z``. -Intros; Apply Rle_lt_trans with ``x+y``; [Pattern 1 x; Rewrite <- (Rplus_Or x); Apply Rle_compatibility; Assumption | Assumption]. -Qed. - -Lemma Rmult_lt2 : (r1,r2,r3,r4:R) ``0<=r1`` -> ``0<=r3`` -> ``r1<r2`` -> ``r3<r4`` -> ``r1*r3<r2*r4``. -Intros; Apply Rle_lt_trans with ``r2*r3``; [Apply Rle_monotony_r; [Assumption | Left; Assumption] | Apply Rlt_monotony; [Apply Rle_lt_trans with r1; Assumption | Assumption]]. -Qed. - -Lemma le_epsilon : (x,y:R) ((eps : R) ``0<eps``->``x<=y+eps``) -> ``x<=y``. -Intros; Elim (total_order x y); Intro. -Left; Assumption. -Elim H0; Intro. -Right; Assumption. -Clear H0; Generalize (Rgt_minus x y H1); Intro H2; Change ``0<x-y`` in H2. -Cut ``0<2``. -Intro. -Generalize (Rmult_lt_pos ``x-y`` ``/2`` H2 (Rlt_Rinv ``2`` H0)); Intro H3; Generalize (H ``(x-y)*/2`` H3); Replace ``y+(x-y)*/2`` with ``(y+x)*/2``. -Intro H4; Generalize (Rle_monotony ``2`` x ``(y+x)*/2`` (Rlt_le ``0`` ``2`` H0) H4); Rewrite <- (Rmult_sym ``((y+x)*/2)``); Rewrite Rmult_assoc; Rewrite <- Rinv_l_sym. -Rewrite Rmult_1r; Replace ``2*x`` with ``x+x``. -Rewrite (Rplus_sym y); Intro H5; Apply Rle_anti_compatibility with x; Assumption. -Ring. -Replace ``2`` with (INR (S (S O))); [Apply not_O_INR; Discriminate | Ring]. -Pattern 2 y; Replace y with ``y/2+y/2``. -Unfold Rminus Rdiv. -Repeat Rewrite Rmult_Rplus_distrl. -Ring. -Cut (z:R) ``2*z == z + z``. -Intro. -Rewrite <- (H4 ``y/2``). -Unfold Rdiv. -Rewrite <- Rmult_assoc; Apply Rinv_r_simpl_m. -Replace ``2`` with (INR (2)). -Apply not_O_INR. -Discriminate. -Unfold INR; Reflexivity. -Intro; Ring. -Cut ~(O=(2)); [Intro H0; Generalize (lt_INR_0 (2) (neq_O_lt (2) H0)); Unfold INR; Intro; Assumption | Discriminate]. -Qed. - -(*****************************************************) -(** Complementary results about [INR] *) -(*****************************************************) - -Fixpoint INR2 [n:nat] : R := Cases n of -O => ``0`` -| (S n0) => Cases n0 of -O => ``1`` -| (S _) => ``1+(INR2 n0)`` -end -end. - -Theorem INR_eq_INR2 : (n:nat) (INR n)==(INR2 n). -Induction n; [Unfold INR INR2; Reflexivity | Intros; Unfold INR INR2; Fold INR INR2; Rewrite H; Case n0; [Reflexivity | Intros; Ring]]. -Qed. - -Lemma add_auto : (p,q:nat) ``(INR2 (S p))+(INR2 q)==(INR2 p)+(INR2 (S q))``. -Intros; Repeat Rewrite <- INR_eq_INR2; Repeat Rewrite S_INR; Ring. -Qed. - -(**********) -Lemma complet_weak : (E:R->Prop) (bound E) -> (ExT [x:R] (E x)) -> (ExT [m:R] (is_lub E m)). -Intros; Elim (complet E H H0); Intros; Split with x; Assumption. -Qed.
\ No newline at end of file +Require Export RIneq. +Require Export DiscrR. diff --git a/theories/Reals/Rbasic_fun.v b/theories/Reals/Rbasic_fun.v index e940ec92b5..0fb879095d 100644 --- a/theories/Reals/Rbasic_fun.v +++ b/theories/Reals/Rbasic_fun.v @@ -13,7 +13,7 @@ (* *) (*********************************************************) -Require RealsB. +Require Rbase. Require R_Ifp. Require Fourier. diff --git a/theories/Reals/Rcomplet.v b/theories/Reals/Rcomplet.v index 195da5c08e..80516e3075 100644 --- a/theories/Reals/Rcomplet.v +++ b/theories/Reals/Rcomplet.v @@ -8,7 +8,7 @@ (*i $Id$ i*) -Require RealsB. +Require Rbase. Require Rfunctions. Require Rseries. Require SeqProp. @@ -169,4 +169,4 @@ Unfold Rdiv; Apply Rmult_lt_pos. Assumption. Apply Rlt_Rinv. Sup0; Try Apply lt_O_Sn. -Qed.
\ No newline at end of file +Qed. diff --git a/theories/Reals/Rderiv.v b/theories/Reals/Rderiv.v index be9cba0a04..234fb3760e 100644 --- a/theories/Reals/Rderiv.v +++ b/theories/Reals/Rderiv.v @@ -13,7 +13,7 @@ (* *) (*********************************************************) -Require RealsB. +Require Rbase. Require Rfunctions. Require Rlimit. Require Fourier. diff --git a/theories/Reals/Reals.v b/theories/Reals/Reals.v index 351374f36e..9bce35b28f 100644 --- a/theories/Reals/Reals.v +++ b/theories/Reals/Reals.v @@ -8,9 +8,9 @@ (*i $Id$ i*) -Require Export RealsB. +Require Export Rbase. Require Export Rfunctions. Require Export SeqSeries. Require Export Rtrigo. Require Export Ranalysis. -Require Export Integration.
\ No newline at end of file +Require Export Integration. diff --git a/theories/Reals/RealsB.v b/theories/Reals/RealsB.v deleted file mode 100644 index 29daec98d3..0000000000 --- a/theories/Reals/RealsB.v +++ /dev/null @@ -1,15 +0,0 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) -(* \VV/ *************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(***********************************************************************) - -(*i $Id$ i*) - -Require Export Rdefinitions. -Require Export TypeSyntax. -Require Export Raxioms. -Require Export Rbase. -Require Export DiscrR. diff --git a/theories/Reals/Rfunctions.v b/theories/Reals/Rfunctions.v index 1574954506..6b25fdcc15 100644 --- a/theories/Reals/Rfunctions.v +++ b/theories/Reals/Rfunctions.v @@ -16,7 +16,7 @@ (* *) (********************************************************) -Require RealsB. +Require Rbase. Require Export R_Ifp. Require Export Rbasic_fun. Require Export R_sqr. @@ -787,4 +787,4 @@ Qed. (*********) Definition infinit_sum:(nat->R)->R->Prop:=[s:nat->R;l:R] (eps:R)(Rgt eps R0)-> - (Ex[N:nat](n:nat)(ge n N)->(Rlt (R_dist (sum_f_R0 s n) l) eps)).
\ No newline at end of file + (Ex[N:nat](n:nat)(ge n N)->(Rlt (R_dist (sum_f_R0 s n) l) eps)). diff --git a/theories/Reals/Rgeom.v b/theories/Reals/Rgeom.v index 54c8725ed8..9588df9d3e 100644 --- a/theories/Reals/Rgeom.v +++ b/theories/Reals/Rgeom.v @@ -8,7 +8,7 @@ (*i $Id$ i*) -Require RealsB. +Require Rbase. Require Rfunctions. Require SeqSeries. Require Rtrigo. diff --git a/theories/Reals/RiemannInt.v b/theories/Reals/RiemannInt.v index fed86e6ef4..9dbd9cbc36 100644 --- a/theories/Reals/RiemannInt.v +++ b/theories/Reals/RiemannInt.v @@ -11,7 +11,7 @@ Require Rfunctions. Require SeqSeries. Require Ranalysis. -Require RealsB. +Require Rbase. Require RiemannInt_SF. Require Classical_Prop. Require Classical_Pred_Type. @@ -1697,4 +1697,4 @@ Qed. Lemma FTC_Riemann : (f:C1_fun;a,b:R;pr:(Riemann_integrable (derive f (diff0 f)) a b)) (RiemannInt pr)==``(f b)-(f a)``. Intros; Case (total_order_Rle a b); Intro; [Apply RiemannInt_P33; Assumption | Assert H : ``b<=a``; [Auto with real | Assert H0 := (RiemannInt_P1 pr); Rewrite (RiemannInt_P8 pr H0); Rewrite (RiemannInt_P33 H0 H); Ring]]. -Qed.
\ No newline at end of file +Qed. diff --git a/theories/Reals/RiemannInt_SF.v b/theories/Reals/RiemannInt_SF.v index e065119c6a..fd75ae4d84 100644 --- a/theories/Reals/RiemannInt_SF.v +++ b/theories/Reals/RiemannInt_SF.v @@ -8,7 +8,7 @@ (*i $Id$ i*) -Require RealsB. +Require Rbase. Require Rfunctions. Require Ranalysis. Require Classical_Prop. diff --git a/theories/Reals/Rlimit.v b/theories/Reals/Rlimit.v index 26b9da460d..ffad4fd8df 100644 --- a/theories/Reals/Rlimit.v +++ b/theories/Reals/Rlimit.v @@ -13,7 +13,7 @@ (* *) (*********************************************************) -Require RealsB. +Require Rbase. Require Rfunctions. Require Classical_Prop. Require Fourier. diff --git a/theories/Reals/Rpower.v b/theories/Reals/Rpower.v index 8075256018..c52c98289a 100644 --- a/theories/Reals/Rpower.v +++ b/theories/Reals/Rpower.v @@ -14,7 +14,7 @@ (* Propriétés *) (************************************************************) -Require RealsB. +Require Rbase. Require Rfunctions. Require SeqSeries. Require Rtrigo. @@ -153,7 +153,7 @@ Apply Rinv_neq_R0; Red; Intro; Rewrite H3 in H; Elim (Rlt_antirefl ? H). Qed. (* Définition du log népérien R+*>R *) -Definition Rln [y:posreal] : R := Cases (ln_exists (pos y) (Rbase.cond_pos y)) of (existTT a b) => a end. +Definition Rln [y:posreal] : R := Cases (ln_exists (pos y) (RIneq.cond_pos y)) of (existTT a b) => a end. (* Une extension sur R *) Definition ln : R->R := [x:R](Cases (total_order_Rlt R0 x) of @@ -162,7 +162,7 @@ Definition ln : R->R := [x:R](Cases (total_order_Rlt R0 x) of Lemma exp_ln : (x : R) ``0<x`` -> (exp (ln x)) == x. Intros; Unfold ln; Case (total_order_Rlt R0 x); Intro. -Unfold Rln; Case (ln_exists (mkposreal x r) (Rbase.cond_pos (mkposreal x r))); Intros. +Unfold Rln; Case (ln_exists (mkposreal x r) (RIneq.cond_pos (mkposreal x r))); Intros. Simpl in e; Symmetry; Apply e. Elim n; Apply H. Qed. @@ -474,7 +474,7 @@ Red; Intros H3; Case H2; Apply ln_inv; Auto. Apply limit_comp with l := (ln y) g := [x : R] (Rdiv (Rminus (exp x) (exp (ln y))) (Rminus x (ln y))) f := ln. Apply ln_continue; Auto. Assert H0 := (derivable_pt_lim_exp (ln y)); Unfold derivable_pt_lim in H0; Unfold limit1_in; Unfold limit_in; Simpl; Unfold R_dist; Intros; Elim (H0 ? H); Intros; Exists (pos x); Split. -Apply (Rbase.cond_pos x). +Apply (RIneq.cond_pos x). Intros; Pattern 3 y; Rewrite <- exp_ln. Pattern 1 x0; Replace x0 with ``(ln y)+(x0-(ln y))``; [Idtac | Ring]. Apply H1. @@ -555,4 +555,4 @@ Apply derivable_pt_lim_const with a := y. Apply derivable_pt_lim_id. Ring. Apply derivable_pt_lim_exp. -Qed.
\ No newline at end of file +Qed. diff --git a/theories/Reals/Rprod.v b/theories/Reals/Rprod.v index 936a501981..5a74e40258 100644 --- a/theories/Reals/Rprod.v +++ b/theories/Reals/Rprod.v @@ -9,7 +9,7 @@ (*i $Id$ i*) Require Compare. -Require RealsB. +Require Rbase. Require Rfunctions. Require Rseries. Require PartSum. @@ -159,4 +159,4 @@ Reflexivity. Rewrite mult_INR; Apply prod_neq_R0; Apply INR_fact_neq_0. Apply prod_neq_R0; Apply INR_fact_neq_0. Apply INR_eq; Rewrite minus_INR; [Rewrite mult_INR; Do 2 Rewrite S_INR; Ring | Apply le_n_2n]. -Qed.
\ No newline at end of file +Qed. diff --git a/theories/Reals/Rseries.v b/theories/Reals/Rseries.v index 7cc969afe8..4496582225 100644 --- a/theories/Reals/Rseries.v +++ b/theories/Reals/Rseries.v @@ -8,7 +8,7 @@ (*i $Id$ i*) -Require RealsB. +Require Rbase. Require Rfunctions. Require Classical. Require Compare. @@ -272,4 +272,4 @@ Assumption. Apply Rabsolu_pos_lt. Apply Rinv_neq_R0. Assumption. -Qed.
\ No newline at end of file +Qed. diff --git a/theories/Reals/Rsigma.v b/theories/Reals/Rsigma.v index 766365c135..4a5e35fbff 100644 --- a/theories/Reals/Rsigma.v +++ b/theories/Reals/Rsigma.v @@ -8,7 +8,7 @@ (*i $Id$ i*) -Require RealsB. +Require Rbase. Require Rfunctions. Require Rseries. Require PartSum. diff --git a/theories/Reals/Rsqrt_def.v b/theories/Reals/Rsqrt_def.v index d47374968e..8ee462aba1 100644 --- a/theories/Reals/Rsqrt_def.v +++ b/theories/Reals/Rsqrt_def.v @@ -9,7 +9,7 @@ (*i $Id$ i*) Require Sumbool. -Require RealsB. +Require Rbase. Require Rfunctions. Require SeqSeries. Require Ranalysis1. @@ -685,4 +685,4 @@ Apply Rsqr_inj. Assumption. Assumption. Rewrite <- H0; Rewrite <- H2; Reflexivity. -Qed.
\ No newline at end of file +Qed. diff --git a/theories/Reals/Rtopology.v b/theories/Reals/Rtopology.v index 9909df51bf..3e900089e3 100644 --- a/theories/Reals/Rtopology.v +++ b/theories/Reals/Rtopology.v @@ -8,7 +8,7 @@ (*i $Id$ i*) -Require RealsB. +Require Rbase. Require Rfunctions. Require Ranalysis1. Require RList. diff --git a/theories/Reals/Rtrigo.v b/theories/Reals/Rtrigo.v index 2219b1b041..f1763a6d2c 100644 --- a/theories/Reals/Rtrigo.v +++ b/theories/Reals/Rtrigo.v @@ -8,7 +8,7 @@ (*i $Id$ i*) -Require RealsB. +Require Rbase. Require Rfunctions. Require SeqSeries. Require Export Rtrigo_fun. @@ -1112,4 +1112,4 @@ Qed. Lemma cos_eq_0_2PI_1 : (x:R) ``0<=x`` -> ``x<=2*PI`` -> ``x==PI/2``\/``x==3*(PI/2)`` -> ``(cos x)==0``. Intros x H1 H2 H3; Elim H3; Intro H4; [ Rewrite H4; Rewrite -> cos_PI2; Reflexivity | Rewrite H4; Rewrite -> cos_3PI2; Reflexivity ]. -Qed.
\ No newline at end of file +Qed. diff --git a/theories/Reals/Rtrigo_alt.v b/theories/Reals/Rtrigo_alt.v index 13ea21aa79..c40cc4da33 100644 --- a/theories/Reals/Rtrigo_alt.v +++ b/theories/Reals/Rtrigo_alt.v @@ -8,7 +8,7 @@ (*i $Id$ i*) -Require RealsB. +Require Rbase. Require Rfunctions. Require SeqSeries. Require Rtrigo_def. @@ -292,4 +292,4 @@ Left; Assumption. Rewrite <- (Ropp_Ropp ``PI/2``); Apply Rle_Ropp1; Unfold Rdiv; Unfold Rdiv in H0; Rewrite <- Ropp_mul1; Exact H0. Intros; Unfold cos_approx; Apply sum_eq; Intros; Unfold cos_term; Do 2 Rewrite pow_Rsqr; Rewrite Rsqr_neg; Unfold Rdiv; Reflexivity. Apply Rgt_RO_Ropp; Assumption. -Qed.
\ No newline at end of file +Qed. diff --git a/theories/Reals/Rtrigo_calc.v b/theories/Reals/Rtrigo_calc.v index a0f7e01b26..0ecc9fbc55 100644 --- a/theories/Reals/Rtrigo_calc.v +++ b/theories/Reals/Rtrigo_calc.v @@ -8,7 +8,7 @@ (*i $Id$ i*) -Require RealsB. +Require Rbase. Require Rfunctions. Require SeqSeries. Require Rtrigo. @@ -529,4 +529,4 @@ Simpl; Discriminate. Simpl; Discriminate. Simpl; Discriminate. Elim (Rlt_antirefl ``0`` (Rle_lt_trans ``0`` a ``0`` H H2)). -Qed.
\ No newline at end of file +Qed. diff --git a/theories/Reals/Rtrigo_def.v b/theories/Reals/Rtrigo_def.v index 842b31b453..9d09f1a532 100644 --- a/theories/Reals/Rtrigo_def.v +++ b/theories/Reals/Rtrigo_def.v @@ -8,7 +8,7 @@ (*i $Id$ i*) -Require RealsB. +Require Rbase. Require Rfunctions. Require SeqSeries. Require Rtrigo_fun. @@ -355,4 +355,4 @@ Apply H0. Apply H. Exact (projT2 ? ? exist_cos0). Assert H := (projT2 ? ? (exist_cos (Rsqr R0))); Unfold cos; Pattern 1 R0; Replace R0 with (Rsqr R0); [Exact H | Apply Rsqr_O]. -Qed.
\ No newline at end of file +Qed. diff --git a/theories/Reals/Rtrigo_fun.v b/theories/Reals/Rtrigo_fun.v index 8e1d565e55..b0ccff5d23 100644 --- a/theories/Reals/Rtrigo_fun.v +++ b/theories/Reals/Rtrigo_fun.v @@ -8,7 +8,7 @@ (*i $Id$ i*) -Require RealsB. +Require Rbase. Require Rfunctions. Require SeqSeries. diff --git a/theories/Reals/Rtrigo_reg.v b/theories/Reals/Rtrigo_reg.v index 2fdf96d0c3..5a34dd7af4 100644 --- a/theories/Reals/Rtrigo_reg.v +++ b/theories/Reals/Rtrigo_reg.v @@ -8,7 +8,7 @@ (*i $Id$ i*) -Require RealsB. +Require Rbase. Require Rfunctions. Require SeqSeries. Require Rtrigo. @@ -491,4 +491,4 @@ Qed. Lemma derive_pt_cos : (x:R) ``(derive_pt cos x (derivable_pt_cos ?))==-(sin x)``. Intros; Apply derive_pt_eq_0. Apply derivable_pt_lim_cos. -Qed.
\ No newline at end of file +Qed. diff --git a/theories/Reals/SeqProp.v b/theories/Reals/SeqProp.v index eee110a9c8..6c9f709e5d 100644 --- a/theories/Reals/SeqProp.v +++ b/theories/Reals/SeqProp.v @@ -8,7 +8,7 @@ (*i $Id$ i*) -Require RealsB. +Require Rbase. Require Rfunctions. Require Rseries. Require Classical. @@ -1123,4 +1123,4 @@ Rewrite plus_INR. Pattern 1 (INR (fact n0)); Rewrite <- Rplus_Or. Apply Rle_compatibility. Apply pos_INR. -Qed.
\ No newline at end of file +Qed. diff --git a/theories/Reals/SeqSeries.v b/theories/Reals/SeqSeries.v index a32691dea3..407f1fa7c7 100644 --- a/theories/Reals/SeqSeries.v +++ b/theories/Reals/SeqSeries.v @@ -8,7 +8,7 @@ (*i $Id$ i*) -Require RealsB. +Require Rbase. Require Rfunctions. Require Export Rseries. Require Export SeqProp. @@ -199,4 +199,4 @@ Apply Rle_trans with (An (plus (S m) n0)); Assumption. Apply Rle_sym1. Apply cond_pos_sum; Intro. Elim (H (plus (S m) n0)); Intros; Assumption. -Qed.
\ No newline at end of file +Qed. diff --git a/theories/Reals/SplitRmult.v b/theories/Reals/SplitRmult.v index 779491bf49..e799c7b8be 100644 --- a/theories/Reals/SplitRmult.v +++ b/theories/Reals/SplitRmult.v @@ -11,7 +11,7 @@ (*i Lemma mult_non_zero :(r1,r2:R)``r1<>0`` /\ ``r2<>0`` -> ``r1*r2<>0``. i*) -Require RealsB. +Require Rbase. Tactic Definition SplitRmult := Match Context With diff --git a/theories/Reals/Sqrt_reg.v b/theories/Reals/Sqrt_reg.v index 05de0f1c6f..9cf2ac0030 100644 --- a/theories/Reals/Sqrt_reg.v +++ b/theories/Reals/Sqrt_reg.v @@ -8,7 +8,7 @@ (*i $Id$ i*) -Require RealsB. +Require Rbase. Require Rfunctions. Require Ranalysis1. Require R_sqrt. @@ -293,4 +293,4 @@ Apply sqrt_positivity; Apply Rle_sym2; Exact r. Left; Exact H2. Apply Rle_sym1; Apply sqrt_positivity; Apply Rle_sym2; Exact r. Elim (Rlt_antirefl ? (Rlt_le_trans ? ? ? H1 H)). -Qed.
\ No newline at end of file +Qed. diff --git a/theories/Reals/TAF.v b/theories/Reals/TAF.v index 2bcbf55d94..d797bb7d5d 100644 --- a/theories/Reals/TAF.v +++ b/theories/Reals/TAF.v @@ -8,7 +8,7 @@ (*i $Id$ i*) -Require RealsB. +Require Rbase. Require Rfunctions. Require Ranalysis1. Require Rtopology. @@ -515,4 +515,4 @@ Assert H9 : ``a<=x0<=b``. Split; Left; Assumption. Apply derivable_pt_lim_minus; [Elim (H ? H9) | Elim (H0 ? H9)]; Intros; EApply derive_pt_eq_1; Symmetry; Apply H10. Assert H8 := (null_derivative_loc (minus_fct g1 g2) a b H5 H6 H7); Unfold constant_D_eq in H8; Assert H9 := (H8 ? H2); Unfold minus_fct in H9; Rewrite <- H9; Ring. -Qed.
\ No newline at end of file +Qed. |