Extension of NArith: Nminus, Nmin, etc

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

10 files changed, 283 insertions, 168 deletions

diff --git a/.depend.coq b/.depend.coq
index ac1fadf50..05031eba1 100644
--- a/.depend.coq
+++ b/.depend.coq
@@ -21,7 +21,7 @@ theories/FSets/FMapWeakFacts.vo: theories/FSets/FMapWeakFacts.v theories/Bool/Bo
 theories/FSets/FMapWeakInterface.vo: theories/FSets/FMapWeakInterface.v theories/FSets/FSetInterface.vo theories/FSets/FSetWeakInterface.vo
 theories/FSets/FMapWeakList.vo: theories/FSets/FMapWeakList.v theories/FSets/FSetInterface.vo theories/FSets/FSetWeakInterface.vo theories/FSets/FMapWeakInterface.vo
 theories/FSets/FMapWeak.vo: theories/FSets/FMapWeak.v theories/Logic/DecidableType.vo theories/Logic/DecidableTypeEx.vo theories/FSets/FMapWeakInterface.vo theories/FSets/FMapWeakList.vo theories/FSets/FMapWeakFacts.vo
-theories/FSets/FMapPositive.vo: theories/FSets/FMapPositive.v theories/Bool/Bool.vo theories/ZArith/ZArith.vo theories/FSets/OrderedType.vo theories/FSets/FMapInterface.vo
+theories/FSets/FMapPositive.vo: theories/FSets/FMapPositive.v theories/Bool/Bool.vo theories/ZArith/ZArith.vo theories/FSets/OrderedType.vo theories/FSets/OrderedTypeEx.vo theories/FSets/FMapInterface.vo
 theories/FSets/FMapIntMap.vo: theories/FSets/FMapIntMap.v theories/Bool/Bool.vo theories/NArith/NArith.vo theories/NArith/Ndigits.vo theories/NArith/Ndec.vo theories/NArith/Nnat.vo theories/IntMap/Allmaps.vo theories/FSets/OrderedType.vo theories/FSets/OrderedTypeEx.vo theories/FSets/FMapInterface.vo theories/FSets/FMapList.vo
 theories/FSets/FSetToFiniteSet.vo: theories/FSets/FSetToFiniteSet.v theories/Sets/Ensembles.vo theories/Sets/Finite_sets.vo theories/FSets/FSetInterface.vo theories/FSets/FSetProperties.vo theories/FSets/OrderedTypeEx.vo
 theories/FSets/FMapAVL.vo: theories/FSets/FMapAVL.v theories/FSets/FSetInterface.vo theories/FSets/FMapInterface.vo theories/FSets/FMapList.vo theories/ZArith/ZArith.vo theories/ZArith/Int.vo
@@ -141,7 +141,7 @@ theories/Arith/Peano_dec.vo: theories/Arith/Peano_dec.v theories/Logic/Decidable
 theories/Arith/Euclid.vo: theories/Arith/Euclid.v theories/Arith/Mult.vo theories/Arith/Compare_dec.vo theories/Arith/Wf_nat.vo
 theories/Arith/Plus.vo: theories/Arith/Plus.v theories/Arith/Le.vo theories/Arith/Lt.vo
 theories/Arith/Wf_nat.vo: theories/Arith/Wf_nat.v theories/Arith/Lt.vo
-theories/Arith/Max.vo: theories/Arith/Max.v theories/Arith/Arith.vo
+theories/Arith/Max.vo: theories/Arith/Max.v theories/Arith/Le.vo
 theories/Arith/Bool_nat.vo: theories/Arith/Bool_nat.v theories/Arith/Compare_dec.vo theories/Arith/Peano_dec.vo theories/Bool/Sumbool.vo
 theories/Arith/Factorial.vo: theories/Arith/Factorial.v theories/Arith/Plus.vo theories/Arith/Mult.vo theories/Arith/Lt.vo
 theories/Arith/Arith_base.vo: theories/Arith/Arith_base.v theories/Arith/Le.vo theories/Arith/Lt.vo theories/Arith/Plus.vo theories/Arith/Gt.vo theories/Arith/Minus.vo theories/Arith/Mult.vo theories/Arith/Between.vo theories/Arith/Peano_dec.vo theories/Arith/Compare_dec.vo theories/Arith/Factorial.vo
@@ -156,7 +156,7 @@ theories/NArith/BinPos.vo: theories/NArith/BinPos.v theories/Logic/Eqdep_dec.vo
 theories/NArith/Pnat.vo: theories/NArith/Pnat.v theories/NArith/BinPos.vo theories/Arith/Le.vo theories/Arith/Lt.vo theories/Arith/Gt.vo theories/Arith/Plus.vo theories/Arith/Mult.vo theories/Arith/Minus.vo
 theories/NArith/BinNat.vo: theories/NArith/BinNat.v theories/NArith/BinPos.vo
 theories/NArith/NArith.vo: theories/NArith/NArith.v theories/NArith/BinPos.vo theories/NArith/BinNat.vo contrib/setoid_ring/NArithRing.vo
-theories/NArith/Nnat.vo: theories/NArith/Nnat.v theories/Arith/Arith_base.vo theories/Arith/Compare_dec.vo theories/Bool/Sumbool.vo theories/Arith/Div2.vo theories/NArith/BinPos.vo theories/NArith/BinNat.vo theories/NArith/Pnat.vo
+theories/NArith/Nnat.vo: theories/NArith/Nnat.v theories/Arith/Arith_base.vo theories/Arith/Compare_dec.vo theories/Bool/Sumbool.vo theories/Arith/Div2.vo theories/Arith/Min.vo theories/Arith/Max.vo theories/NArith/BinPos.vo theories/NArith/BinNat.vo theories/NArith/Pnat.vo
 theories/NArith/Ndigits.vo: theories/NArith/Ndigits.v theories/Bool/Bool.vo theories/Bool/Bvector.vo theories/NArith/BinPos.vo theories/NArith/BinNat.vo
 theories/NArith/Ndec.vo: theories/NArith/Ndec.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/Arith/Arith.vo theories/NArith/BinPos.vo theories/NArith/BinNat.vo theories/NArith/Pnat.vo theories/NArith/Nnat.vo theories/NArith/Ndigits.vo
 theories/NArith/Ndist.vo: theories/NArith/Ndist.v theories/Arith/Arith.vo theories/Arith/Min.vo theories/NArith/BinPos.vo theories/NArith/BinNat.vo theories/NArith/Ndigits.vo
