Numbers: BigN and BigZ get instantiations of all properties about div and mod

 NB: for declaring div and mod as a morphism, even when divisor is zero,
 I've slightly changed the definition of div_eucl: it now starts by a
 check of whether the divisor is zero. Not very nice, but this way
 we can say that BigN.div and BigZ.div _always_ answer like Zdiv.Zdiv.

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

9 files changed, 136 insertions, 57 deletions

diff --git a/theories/Numbers/Integer/BigZ/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v
index 1ec7960ae..fc94f693a 100644
--- a/theories/Numbers/Integer/BigZ/BigZ.v
+++ b/theories/Numbers/Integer/BigZ/BigZ.v
@@ -11,10 +11,7 @@
 (*i $Id$ i*)
 
 Require Export BigN.
-Require Import ZProperties.
-Require Import ZSig.
-Require Import ZSigZAxioms.
-Require Import ZMake.
+Require Import ZProperties ZDivFloor ZSig ZSigZAxioms ZMake.
 
 Module BigZ <: ZType := ZMake.Make BigN.
 
@@ -22,6 +19,7 @@ Module BigZ <: ZType := ZMake.Make BigN.
 
 Module Export BigZAxiomsMod := ZSig_ZAxioms BigZ.
 Module Export BigZPropMod := ZPropFunct BigZAxiomsMod.
+Module Export BigZDivPropMod := ZDivPropFunct BigZAxiomsMod BigZPropMod.
 
 (** Notations about [BigZ] *)
 
@@ -71,6 +69,7 @@ Infix "<=" := BigZ.le : bigZ_scope.
 Notation "x > y" := (BigZ.lt y x)(only parsing) : bigZ_scope.
 Notation "x >= y" := (BigZ.le y x)(only parsing) : bigZ_scope.
 Notation "[ i ]" := (BigZ.to_Z i) : bigZ_scope.
+Infix "mod" := modulo (at level 40, no associativity) : bigN_scope.
 
 Local Open Scope bigZ_scope.
 
diff --git a/theories/Numbers/Integer/BigZ/ZMake.v b/theories/Numbers/Integer/BigZ/ZMake.v
index 827877fc5..0ab509650 100644
--- a/theories/Numbers/Integer/BigZ/ZMake.v
+++ b/theories/Numbers/Integer/BigZ/ZMake.v
@@ -369,17 +369,17 @@ Module Make (N:NType) <: ZType.
   end.
 
 
- Theorem spec_div_eucl: forall x y,
+ Theorem spec_div_eucl_nz: forall x y,
       to_Z y <> 0 ->
       let (q,r) := div_eucl x y in
       (to_Z q, to_Z r) = Zdiv_eucl (to_Z x) (to_Z y).
  unfold div_eucl, to_Z; intros [x | x] [y | y] H.
  assert (H1: 0 < N.to_Z y).
    generalize (N.spec_pos y); auto with zarith.
- generalize (N.spec_div_eucl x y H1); case N.div_eucl; auto.
+ generalize (N.spec_div_eucl x y); case N.div_eucl; auto.
  assert (HH: 0 < N.to_Z y).
    generalize (N.spec_pos y); auto with zarith.
- generalize (N.spec_div_eucl x y HH); case N.div_eucl; auto.
+ generalize (N.spec_div_eucl x y); case N.div_eucl; auto.
  intros q r; generalize (N.spec_pos x) HH; unfold Zdiv_eucl;
    case_eq (N.to_Z x); case_eq (N.to_Z y);
      try (intros; apply False_ind; auto with zarith; fail).
@@ -411,7 +411,7 @@ Module Make (N:NType) <: ZType.
    intros; apply False_ind; auto with zarith.
  assert (HH: 0 < N.to_Z y).
    generalize (N.spec_pos y); auto with zarith.
- generalize (N.spec_div_eucl x y HH); case N.div_eucl; auto.
+ generalize (N.spec_div_eucl x y); case N.div_eucl; auto.
  intros q r; generalize (N.spec_pos x) HH; unfold Zdiv_eucl;
    case_eq (N.to_Z x); case_eq (N.to_Z y);
      try (intros; apply False_ind; auto with zarith; fail).