@@ -242,7 +242,7 @@ theories/FSets/FMapWeakFacts.vo: theories/FSets/FMapWeakFacts.v theories/Bool/Bo
 theories/FSets/FMapWeakInterface.vo: theories/FSets/FMapWeakInterface.v theories/FSets/FSetInterface.vo theories/FSets/FSetWeakInterface.vo
 theories/FSets/FMapWeakList.vo: theories/FSets/FMapWeakList.v theories/FSets/FSetInterface.vo theories/FSets/FSetWeakInterface.vo theories/FSets/FMapWeakInterface.vo
 theories/FSets/FMapWeak.vo: theories/FSets/FMapWeak.v theories/Logic/DecidableType.vo theories/Logic/DecidableTypeEx.vo theories/FSets/FMapWeakInterface.vo theories/FSets/FMapWeakList.vo theories/FSets/FMapWeakFacts.vo
-theories/FSets/FMapPositive.vo: theories/FSets/FMapPositive.v theories/Bool/Bool.vo theories/ZArith/ZArith.vo theories/FSets/OrderedType.vo theories/FSets/FMapInterface.vo
+theories/FSets/FMapPositive.vo: theories/FSets/FMapPositive.v theories/Bool/Bool.vo theories/ZArith/ZArith.vo theories/FSets/OrderedType.vo theories/FSets/OrderedTypeEx.vo theories/FSets/FMapInterface.vo
 theories/FSets/FMapIntMap.vo: theories/FSets/FMapIntMap.v theories/Bool/Bool.vo theories/NArith/NArith.vo theories/NArith/Ndigits.vo theories/NArith/Ndec.vo theories/NArith/Nnat.vo theories/IntMap/Allmaps.vo theories/FSets/OrderedType.vo theories/FSets/OrderedTypeEx.vo theories/FSets/FMapInterface.vo theories/FSets/FMapList.vo
 theories/FSets/FSetToFiniteSet.vo: theories/FSets/FSetToFiniteSet.v theories/Sets/Ensembles.vo theories/Sets/Finite_sets.vo theories/FSets/FSetInterface.vo theories/FSets/FSetProperties.vo theories/FSets/OrderedTypeEx.vo
 theories/FSets/FMapAVL.vo: theories/FSets/FMapAVL.v theories/FSets/FSetInterface.vo theories/FSets/FMapInterface.vo theories/FSets/FMapList.vo theories/ZArith/ZArith.vo theories/ZArith/Int.vo
@@ -282,54 +282,6 @@ theories/Reals/DiscrR.vo: theories/Reals/DiscrR.v theories/Reals/RIneq.vo contri
 theories/Reals/Rbase.vo: theories/Reals/Rbase.v theories/Reals/Rdefinitions.vo theories/Reals/Raxioms.vo theories/Reals/RIneq.vo theories/Reals/DiscrR.vo
 theories/Reals/LegacyRfield.vo: theories/Reals/LegacyRfield.v theories/Reals/Raxioms.vo contrib/field/LegacyField.vo
 theories/Reals/Rpow_def.vo: theories/Reals/Rpow_def.v theories/Reals/Rdefinitions.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/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 contrib/setoid_ring/ArithRing.vo
-theories/Reals/Rfunctions.vo: theories/Reals/Rfunctions.v contrib/setoid_ring/ArithRing.vo theories/Reals/Rbase.vo theories/Reals/Rpow_def.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/Rcomplete.vo: theories/Reals/Rcomplete.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/Rcomplete.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/Binomial.vo: theories/Reals/Binomial.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/Binomial.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/Arith/Max.vo theories/Reals/Rseries.vo theories/Reals/SeqProp.vo theories/Reals/Rcomplete.vo theories/Reals/PartSum.vo theories/Reals/AltSeries.vo theories/Reals/Binomial.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
-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/MVT.vo: theories/Reals/MVT.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/MVT.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/MVT.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/Rbase.vo theories/Reals/Rfunctions.vo theories/Reals/SeqSeries.vo theories/Reals/Rtrigo.vo theories/Reals/Ranalysis.vo theories/Reals/Integration.vo
 theories/Sorting/Heap.vo: theories/Sorting/Heap.v theories/Lists/List.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/List.vo theories/Sets/Multiset.vo theories/Arith/Arith.vo
 theories/Sorting/Sorting.vo: theories/Sorting/Sorting.v theories/Lists/List.vo theories/Sets/Multiset.vo theories/Sorting/Permutation.vo theories/Relations/Relations.vo
@@ -341,6 +293,31 @@ theories/QArith/Qring.vo: theories/QArith/Qring.v contrib/setoid_ring/Ring.vo th
 theories/QArith/Qreals.vo: theories/QArith/Qreals.v theories/Reals/Rbase.vo theories/QArith/QArith_base.vo
 theories/QArith/QArith.vo: theories/QArith/QArith.v theories/QArith/QArith_base.vo theories/QArith/Qring.vo theories/QArith/Qreduction.vo
 theories/QArith/Qcanon.vo: theories/QArith/Qcanon.v contrib/setoid_ring/Field.vo theories/QArith/QArith.vo theories/ZArith/Znumtheory.vo theories/Logic/Eqdep_dec.vo