@@ -441,7 +441,7 @@ Module Make (N:NType) <: ZType.
  rewrite N.spec_0; generalize (N.spec_pos r); intros; apply False_ind; auto with zarith.
  assert (H1: 0 < N.to_Z y).
    generalize (N.spec_pos y); auto with zarith.
- generalize (N.spec_div_eucl x y H1); case N.div_eucl; auto.
+ generalize (N.spec_div_eucl x y); case N.div_eucl; auto.
  intros q r; generalize (N.spec_pos x) H1; unfold Zdiv_eucl;
    case_eq (N.to_Z x); case_eq (N.to_Z y);
      try (intros; apply False_ind; auto with zarith; fail).
@@ -455,11 +455,43 @@ Module Make (N:NType) <: ZType.
  rewrite <- H2; auto.
  Qed.
 
+ Lemma Zdiv_eucl_0 : forall a, Zdiv_eucl a 0 = (0,0).
+ Proof. destruct a; auto. Qed.
+
+ Theorem spec_div_eucl: forall x y,
+      let (q,r) := div_eucl x y in
+      (to_Z q, to_Z r) = Zdiv_eucl (to_Z x) (to_Z y).
+ Proof.
+ intros. destruct (Z_eq_dec (to_Z y) 0) as [EQ|NEQ];
+  [|apply spec_div_eucl_nz; auto].
+ unfold div_eucl.
+ destruct x; destruct y; simpl in *.
+ generalize (N.spec_div_eucl t0 t1). destruct N.div_eucl; simpl; auto.
+ generalize (N.spec_div_eucl t0 t1). destruct N.div_eucl; simpl; auto.
+ assert (EQ' : N.to_Z t1 = 0) by auto with zarith.
+ rewrite EQ'. simpl. rewrite Zdiv_eucl_0. injection 1; intros.
+ generalize (N.spec_compare N.zero t3); destruct N.compare.
+ simpl. intros. f_equal; auto with zarith.
+ rewrite N.spec_0; intro; exfalso; auto with zarith.
+ rewrite N.spec_0; intro; exfalso; auto with zarith.
+ generalize (N.spec_div_eucl t0 t1). destruct N.div_eucl; simpl; auto.
+ assert (EQ' : N.to_Z t1 = 0) by auto with zarith.
+ rewrite EQ'. simpl. rewrite 2 Zdiv_eucl_0. injection 1; intros.
+ generalize (N.spec_compare N.zero t3); destruct N.compare.
+ simpl. intros. f_equal; auto with zarith.
+ rewrite N.spec_0; intro; exfalso; auto with zarith.
+ rewrite N.spec_0; intro; exfalso; auto with zarith.
+ generalize (N.spec_div_eucl t0 t1). destruct N.div_eucl; simpl; auto.
+ assert (EQ' : N.to_Z t1 = 0) by auto with zarith.
+ rewrite EQ'. simpl. rewrite 2 Zdiv_eucl_0. injection 1; intros.
+ f_equal; auto with zarith.
+ Qed.
+
  Definition div x y := fst (div_eucl x y).
 
  Definition spec_div: forall x y,
-     to_Z y <> 0 -> to_Z (div x y) = to_Z x / to_Z y.
- intros x y H1; generalize (spec_div_eucl x y H1); unfold div, Zdiv.
+     to_Z (div x y) = to_Z x / to_Z y.
+ intros x y; generalize (spec_div_eucl x y); unfold div, Zdiv.
  case div_eucl; case Zdiv_eucl; simpl; auto.
  intros q r q11 r1 H; injection H; auto.
  Qed.
@@ -467,8 +499,8 @@ Module Make (N:NType) <: ZType.
  Definition modulo x y := snd (div_eucl x y).
 
  Theorem spec_modulo:
-   forall x y, to_Z y <> 0  -> to_Z (modulo x y) = to_Z x mod to_Z y.
- intros x y H1; generalize (spec_div_eucl x y H1); unfold modulo, Zmod.
+   forall x y, to_Z (modulo x y) = to_Z x mod to_Z y.
+ intros x y; generalize (spec_div_eucl x y); unfold modulo, Zmod.
  case div_eucl; case Zdiv_eucl; simpl; auto.
  intros q r q11 r1 H; injection H; auto.
  Qed.
diff --git a/theories/Numbers/Integer/SpecViaZ/ZSig.v b/theories/Numbers/Integer/SpecViaZ/ZSig.v
index ef3cd5c34..a7c5473aa 100644
--- a/theories/Numbers/Integer/SpecViaZ/ZSig.v
+++ b/theories/Numbers/Integer/SpecViaZ/ZSig.v
@@ -98,17 +98,16 @@ Module Type ZType.
 
  Parameter div_eucl : t -> t -> t * t.
 
- Parameter spec_div_eucl: forall x y, [y] <> 0 ->
+ Parameter spec_div_eucl: forall x y,
    let (q,r) := div_eucl x y in ([q], [r]) = Zdiv_eucl [x] [y].
 
  Parameter div : t -> t -> t.
 
- Parameter spec_div: forall x y, [y] <> 0 -> [div x y] = [x] / [y].
+ Parameter spec_div: forall x y, [div x y] = [x] / [y].
 
  Parameter modulo : t -> t -> t.
 
- Parameter spec_modulo: forall x y, [y] <> 0 ->
-   [modulo x y] = [x] mod [y].
+ Parameter spec_modulo: forall x y, [modulo x y] = [x] mod [y].
 
  Parameter gcd : t -> t -> t.
 
diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
index 80166d5bf..cb5a771da 100644
--- a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
+++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
@@ -8,11 +8,15 @@
 
 (*i $Id$ i*)
 
-Require Import ZArith ZAxioms ZSgnAbs ZSig.
+Require Import ZArith ZAxioms ZDivFloor ZSig.
 
-(** * The interface [ZSig.ZType] implies the interface [ZAxiomsSig] *)
+(** * The interface [ZSig.ZType] implies the interface [ZAxiomsSig]
 
-Module ZSig_ZAxioms (Z:ZType) <: ZAxiomsExtSig.
+    It also provides [sgn], [abs], [div], [mod]
+*)
+
+
+Module ZSig_ZAxioms (Z:ZType) <: ZAxiomsSig <: ZDivSig.
 
 Local Notation "[ x ]" := (Z.to_Z x).
 Local Infix "=="  := Z.eq (at level 70).
@@ -26,7 +30,7 @@ Local Infix "<" := Z.lt.
 
 Hint Rewrite
  Z.spec_0 Z.spec_1 Z.spec_add Z.spec_sub Z.spec_pred Z.spec_succ
- Z.spec_mul Z.spec_opp Z.spec_of_Z : zspec.
+ Z.spec_mul Z.spec_opp Z.spec_of_Z Z.spec_div Z.spec_modulo: zspec.
 
 Ltac zsimpl := unfold Z.eq in *; autorewrite with zspec.
 Ltac zcongruence := repeat red; intros; zsimpl; congruence.
@@ -235,32 +239,53 @@ Qed.
 
 Theorem abs_eq : forall n, 0 <= n -> Z.abs n == n.
 Proof.
-intros. red. rewrite Z.spec_abs. apply Zabs_eq.
- rewrite <- Z.spec_0, <- spec_le; auto.
+intros n. red. rewrite spec_le, Z.spec_0, Z.spec_abs. apply Zabs_eq.
 Qed.
 
 Theorem abs_neq : forall n, n <= 0 -> Z.abs n == -n.
 Proof.
-intros. red. rewrite Z.spec_abs, Z.spec_opp. apply Zabs_non_eq.
- rewrite <- Z.spec_0, <- spec_le; auto.
+intros n. red. rewrite spec_le, Z.spec_0, Z.spec_abs, Z.spec_opp.
+ apply Zabs_non_eq.
 Qed.
 
 Theorem sgn_null : forall n, n==0 -> Z.sgn n == 0.
 Proof.
-intros. red. rewrite Z.spec_sgn, Z.spec_0. rewrite Zsgn_null.
- rewrite <- Z.spec_0; auto.
+intros n. unfold Z.eq. rewrite Z.spec_sgn, Z.spec_0. rewrite Zsgn_null; auto.
 Qed.
 
 Theorem sgn_pos : forall n, 0<n -> Z.sgn n == Z.succ 0.
 Proof.
-intros. red. rewrite Z.spec_sgn. zsimpl. rewrite Zsgn_pos.
- rewrite <- Z.spec_0, <- spec_lt; auto.
+intros n. red. rewrite spec_lt, Z.spec_sgn. zsimpl. rewrite Zsgn_pos; auto.
 Qed.
 
 Theorem sgn_neg : forall n, n<0 -> Z.sgn n == Z.opp (Z.succ 0).
 Proof.
-intros. red. rewrite Z.spec_sgn. zsimpl. rewrite Zsgn_neg.
- rewrite <- Z.spec_0, <- spec_lt; auto.
+intros n. red. rewrite spec_lt, Z.spec_sgn. zsimpl. rewrite Zsgn_neg; auto.
+Qed.
+
+Program Instance div_wd : Proper (Z.eq==>Z.eq==>Z.eq) Z.div.
+Program Instance mod_wd : Proper (Z.eq==>Z.eq==>Z.eq) Z.modulo.
+
+Theorem div_mod : forall a b, ~b==0 -> a == b*(Z.div a b) + (Z.modulo a b).
+Proof.
+intros a b. unfold Z.eq; zsimpl. intros.
+apply Z_div_mod_eq_full; auto.
+Qed.
+
+Theorem mod_pos_bound :
+ forall a b, 0 < b -> 0 <= Z.modulo a b /\ Z.modulo a b < b.
+Proof.
+intros a b. rewrite 2 spec_lt, spec_le, Z.spec_0. intros.
+rewrite Z.spec_modulo; auto with zarith.
+apply Z_mod_lt; auto with zarith.
+Qed.
+
+Theorem mod_neg_bound :
+ forall a b, b < 0 -> b < Z.modulo a b /\ Z.modulo a b <= 0.
+Proof.
+intros a b. rewrite 2 spec_lt, spec_le, Z.spec_0. intros.
+rewrite Z.spec_modulo; auto with zarith.
+apply Z_mod_neg; auto with zarith.
 Qed.
 
 (** Aliases *)
@@ -280,5 +305,7 @@ Definition min := Z.min.
 Definition max := Z.max.
 Definition abs := Z.abs.
 Definition sgn := Z.sgn.
+Definition div := Z.div.
+Definition modulo := Z.modulo.
 
 End ZSig_ZAxioms.
diff --git a/theories/Numbers/NatInt/NZDiv.v b/theories/Numbers/NatInt/NZDiv.v
index 4acd6540d..b189d5b29 100644
--- a/theories/Numbers/NatInt/NZDiv.v
+++ b/theories/Numbers/NatInt/NZDiv.v
@@ -13,7 +13,7 @@ Require Import NZAxioms NZMulOrder.
 (** The first signatures will be common to all divisions over NZ, N and Z *)
 
 Module Type DivMod (Import T:Typ).
- Parameters div modulo : t -> t -> t.
+ Parameters Inline div modulo : t -> t -> t.
 End DivMod.
 
 Module Type DivModNotation (T:Typ)(Import NZ:DivMod T).
diff --git a/theories/Numbers/Natural/BigN/BigN.v b/theories/Numbers/Natural/BigN/BigN.v
index bc2f3ecdf..b87056a63 100644
--- a/theories/Numbers/Natural/BigN/BigN.v
+++ b/theories/Numbers/Natural/BigN/BigN.v
@@ -15,12 +15,7 @@ Author: Arnaud Spiwack
 *)
 
 Require Export Int31.
-Require Import CyclicAxioms.
-Require Import Cyclic31.
-Require Import NSig.
-Require Import NSigNAxioms.
-Require Import NMake.
-Require Import NProperties.
+Require Import CyclicAxioms Cyclic31 NSig NSigNAxioms NMake NProperties NDiv.
 
 Module BigN <: NType := NMake.Make Int31Cyclic.
 
@@ -28,6 +23,7 @@ Module BigN <: NType := NMake.Make Int31Cyclic.
 
 Module Export BigNAxiomsMod := NSig_NAxioms BigN.
 Module Export BigNPropMod := NPropFunct BigNAxiomsMod.
+Module Export BigDivModProp := NDivPropFunct BigNAxiomsMod BigNPropMod.
 
 (** Notations about [BigN] *)
 
@@ -73,6 +69,7 @@ Infix "<=" := BigN.le : bigN_scope.
 Notation "x > y" := (BigN.lt y x)(only parsing) : bigN_scope.
 Notation "x >= y" := (BigN.le y x)(only parsing) : bigN_scope.
 Notation "[ i ]" := (BigN.to_Z i) : bigN_scope.
+Infix "mod" := modulo (at level 40, no associativity) : bigN_scope.
 
 Local Open Scope bigN_scope.
 
diff --git a/theories/Numbers/Natural/BigN/NMake_gen.ml b/theories/Numbers/Natural/BigN/NMake_gen.ml
index 769d804d7..b8e879c66 100644
--- a/theories/Numbers/Natural/BigN/NMake_gen.ml
+++ b/theories/Numbers/Natural/BigN/NMake_gen.ml
@@ -1956,6 +1956,7 @@ let _ =
   pr "";
 
   pr " Definition div_eucl x y :=";
+  pr "  if eq_bool y zero then (zero,zero) else";
   pr "  match compare x y with";
   pr "  | Eq => (one, zero)";
   pr "  | Lt => (zero, x)";
@@ -1964,7 +1965,6 @@ let _ =
   pr "";
 
   pr " Theorem spec_div_eucl: forall x y,";
-  pr "      0 < [y] ->";
   pr "      let (q,r) := div_eucl x y in";
   pr "      ([q], [r]) = Zdiv_eucl [x] [y].";
   pa " Admitted.";
@@ -1973,8 +1973,13 @@ let _ =
   pp "   exact (spec_0 w0_spec).";
   pp " assert (F1: [one] = 1).";
   pp "   exact (spec_1 w0_spec).";
-  pp " intros x y H; generalize (spec_compare x y);";
-  pp "   unfold div_eucl; case compare; try rewrite F0;";
+  pp " intros x y. unfold div_eucl.";
+  pp " generalize (spec_eq_bool y zero). destruct eq_bool; rewrite F0.";
+  pp " intro H. rewrite H. destruct [x]; auto.";
+  pp " intro H'.";
+  pp " assert (0 < [y]) by (generalize (spec_pos y); auto with zarith).";
+  pp " clear H'.";
+  pp " generalize (spec_compare x y); case compare; try rewrite F0;";
   pp "   try rewrite F1; intros; auto with zarith.";
   pp " rewrite H0; generalize (Z_div_same [y] (Zlt_gt _ _ H))";
   pp "                        (Z_mod_same [y] (Zlt_gt _ _ H));";
@@ -1994,10 +1999,10 @@ let _ =
   pr "";
 
   pr " Theorem spec_div:";
-  pr "   forall x y, 0 < [y] -> [div x y] = [x] / [y].";
+  pr "   forall x y, [div x y] = [x] / [y].";
   pa " Admitted.";
   pp " Proof.";
-  pp " intros x y H1; unfold div; generalize (spec_div_eucl x y H1);";
+  pp " intros x y; unfold div; generalize (spec_div_eucl x y);";
   pp "   case div_eucl; simpl fst.";
   pp " intros xx yy; unfold Zdiv; case Zdiv_eucl; intros qq rr H; ";
   pp "  injection H; auto.";
@@ -2099,6 +2104,7 @@ let _ =
   pr "";
 
   pr " Definition modulo x y := ";
+  pr "  if eq_bool y zero then zero else";
   pr "  match compare x y with";
   pr "  | Eq => zero";
   pr "  | Lt => x";
@@ -2107,15 +2113,20 @@ let _ =
   pr "";
 
   pr " Theorem spec_modulo:";
-  pr "   forall x y, 0 < [y] -> [modulo x y] = [x] mod [y].";
+  pr "   forall x y, [modulo x y] = [x] mod [y].";
   pa " Admitted.";
   pp " Proof.";
   pp " assert (F0: [zero] = 0).";
   pp "   exact (spec_0 w0_spec).";
   pp " assert (F1: [one] = 1).";
   pp "   exact (spec_1 w0_spec).";
-  pp " intros x y H; generalize (spec_compare x y);";
-  pp "   unfold modulo; case compare; try rewrite F0;";
+  pp " intros x y. unfold modulo.";
+  pp " generalize (spec_eq_bool y zero). destruct eq_bool; rewrite F0.";
+  pp " intro H; rewrite H. destruct [x]; auto.";
+  pp " intro H'.";
+  pp " assert (H : 0 < [y]) by (generalize (spec_pos y); auto with zarith).";
+  pp " clear H'.";
+  pp " generalize (spec_compare x y); case compare; try rewrite F0;";
   pp "   try rewrite F1; intros; try split; auto with zarith.";
   pp " rewrite H0; apply sym_equal; apply Z_mod_same; auto with zarith.";
   pp " apply sym_equal; apply Zmod_small; auto with zarith.";
diff --git a/theories/Numbers/Natural/SpecViaZ/NSig.v b/theories/Numbers/Natural/SpecViaZ/NSig.v
index 2dfa783aa..ecb49d32d 100644
--- a/theories/Numbers/Natural/SpecViaZ/NSig.v
+++ b/theories/Numbers/Natural/SpecViaZ/NSig.v
@@ -94,17 +94,15 @@ Module Type NType.
  Parameter div_eucl : t -> t -> t * t.
 
  Parameter spec_div_eucl: forall x y,
-      0 < [y] ->
-      let (q,r) := div_eucl x y in ([q], [r]) = Zdiv_eucl [x] [y].
+  let (q,r) := div_eucl x y in ([q], [r]) = Zdiv_eucl [x] [y].
 
  Parameter div : t -> t -> t.
 
- Parameter spec_div: forall x y, 0 < [y] -> [div x y] = [x] / [y].
+ Parameter spec_div: forall x y, [div x y] = [x] / [y].
 
  Parameter modulo : t -> t -> t.
 
- Parameter spec_modulo:
-   forall x y, 0 < [y] -> [modulo x y] = [x] mod [y].
+ Parameter spec_modulo: forall x y, [modulo x y] = [x] mod [y].
 
  Parameter gcd : t -> t -> t.
 
diff --git a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
index 66d3a89c2..8a34185d9 100644
--- a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
+++ b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
@@ -8,14 +8,11 @@
 
 (*i $Id$ i*)
 
-Require Import ZArith.
-Require Import Nnat.
-Require Import NAxioms.
-Require Import NSig.
+Require Import ZArith Nnat NAxioms NDiv NSig.
 
 (** * The interface [NSig.NType] implies the interface [NAxiomsSig] *)
 
-Module NSig_NAxioms (N:NType) <: NAxiomsSig.
+Module NSig_NAxioms (N:NType) <: NAxiomsSig <: NDivSig.
 
 Delimit Scope NumScope with Num.
 Bind Scope NumScope with N.t.
@@ -28,7 +25,8 @@ Local Infix "-" := N.sub : NumScope.
 Local Infix "*" := N.mul : NumScope.
 
 Hint Rewrite
- N.spec_0 N.spec_succ N.spec_add N.spec_mul N.spec_pred N.spec_sub : num.
+ N.spec_0 N.spec_succ N.spec_add N.spec_mul N.spec_pred N.spec_sub
+ N.spec_div N.spec_modulo : num.
 Ltac nsimpl := autorewrite with num.
 Ltac ncongruence := unfold N.eq; repeat red; intros; nsimpl; congruence.
 
@@ -212,6 +210,22 @@ Proof.
 red; nsimpl; auto.
 Qed.
 
+Program Instance div_wd : Proper (N.eq==>N.eq==>N.eq) N.div.
+Program Instance mod_wd : Proper (N.eq==>N.eq==>N.eq) N.modulo.
+
+Theorem div_mod : forall a b, ~b==0 -> a == b*(N.div a b) + (N.modulo a b).
+Proof.
+intros a b. unfold N.eq. nsimpl. intros.
+apply Z_div_mod_eq_full; auto.
+Qed.
+
+Theorem mod_upper_bound : forall a b, ~b==0 -> N.modulo a b < b.
+Proof.
+intros a b. unfold N.eq. rewrite spec_lt. nsimpl. intros.
+destruct (Z_mod_lt [a] [b]); auto.
+generalize (N.spec_pos b); auto with zarith.
+Qed.
+
 Definition recursion (A : Type) (a : A) (f : N.t -> A -> A) (n : N.t) :=
   Nrect (fun _ => A) a (fun n a => f (N.of_N n) a) (N.to_N n).
 Implicit Arguments recursion [A].
@@ -282,5 +296,7 @@ Definition lt := N.lt.
 Definition le := N.le.
 Definition min := N.min.
 Definition max := N.max.
+Definition div := N.div.
+Definition modulo := N.modulo.
 
 End NSig_NAxioms.