+theories/Ints/Z/IntsZmisc.vo: theories/Ints/Z/IntsZmisc.v theories/ZArith/ZArith.vo
+theories/Ints/Z/Pmod.vo: theories/Ints/Z/Pmod.v theories/Ints/Z/IntsZmisc.vo theories/ZArith/Zwf.vo theories/ZArith/ZArith.vo theories/ZArith/Znumtheory.vo
+theories/Ints/Tactic.vo: theories/Ints/Tactic.v
+theories/Ints/Z/ZAux.vo: theories/Ints/Z/ZAux.v contrib/setoid_ring/ArithRing.vo theories/ZArith/ZArith.vo theories/ZArith/Znumtheory.vo theories/Ints/Tactic.vo
+theories/Ints/Z/ZPowerAux.vo: theories/Ints/Z/ZPowerAux.v theories/ZArith/ZArith.vo theories/ZArith/Znumtheory.vo theories/Ints/Tactic.vo
+theories/Ints/Z/ZDivModAux.vo: theories/Ints/Z/ZDivModAux.v theories/ZArith/ZArith.vo theories/ZArith/Znumtheory.vo theories/Ints/Tactic.vo theories/Ints/Z/ZAux.vo theories/Ints/Z/ZPowerAux.vo
+theories/Ints/Z/Zmod.vo: theories/Ints/Z/Zmod.v theories/ZArith/ZArith.vo theories/Ints/Z/ZAux.vo
+theories/Ints/Basic_type.vo: theories/Ints/Basic_type.v theories/ZArith/ZArith.vo theories/Ints/Z/ZDivModAux.vo theories/Ints/Z/ZPowerAux.vo
+theories/Ints/Int31.vo: theories/Ints/Int31.v theories/ZArith/ZArith.vo theories/Ints/Basic_type.vo
+theories/Ints/num/GenBase.vo: theories/Ints/num/GenBase.v theories/ZArith/ZArith.vo theories/Ints/Z/ZAux.vo theories/Ints/Z/ZDivModAux.vo theories/Ints/Z/ZPowerAux.vo theories/Ints/Basic_type.vo theories/Logic/JMeq.vo
+theories/Ints/num/ZnZ.vo: theories/Ints/num/ZnZ.v theories/Ints/Tactic.vo theories/ZArith/ZArith.vo theories/ZArith/Znumtheory.vo theories/Ints/Basic_type.vo theories/Ints/num/GenBase.vo
+theories/Ints/num/GenAdd.vo: theories/Ints/num/GenAdd.v theories/ZArith/ZArith.vo theories/Ints/Z/ZAux.vo theories/Ints/Z/ZDivModAux.vo theories/Ints/Basic_type.vo theories/Ints/num/GenBase.vo
+theories/Ints/num/GenSub.vo: theories/Ints/num/GenSub.v theories/ZArith/ZArith.vo theories/Ints/Z/ZAux.vo theories/Ints/Z/ZDivModAux.vo theories/Ints/Basic_type.vo theories/Ints/num/GenBase.vo
+theories/Ints/num/GenMul.vo: theories/Ints/num/GenMul.v theories/ZArith/ZArith.vo theories/Ints/Z/ZAux.vo theories/Ints/Z/ZDivModAux.vo theories/Ints/Basic_type.vo theories/Ints/num/GenBase.vo
+theories/Ints/num/GenDivn1.vo: theories/Ints/num/GenDivn1.v theories/ZArith/ZArith.vo theories/Ints/Z/ZDivModAux.vo theories/Ints/Z/ZPowerAux.vo theories/Ints/Basic_type.vo theories/Ints/num/GenBase.vo
+theories/Ints/num/GenDiv.vo: theories/Ints/num/GenDiv.v theories/ZArith/ZArith.vo theories/Ints/Z/ZAux.vo theories/Ints/Z/ZDivModAux.vo theories/Ints/Z/ZPowerAux.vo theories/Ints/Z/Zmod.vo theories/Ints/Basic_type.vo theories/Ints/num/GenBase.vo theories/Ints/num/GenDivn1.vo theories/Ints/num/GenAdd.vo theories/Ints/num/GenSub.vo
+theories/Ints/num/GenSqrt.vo: theories/Ints/num/GenSqrt.v theories/ZArith/ZArith.vo theories/Ints/Z/ZAux.vo theories/Ints/Z/ZDivModAux.vo theories/Ints/Z/ZPowerAux.vo theories/Ints/Basic_type.vo theories/Ints/num/GenBase.vo
+theories/Ints/num/GenLift.vo: theories/Ints/num/GenLift.v theories/ZArith/ZArith.vo theories/Ints/Z/ZAux.vo theories/Ints/Z/ZPowerAux.vo theories/Ints/Z/ZDivModAux.vo theories/Ints/Z/Zmod.vo theories/Ints/Basic_type.vo theories/Ints/num/GenBase.vo
+theories/Ints/num/Zn2Z.vo: theories/Ints/num/Zn2Z.v theories/ZArith/ZArith.vo theories/Ints/Z/ZAux.vo theories/Ints/Z/ZDivModAux.vo theories/Ints/Basic_type.vo theories/Ints/num/GenBase.vo theories/Ints/num/GenAdd.vo theories/Ints/num/GenSub.vo theories/Ints/num/GenMul.vo theories/Ints/num/GenSqrt.vo theories/Ints/num/GenLift.vo theories/Ints/num/GenDivn1.vo theories/Ints/num/GenDiv.vo theories/Ints/num/ZnZ.vo
+theories/Ints/num/Nbasic.vo: theories/Ints/num/Nbasic.v theories/ZArith/ZArith.vo theories/Ints/Basic_type.vo
+theories/Ints/num/NMake.vo: theories/Ints/num/NMake.v theories/ZArith/ZArith.vo theories/Ints/Basic_type.vo theories/Ints/num/ZnZ.vo theories/Ints/num/Zn2Z.vo theories/Ints/num/Nbasic.vo theories/Ints/num/GenMul.vo theories/Ints/num/GenDivn1.vo
+theories/Ints/BigN.vo: theories/Ints/BigN.v theories/Ints/Int31.vo theories/Ints/num/NMake.vo theories/Ints/num/ZnZ.vo
+theories/Ints/num/ZMake.vo: theories/Ints/num/ZMake.v theories/ZArith/ZArith.vo
+theories/Ints/BigZ.vo: theories/Ints/BigZ.v theories/Ints/BigN.vo theories/Ints/num/ZMake.vo
+theories/Ints/num/QMake.vo: theories/Ints/num/QMake.v theories/Bool/Bool.vo theories/ZArith/ZArith.vo theories/Arith/Arith.vo theories/Ints/BigN.vo theories/Ints/BigZ.vo
 contrib/omega/OmegaLemmas.vo: contrib/omega/OmegaLemmas.v theories/ZArith/ZArith_base.vo
 contrib/omega/Omega.vo: contrib/omega/Omega.v theories/ZArith/ZArith_base.vo contrib/omega/OmegaLemmas.vo theories/ZArith/Zhints.vo
 contrib/romega/ReflOmegaCore.vo: contrib/romega/ReflOmegaCore.v theories/Arith/Arith.vo theories/Lists/List.vo theories/Bool/Bool.vo theories/ZArith/ZArith_base.vo contrib/omega/OmegaLemmas.vo theories/Logic/Decidable.vo
diff --git a/contrib/setoid_ring/Ring_zdiv.v b/contrib/setoid_ring/Ring_zdiv.v
index 5b93d50b5..10141b6b4 100644
--- a/contrib/setoid_ring/Ring_zdiv.v
+++ b/contrib/setoid_ring/Ring_zdiv.v
@@ -11,21 +11,11 @@ Require Import BinPos.
 Require Import BinNat.
 Require Import ZArith_base.
 
-Definition Nge a b :=
+Definition Ngeb a b :=
   match a with
    N0 => false
  | Npos na => match Pcompare na b Eq with Lt => false | _ => true end end.
 
-Definition Nminus a b := match a, b with
-  | N0, _ => N0
-  | _ , N0 => a
-  | Npos na, Npos nb => 
-      match (na - nb)%positive with
-        xH => match Pcompare na nb Eq with Eq => N0 | _ => Npos xH end
-      | t => Npos t
-      end
-  end.
-
 Fixpoint pdiv_eucl (a b:positive) {struct a} : N * N :=
   match a with
     | xH => 
@@ -33,24 +23,24 @@ Fixpoint pdiv_eucl (a b:positive) {struct a} : N * N :=
     | xO a' =>
        let (q, r) := pdiv_eucl a' b in
        let r' := (2 * r)%N in
-        if (Nge r' b) then(2 * q + 1, (Nminus r'  (Npos b)))%N
+        if (Ngeb r' b) then(2 * q + 1, (Nminus r'  (Npos b)))%N
         else  (2 * q, r')%N
     | xI a' =>
        let (q, r) := pdiv_eucl a' b in
        let r' := (2 * r + 1)%N in
-        if (Nge r' b) then(2 * q + 1, (Nminus r' (Npos b)))%N
+        if (Ngeb r' b) then(2 * q + 1, (Nminus r' (Npos b)))%N
         else  (2 * q, r')%N
   end.
 
 
-Theorem Nge_correct: forall a b, 
-  if Nge a b then a = ((Nminus a (Npos b)) + Npos b)%N else True.
+Theorem Ngeb_correct: forall a b, 
+  if Ngeb a b then a = ((Nminus a (Npos b)) + Npos b)%N else True.
 destruct a; intros; simpl; auto.
   case_eq (Pcompare p b Eq); intros; auto.
   rewrite (Pcompare_Eq_eq _ _ H).
   assert (HH: forall p, Pminus p p = xH).
     intro p0; unfold Pminus; rewrite Pminus_mask_diag; auto.
-  rewrite HH; auto.
+  simpl; auto.
   generalize (Pplus_minus _ _ H).
   case (p - b)%positive; intros; subst;
   unfold Nplus; rewrite Pplus_comm; trivial.
@@ -79,7 +69,7 @@ Theorem pdiv_eucl_correct: forall a b,
 induction a; unfold pdiv_eucl; fold pdiv_eucl.
   intros b; generalize (IHa b); case pdiv_eucl.
     intros q1 r1 Hq1.
-     generalize (Nge_correct (2 * r1 + 1) b); case Nge; intros H.
+     generalize (Ngeb_correct (2 * r1 + 1) b); case Ngeb; intros H.
      set (u := Nminus (2 * r1 + 1) (Npos b)) in * |- *.
      assert (HH: Z_of_N u = (Z_of_N (2 * r1 + 1) - Zpos b)%Z).
         rewrite H; z_of_n_tac; simpl.
@@ -91,7 +81,7 @@ induction a; unfold pdiv_eucl; fold pdiv_eucl.
      rewrite Zpos_xI; rewrite Hq1; z_of_n_tac; ztac; auto.
   intros b; generalize (IHa b); case pdiv_eucl.
     intros q1 r1 Hq1.
-     generalize (Nge_correct (2 * r1) b); case Nge; intros H.
+     generalize (Ngeb_correct (2 * r1) b); case Ngeb; intros H.
      set (u := Nminus (2 * r1) (Npos b)) in * |- *.
      assert (HH: Z_of_N u = (Z_of_N (2 * r1) - Zpos b)%Z).
         rewrite H; z_of_n_tac; simpl.
diff --git a/theories/Arith/Max.v b/theories/Arith/Max.v
index a3d658d0c..75e1cdf0c 100644
--- a/theories/Arith/Max.v
+++ b/theories/Arith/Max.v
@@ -8,7 +8,7 @@
 
 (*i $Id$ i*)
 
-Require Import Arith.
+Require Import Le.
 
 Open Local Scope nat_scope.
 
diff --git a/theories/FSets/OrderedTypeEx.v b/theories/FSets/OrderedTypeEx.v
index 8da19706e..0295133a6 100644
--- a/theories/FSets/OrderedTypeEx.v
+++ b/theories/FSets/OrderedTypeEx.v
@@ -154,16 +154,16 @@ Module N_as_OT <: UsualOrderedType.
   Definition eq_sym := @sym_eq t.
   Definition eq_trans := @trans_eq t.
 
-  Definition lt p q:= Nle q p = false.
+  Definition lt p q:= Nleb q p = false.
  
-  Definition lt_trans := Nlt_trans.
+  Definition lt_trans := Nltb_trans.
 
   Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y.
   Proof.
   intros; intro.
   rewrite H0 in H.
   unfold lt in H.
-  rewrite Nle_refl in H; discriminate.
+  rewrite Nleb_refl in H; discriminate.
   Qed.
 
   Definition compare : forall x y : t, Compare lt eq x y.
@@ -172,16 +172,15 @@ Module N_as_OT <: UsualOrderedType.
   case_eq ((x ?= y)%N); intros.
   apply EQ; apply Ncompare_Eq_eq; auto.
   apply LT; unfold lt; auto.
-   generalize (Nle_Ncompare y x).
-   destruct (Nle y x); auto.
-   rewrite <- Ncompare_antisym.
+   generalize (Nleb_Nle y x).
+   unfold Nle; rewrite <- Ncompare_antisym.
    destruct (x ?= y)%N; simpl; try discriminate.
-   intros (H0,_); elim H0; auto.
+   clear H; intros H.
+   destruct (Nleb y x); intuition.
   apply GT; unfold lt.
-   generalize (Nle_Ncompare x y).
-   destruct (Nle x y); auto.
-   destruct (x ?= y)%N; simpl; try discriminate.
-   intros (H0,_); elim H0; auto.
+   generalize (Nleb_Nle x y).
+   unfold Nle; destruct (x ?= y)%N; simpl; try discriminate.
+   destruct (Nleb x y); intuition.
   Defined.
 
 End N_as_OT.
diff --git a/theories/IntMap/Adalloc.v b/theories/IntMap/Adalloc.v
index d475bb54d..ef68b1e5c 100644
--- a/theories/IntMap/Adalloc.v
+++ b/theories/IntMap/Adalloc.v
@@ -64,20 +64,20 @@ Section AdAlloc.
 
   Lemma ad_alloc_opt_optimal_1 :
    forall (m:Map A) (a:ad),
-     Nle (ad_alloc_opt m) a = false -> {y : A | MapGet A m a = Some y}.
+     Nleb (ad_alloc_opt m) a = false -> {y : A | MapGet A m a = Some y}.
   Proof.
     induction m as [| a y| m0 H m1 H0]. simpl in |- *. unfold Nle in |- *. simpl in |- *. intros. discriminate H.
     simpl in |- *. intros b H. elim (sumbool_of_bool (Neqb a N0)). intro H0. rewrite H0 in H.
-    unfold Nle in H. cut (N0 = b). intro. split with y. rewrite <- H1. rewrite H0. reflexivity.
+    unfold Nleb in H. cut (N0 = b). intro. split with y. rewrite <- H1. rewrite H0. reflexivity.
     rewrite <- (N_of_nat_of_N b).
     rewrite <- (le_n_O_eq _ (le_S_n _ _ (leb_complete_conv _ _ H))). reflexivity.
     intro H0. rewrite H0 in H. discriminate H.
     intros. simpl in H1. elim (Ndouble_or_double_plus_un a). intro H2. elim H2. intros a0 H3.
-    rewrite H3 in H1. elim (H _ (Nlt_double_mono_conv _ _ (Nmin_lt_3 _ _ _ H1))). intros y H4.
+    rewrite H3 in H1. elim (H _ (Nltb_double_mono_conv _ _ (Nmin_lt_3 _ _ _ H1))). intros y H4.
     split with y. rewrite H3. rewrite MapGet_M2_bit_0_0. rewrite Ndouble_div2. assumption.
     apply Ndouble_bit0.
     intro H2. elim H2. intros a0 H3. rewrite H3 in H1.
-    elim (H0 _ (Nlt_double_plus_one_mono_conv _ _ (Nmin_lt_4 _ _ _ H1))). intros y H4.
+    elim (H0 _ (Nltb_double_plus_one_mono_conv _ _ (Nmin_lt_4 _ _ _ H1))). intros y H4.
     split with y. rewrite H3. rewrite MapGet_M2_bit_0_1. rewrite Ndouble_plus_one_div2.
     assumption.
     apply Ndouble_plus_one_bit0.
@@ -85,7 +85,7 @@ Section AdAlloc.
 
   Lemma ad_alloc_opt_optimal :
    forall (m:Map A) (a:ad),
-     Nle (ad_alloc_opt m) a = false -> in_dom A a m = true.
+     Nleb (ad_alloc_opt m) a = false -> in_dom A a m = true.
   Proof.
     intros. unfold in_dom in |- *. elim (ad_alloc_opt_optimal_1 m a H). intros y H0. rewrite H0.
     reflexivity.
diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v
index 0f2782bd9..b26a22c9e 100644
--- a/theories/NArith/BinNat.v
+++ b/theories/NArith/BinNat.v
@@ -70,6 +70,21 @@ Definition Nplus n m :=
 
 Infix "+" := Nplus : N_scope.
 
+(** Substraction *)
+
+Definition Nminus (x y:N) :=
+  match x, y with
+    | N0, _ => N0
+    | x, N0 => x
+    | Npos x', Npos y' =>
+      match Pcompare x' y' Eq with
+        | Lt | Eq => N0
+        | Gt => Npos (x' - y')
+      end
+  end.
+
+Infix "-" := Nminus : N_scope.
+
 (** Multiplication *)
 
 Definition Nmult n m :=
@@ -93,6 +108,28 @@ Definition Ncompare n m :=
 
 Infix "?=" := Ncompare (at level 70, no associativity) : N_scope.
 
+Definition Nlt (x y:N) := (x ?= y) = Lt.
+Definition Ngt (x y:N) := (x ?= y) = Gt.
+Definition Nle (x y:N) := (x ?= y) <> Gt.
+Definition Nge (x y:N) := (x ?= y) <> Lt.
+
+Infix "<=" := Nle : N_scope.
+Infix "<" := Nlt : N_scope.
+Infix ">=" := Nge : N_scope.
+Infix ">" := Ngt : N_scope.
+
+(** Min and max *)
+
+Definition Nmin (n n' : N) := match Ncompare n n' with 
+ | Lt | Eq => n
+ | Gt => n'
+ end.
+
+Definition Nmax (n n' : N) := match Ncompare n n' with 
+ | Lt | Eq => n'
+ | Gt => n
+ end.
+
 (** convenient induction principles *)
 
 Lemma N_ind_double :
@@ -217,6 +254,23 @@ intro n; pattern n in |- *; apply Nind; clear n; simpl in |- *.
   apply IHn; apply Nsucc_inj; assumption.
 Qed.
 
+(** Properties of substraction. *)
+
+Lemma Nle_Nminus_N0 : forall n n':N, n <= n' -> n-n' = N0.
+Proof.
+  destruct n; destruct n'; simpl; intros; auto.
+  elim H; auto.
+  red in H; simpl in *.
+  intros; destruct (Pcompare p p0 Eq); auto.
+  elim H; auto.
+Qed.
+
+Lemma Nminus_N0_Nle : forall n n':N, n-n' = N0 -> n <= n'.
+Proof.
+  destruct n; destruct n'; red; simpl; intros; try discriminate.
+  destruct (Pcompare p p0 Eq); discriminate.
+Qed.
+
 (** Properties of multiplication *)
 
 Theorem Nmult_0_l : forall n:N, N0 * n = N0.
diff --git a/theories/NArith/BinPos.v b/theories/NArith/BinPos.v
index c8c94f781..2e3c6a3a5 100644
--- a/theories/NArith/BinPos.v
+++ b/theories/NArith/BinPos.v
@@ -13,7 +13,7 @@ Unset Boxed Definitions.
 (**********************************************************************)
 (** Binary positive numbers *)
 
-(** Original development by Pierre Crégut, CNET, Lannion, France *)
+(** Original development by Pierre Crégut, CNET, Lannion, France *)
 
 Inductive positive : Set :=
 | xI : positive -> positive
@@ -220,6 +220,16 @@ Fixpoint Pcompare (x y:positive) (r:comparison) {struct y} : comparison :=
 
 Infix "?=" := Pcompare (at level 70, no associativity) : positive_scope.
 
+Definition Pmin (p p' : positive) := match Pcompare p p' Eq with 
+ | Lt | Eq => p 
+ | Gt => p'
+ end.
+
+Definition Pmax (p p' : positive) := match Pcompare p p' Eq with 
+ | Lt | Eq => p' 
+ | Gt => p
+ end.
+
 (**********************************************************************)
 (** Miscellaneous properties of binary positive numbers *)
 
diff --git a/theories/NArith/Ndec.v b/theories/NArith/Ndec.v
index 29ac72d00..bbab81f4e 100644
--- a/theories/NArith/Ndec.v
+++ b/theories/NArith/Ndec.v
@@ -37,6 +37,13 @@ Proof.
  induction p; destruct p'; simpl; intros; try discriminate; auto.
 Qed.
 
+Lemma Peqb_complete : forall p p', Peqb p p' = true -> p = p'.
+Proof.
+  intros.
+  apply Pcompare_Eq_eq.
+  apply Peqb_Pcompare; auto.
+Qed.
+
 Lemma Pcompare_Peqb : forall p p', Pcompare p p' Eq = Eq -> Peqb p p' = true.
 Proof. 
 intros; rewrite <- (Pcompare_Eq_eq _ _ H).
@@ -208,205 +215,220 @@ Qed.
 
 (** A boolean order on [N] *)
 
-Definition Nle (a b:N) := leb (nat_of_N a) (nat_of_N b).
+Definition Nleb (a b:N) := leb (nat_of_N a) (nat_of_N b).
 
-Lemma Nle_Ncompare : forall a b, Nle a b = true <-> Ncompare a b <> Gt.
+Lemma Nleb_Nle : forall a b, Nleb a b = true <-> Nle a b.
 Proof.
- intros; rewrite nat_of_Ncompare.
- unfold Nle; apply leb_compare.
+ intros; unfold Nle; rewrite nat_of_Ncompare.
+ unfold Nleb; apply leb_compare.
 Qed.
 
-Lemma Nle_refl : forall a, Nle a a = true.
+Lemma Nleb_refl : forall a, Nleb a a = true.
 Proof.
-  intro. unfold Nle in |- *. apply leb_correct. apply le_n.
+  intro. unfold Nleb in |- *. apply leb_correct. apply le_n.
 Qed.
 
-Lemma Nle_antisym :
- forall a b, Nle a b = true -> Nle b a = true -> a = b.
+Lemma Nleb_antisym :
+ forall a b, Nleb a b = true -> Nleb b a = true -> a = b.
 Proof.
-  unfold Nle in |- *. intros. rewrite <- (N_of_nat_of_N a). rewrite <- (N_of_nat_of_N b).
+  unfold Nleb in |- *. intros. rewrite <- (N_of_nat_of_N a). rewrite <- (N_of_nat_of_N b).
   rewrite (le_antisym _ _ (leb_complete _ _ H) (leb_complete _ _ H0)). reflexivity.
 Qed.
 
-Lemma Nle_trans :
- forall a b c, Nle a b = true -> Nle b c = true -> Nle a c = true.
+Lemma Nleb_trans :
+ forall a b c, Nleb a b = true -> Nleb b c = true -> Nleb a c = true.
 Proof.
-  unfold Nle in |- *. intros. apply leb_correct. apply le_trans with (m := nat_of_N b).
+  unfold Nleb in |- *. intros. apply leb_correct. apply le_trans with (m := nat_of_N b).
   apply leb_complete. assumption.
   apply leb_complete. assumption.
 Qed.
 
-Lemma Nle_lt_trans :
+Lemma Nleb_ltb_trans :
  forall a b c,
-   Nle a b = true -> Nle c b = false -> Nle c a = false.
+   Nleb a b = true -> Nleb c b = false -> Nleb c a = false.
 Proof.
-  unfold Nle in |- *. intros. apply leb_correct_conv. apply le_lt_trans with (m := nat_of_N b).
+  unfold Nleb in |- *. intros. apply leb_correct_conv. apply le_lt_trans with (m := nat_of_N b).
   apply leb_complete. assumption.
   apply leb_complete_conv. assumption.
 Qed.
 
-Lemma Nlt_le_trans :
+Lemma Nltb_leb_trans :
  forall a b c,
-   Nle b a = false -> Nle b c = true -> Nle c a = false.
+   Nleb b a = false -> Nleb b c = true -> Nleb c a = false.
 Proof.
-  unfold Nle in |- *. intros. apply leb_correct_conv. apply lt_le_trans with (m := nat_of_N b).
+  unfold Nleb in |- *. intros. apply leb_correct_conv. apply lt_le_trans with (m := nat_of_N b).
   apply leb_complete_conv. assumption.
   apply leb_complete. assumption.
 Qed.
 
-Lemma Nlt_trans :
+Lemma Nltb_trans :
  forall a b c,
-   Nle b a = false -> Nle c b = false -> Nle c a = false.
+   Nleb b a = false -> Nleb c b = false -> Nleb c a = false.
 Proof.
-  unfold Nle in |- *. intros. apply leb_correct_conv. apply lt_trans with (m := nat_of_N b).
+  unfold Nleb in |- *. intros. apply leb_correct_conv. apply lt_trans with (m := nat_of_N b).
   apply leb_complete_conv. assumption.
   apply leb_complete_conv. assumption.
 Qed.
 
-Lemma Nlt_le_weak : forall a b:N, Nle b a = false -> Nle a b = true.
+Lemma Nltb_leb_weak : forall a b:N, Nleb b a = false -> Nleb a b = true.
 Proof.
-  unfold Nle in |- *. intros. apply leb_correct. apply lt_le_weak.
+  unfold Nleb in |- *. intros. apply leb_correct. apply lt_le_weak.
   apply leb_complete_conv. assumption.
 Qed.
 
-Lemma Nle_double_mono :
+Lemma Nleb_double_mono :
  forall a b,
-   Nle a b = true -> Nle (Ndouble a) (Ndouble b) = true.
+   Nleb a b = true -> Nleb (Ndouble a) (Ndouble b) = true.
 Proof.
-  unfold Nle in |- *. intros. rewrite nat_of_Ndouble. rewrite nat_of_Ndouble. apply leb_correct.
+  unfold Nleb in |- *. intros. rewrite nat_of_Ndouble. rewrite nat_of_Ndouble. apply leb_correct.
   simpl in |- *. apply plus_le_compat. apply leb_complete. assumption.
   apply plus_le_compat. apply leb_complete. assumption.
   apply le_n.
 Qed.
 
-Lemma Nle_double_plus_one_mono :
+Lemma Nleb_double_plus_one_mono :
  forall a b,
-   Nle a b = true ->
-   Nle (Ndouble_plus_one a) (Ndouble_plus_one b) = true.
+   Nleb a b = true ->
+   Nleb (Ndouble_plus_one a) (Ndouble_plus_one b) = true.
 Proof.
-  unfold Nle in |- *. intros. rewrite nat_of_Ndouble_plus_one. rewrite nat_of_Ndouble_plus_one.
+  unfold Nleb in |- *. intros. rewrite nat_of_Ndouble_plus_one. rewrite nat_of_Ndouble_plus_one.
   apply leb_correct. apply le_n_S. simpl in |- *. apply plus_le_compat. apply leb_complete.
   assumption.
   apply plus_le_compat. apply leb_complete. assumption.
   apply le_n.
 Qed.
 
-Lemma Nle_double_mono_conv :
+Lemma Nleb_double_mono_conv :
  forall a b,
-   Nle (Ndouble a) (Ndouble b) = true -> Nle a b = true.
+   Nleb (Ndouble a) (Ndouble b) = true -> Nleb a b = true.
 Proof.
-  unfold Nle in |- *. intros a b. rewrite nat_of_Ndouble. rewrite nat_of_Ndouble. intro.
+  unfold Nleb in |- *. intros a b. rewrite nat_of_Ndouble. rewrite nat_of_Ndouble. intro.
   apply leb_correct. apply (mult_S_le_reg_l 1). apply leb_complete. assumption.
 Qed.
 
-Lemma Nle_double_plus_one_mono_conv :
+Lemma Nleb_double_plus_one_mono_conv :
  forall a b,
-   Nle (Ndouble_plus_one a) (Ndouble_plus_one b) = true ->
-   Nle a b = true.
+   Nleb (Ndouble_plus_one a) (Ndouble_plus_one b) = true ->
+   Nleb a b = true.
 Proof.
-  unfold Nle in |- *. intros a b. rewrite nat_of_Ndouble_plus_one. rewrite nat_of_Ndouble_plus_one.
+  unfold Nleb in |- *. intros a b. rewrite nat_of_Ndouble_plus_one. rewrite nat_of_Ndouble_plus_one.
   intro. apply leb_correct. apply (mult_S_le_reg_l 1). apply le_S_n. apply leb_complete.
   assumption.
 Qed.
 
-Lemma Nlt_double_mono :
+Lemma Nltb_double_mono :
  forall a b,
-   Nle a b = false -> Nle (Ndouble a) (Ndouble b) = false.
+   Nleb a b = false -> Nleb (Ndouble a) (Ndouble b) = false.
 Proof.
-  intros. elim (sumbool_of_bool (Nle (Ndouble a) (Ndouble b))). intro H0.
-  rewrite (Nle_double_mono_conv _ _ H0) in H. discriminate H.
+  intros. elim (sumbool_of_bool (Nleb (Ndouble a) (Ndouble b))). intro H0.
+  rewrite (Nleb_double_mono_conv _ _ H0) in H. discriminate H.
   trivial.
 Qed.
 
-Lemma Nlt_double_plus_one_mono :
+Lemma Nltb_double_plus_one_mono :
  forall a b,
-   Nle a b = false ->
-   Nle (Ndouble_plus_one a) (Ndouble_plus_one b) = false.
+   Nleb a b = false ->
+   Nleb (Ndouble_plus_one a) (Ndouble_plus_one b) = false.
 Proof.
-  intros. elim (sumbool_of_bool (Nle (Ndouble_plus_one a) (Ndouble_plus_one b))). intro H0.
-  rewrite (Nle_double_plus_one_mono_conv _ _ H0) in H. discriminate H.
+  intros. elim (sumbool_of_bool (Nleb (Ndouble_plus_one a) (Ndouble_plus_one b))). intro H0.
+  rewrite (Nleb_double_plus_one_mono_conv _ _ H0) in H. discriminate H.
   trivial.
 Qed.
 
-Lemma Nlt_double_mono_conv :
+Lemma Nltb_double_mono_conv :
  forall a b,
-   Nle (Ndouble a) (Ndouble b) = false -> Nle a b = false.
+   Nleb (Ndouble a) (Ndouble b) = false -> Nleb a b = false.
 Proof.
-  intros. elim (sumbool_of_bool (Nle a b)). intro H0. rewrite (Nle_double_mono _ _ H0) in H.
+  intros. elim (sumbool_of_bool (Nleb a b)). intro H0. rewrite (Nleb_double_mono _ _ H0) in H.
   discriminate H.
   trivial.
 Qed.
 
-Lemma Nlt_double_plus_one_mono_conv :
+Lemma Nltb_double_plus_one_mono_conv :
  forall a b,
-   Nle (Ndouble_plus_one a) (Ndouble_plus_one b) = false ->
-   Nle a b = false.
+   Nleb (Ndouble_plus_one a) (Ndouble_plus_one b) = false ->
+   Nleb a b = false.
 Proof.
-  intros. elim (sumbool_of_bool (Nle a b)). intro H0.
-  rewrite (Nle_double_plus_one_mono _ _ H0) in H. discriminate H.
+  intros. elim (sumbool_of_bool (Nleb a b)). intro H0.
+  rewrite (Nleb_double_plus_one_mono _ _ H0) in H. discriminate H.
   trivial.
 Qed.
 
-(* A [min] function over [N] *)
+(* An alternate [min] function over [N] *)
 
-Definition Nmin (a b:N) := if Nle a b then a else b.
+Definition Nmin' (a b:N) := if Nleb a b then a else b.
+
+Lemma Nmin_Nmin' : forall a b, Nmin a b = Nmin' a b.
+Proof.
+ unfold Nmin, Nmin', Nleb; intros.
+ rewrite nat_of_Ncompare.
+ generalize (leb_compare (nat_of_N a) (nat_of_N b)); 
+ destruct (nat_compare (nat_of_N a) (nat_of_N b)); 
+ destruct (leb (nat_of_N a) (nat_of_N b)); intuition.
+ lapply H1; intros; discriminate.
+ lapply H1; intros; discriminate.
+Qed.
 
 Lemma Nmin_choice : forall a b, {Nmin a b = a} + {Nmin a b = b}.
 Proof.
-  unfold Nmin in |- *. intros. elim (sumbool_of_bool (Nle a b)). intro H. left. rewrite H.
-  reflexivity.
-  intro H. right. rewrite H. reflexivity.
+  unfold Nmin in *; intros; destruct (Ncompare a b); auto.
 Qed.
 
-Lemma Nmin_le_1 : forall a b, Nle (Nmin a b) a = true.
+Lemma Nmin_le_1 : forall a b, Nleb (Nmin a b) a = true.
 Proof.
-  unfold Nmin in |- *. intros. elim (sumbool_of_bool (Nle a b)). intro H. rewrite H.
-  apply Nle_refl.
-  intro H. rewrite H. apply Nlt_le_weak. assumption.
+  intros; rewrite Nmin_Nmin'.
+  unfold Nmin'; elim (sumbool_of_bool (Nleb a b)). intro H. rewrite H.
+  apply Nleb_refl.
+  intro H. rewrite H. apply Nltb_leb_weak. assumption.
 Qed.
 
-Lemma Nmin_le_2 : forall a b, Nle (Nmin a b) b = true.
+Lemma Nmin_le_2 : forall a b, Nleb (Nmin a b) b = true.
 Proof.
-  unfold Nmin in |- *. intros. elim (sumbool_of_bool (Nle a b)). intro H. rewrite H. assumption.
-  intro H. rewrite H. apply Nle_refl.
+  intros; rewrite Nmin_Nmin'.
+  unfold Nmin'; elim (sumbool_of_bool (Nleb a b)). intro H. rewrite H. assumption.
+  intro H. rewrite H. apply Nleb_refl.
 Qed.
 
 Lemma Nmin_le_3 :
- forall a b c, Nle a (Nmin b c) = true -> Nle a b = true.
+ forall a b c, Nleb a (Nmin b c) = true -> Nleb a b = true.
 Proof.
-  unfold Nmin in |- *. intros. elim (sumbool_of_bool (Nle b c)). intro H0. rewrite H0 in H.
+  intros; rewrite Nmin_Nmin' in *. 
+  unfold Nmin' in *; elim (sumbool_of_bool (Nleb b c)). intro H0. rewrite H0 in H.
   assumption.
-  intro H0. rewrite H0 in H. apply Nlt_le_weak. apply Nle_lt_trans with (b := c); assumption.
+  intro H0. rewrite H0 in H. apply Nltb_leb_weak. apply Nleb_ltb_trans with (b := c); assumption.
 Qed.
 
 Lemma Nmin_le_4 :
- forall a b c, Nle a (Nmin b c) = true -> Nle a c = true.
+ forall a b c, Nleb a (Nmin b c) = true -> Nleb a c = true.
 Proof.
-  unfold Nmin in |- *. intros. elim (sumbool_of_bool (Nle b c)). intro H0. rewrite H0 in H.
-  apply Nle_trans with (b := b); assumption.
+  intros; rewrite Nmin_Nmin' in *. 
+  unfold Nmin' in *; elim (sumbool_of_bool (Nleb b c)). intro H0. rewrite H0 in H.
+  apply Nleb_trans with (b := b); assumption.
   intro H0. rewrite H0 in H. assumption.
 Qed.
 
 Lemma Nmin_le_5 :
  forall a b c,
-   Nle a b = true -> Nle a c = true -> Nle a (Nmin b c) = true.
+   Nleb a b = true -> Nleb a c = true -> Nleb a (Nmin b c) = true.
 Proof.
   intros. elim (Nmin_choice b c). intro H1. rewrite H1. assumption.
   intro H1. rewrite H1. assumption.
 Qed.
 
 Lemma Nmin_lt_3 :
- forall a b c, Nle (Nmin b c) a = false -> Nle b a = false.
+ forall a b c, Nleb (Nmin b c) a = false -> Nleb b a = false.
 Proof.
-  unfold Nmin in |- *. intros. elim (sumbool_of_bool (Nle b c)). intro H0. rewrite H0 in H.
+  intros; rewrite Nmin_Nmin' in *. 
+  unfold Nmin' in *. intros. elim (sumbool_of_bool (Nleb b c)). intro H0. rewrite H0 in H.
   assumption.
-  intro H0. rewrite H0 in H. apply Nlt_trans with (b := c); assumption.
+  intro H0. rewrite H0 in H. apply Nltb_trans with (b := c); assumption.
 Qed.
 
 Lemma Nmin_lt_4 :
- forall a b c, Nle (Nmin b c) a = false -> Nle c a = false.
+ forall a b c, Nleb (Nmin b c) a = false -> Nleb c a = false.
 Proof.
-  unfold Nmin in |- *. intros. elim (sumbool_of_bool (Nle b c)). intro H0. rewrite H0 in H.
-  apply Nlt_le_trans with (b := b); assumption.
+  intros; rewrite Nmin_Nmin' in *. 
+  unfold Nmin' in *. elim (sumbool_of_bool (Nleb b c)). intro H0. rewrite H0 in H.
+  apply Nltb_leb_trans with (b := b); assumption.
   intro H0. rewrite H0 in H. assumption.
 Qed.
diff --git a/theories/NArith/Nnat.v b/theories/NArith/Nnat.v
index 5465bc692..e19989aed 100644
--- a/theories/NArith/Nnat.v
+++ b/theories/NArith/Nnat.v
@@ -12,6 +12,8 @@ Require Import Arith_base.
 Require Import Compare_dec.
 Require Import Sumbool.
 Require Import Div2.
+Require Import Min.
+Require Import Max.
 Require Import BinPos.
 Require Import BinNat.
 Require Import Pnat.
@@ -108,6 +110,27 @@ Proof.
   apply N_of_nat_of_N.
 Qed.
 
+Lemma nat_of_Nminus :
+  forall a a', nat_of_N (Nminus a a') = ((nat_of_N a)-(nat_of_N a'))%nat.
+Proof.
+  destruct a; destruct a'; simpl; auto with arith.
+  case_eq (Pcompare p p0 Eq); simpl; intros.
+  rewrite (Pcompare_Eq_eq _ _ H); auto with arith.
+  symmetry; apply not_le_minus_0.
+  generalize (nat_of_P_lt_Lt_compare_morphism _ _ H); auto with arith.
+  apply nat_of_P_minus_morphism; auto.
+Qed.
+
+Lemma N_of_minus :
+  forall n n', N_of_nat (n-n') = Nminus (N_of_nat n) (N_of_nat n').
+Proof.
+  intros.
+  pattern n at 1; rewrite <- (nat_of_N_of_nat n).
+  pattern n' at 1; rewrite <- (nat_of_N_of_nat n').
+  rewrite <- nat_of_Nminus.
+  apply N_of_nat_of_N.
+Qed.
+
 Lemma nat_of_Nmult : 
   forall a a', nat_of_N (Nmult a a') = (nat_of_N a)*(nat_of_N a').
 Proof.
@@ -175,3 +198,43 @@ Proof.
   pattern n' at 1; rewrite <- (nat_of_N_of_nat n').
   symmetry; apply nat_of_Ncompare.
 Qed.
+
+Lemma nat_of_Nmin :
+  forall a a', nat_of_N (Nmin a a') = min (nat_of_N a) (nat_of_N a').
+Proof.
+  intros; unfold Nmin; rewrite nat_of_Ncompare.
+  unfold nat_compare.
+  destruct (lt_eq_lt_dec (nat_of_N a) (nat_of_N a')) as [[|]|]; 
+    simpl; intros; symmetry; auto with arith.
+  apply min_l; rewrite e; auto with arith.
+Qed.
+
+Lemma N_of_min :
+  forall n n', N_of_nat (min n n') = Nmin (N_of_nat n) (N_of_nat n').
+Proof.
+  intros.
+  pattern n at 1; rewrite <- (nat_of_N_of_nat n).
+  pattern n' at 1; rewrite <- (nat_of_N_of_nat n').
+  rewrite <- nat_of_Nmin.
+  apply N_of_nat_of_N.
+Qed.
+
+Lemma nat_of_Nmax :
+  forall a a', nat_of_N (Nmax a a') = max (nat_of_N a) (nat_of_N a').
+Proof.
+  intros; unfold Nmax; rewrite nat_of_Ncompare.
+  unfold nat_compare.
+  destruct (lt_eq_lt_dec (nat_of_N a) (nat_of_N a')) as [[|]|]; 
+    simpl; intros; symmetry; auto with arith.
+  apply max_r; rewrite e; auto with arith.
+Qed.
+
+Lemma N_of_max :
+  forall n n', N_of_nat (max n n') = Nmax (N_of_nat n) (N_of_nat n').
+Proof.
+  intros.
+  pattern n at 1; rewrite <- (nat_of_N_of_nat n).
+  pattern n' at 1; rewrite <- (nat_of_N_of_nat n').
+  rewrite <- nat_of_Nmax.
+  apply N_of_nat_of_N.
+Qed.
diff --git a/theories/NArith/Pnat.v b/theories/NArith/Pnat.v
index f1c1d72fc..9bec3e994 100644
--- a/theories/NArith/Pnat.v
+++ b/theories/NArith/Pnat.v
@@ -14,7 +14,7 @@ Require Import BinPos.
 (** Properties of the injection from binary positive numbers to Peano 
     natural numbers *)
 
-(** Original development by Pierre Crégut, CNET, Lannion, France *)
+(** Original development by Pierre Crégut, CNET, Lannion, France *)
 
 Require Import Le.
 Require Import Lt.