Remove non-DFSG contentsupstream/8.4_beta+dfsg

1 files changed, 0 insertions, 947 deletions

diff --git a/theories/ZArith/ZOdiv.v b/theories/ZArith/ZOdiv.v
deleted file mode 100644
index 70f6866e..00000000
--- a/theories/ZArith/ZOdiv.v
+++ /dev/null
@@ -1,947 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-
-Require Import BinPos BinNat Nnat ZArith_base ROmega ZArithRing.
-Require Export ZOdiv_def.
-Require Zdiv.
-
-Open Scope Z_scope.
-
-(** This file provides results about the Round-Toward-Zero Euclidean
-  division [ZOdiv_eucl], whose projections are [ZOdiv] and [ZOmod].
-  Definition of this division can be found in file [ZOdiv_def].
-
-  This division and the one defined in Zdiv agree only on positive
-  numbers. Otherwise, Zdiv performs Round-Toward-Bottom.
-
-  The current approach is compatible with the division of usual
-  programming languages such as Ocaml. In addition, it has nicer
-  properties with respect to opposite and other usual operations.
-*)
-
-(** Since ZOdiv and Zdiv are not meant to be used concurrently,
-   we reuse the same notation. *)
-
-Infix "/" := ZOdiv : Z_scope.
-Infix "mod" := ZOmod (at level 40, no associativity) : Z_scope.
-
-Infix "/" := Ndiv : N_scope.
-Infix "mod" := Nmod (at level 40, no associativity) : N_scope.
-
-(** Auxiliary results on the ad-hoc comparison [NPgeb]. *)
-
-Lemma NPgeb_Zge : forall (n:N)(p:positive),
-  NPgeb n p = true -> Z_of_N n >= Zpos p.
-Proof.
- destruct n as [|n]; simpl; intros.
- discriminate.
- red; simpl; destruct Pcompare; now auto.
-Qed.
-
-Lemma NPgeb_Zlt : forall (n:N)(p:positive),
-  NPgeb n p = false -> Z_of_N n < Zpos p.
-Proof.
- destruct n as [|n]; simpl; intros.
- red; auto.
- red; simpl; destruct Pcompare; now auto.
-Qed.
-
-(** * Relation between division on N and on Z. *)
-
-Lemma Ndiv_Z0div : forall a b:N,
-  Z_of_N (a/b) = (Z_of_N a / Z_of_N b).
-Proof.
-  intros.
-  destruct a; destruct b; simpl; auto.
-  unfold Ndiv, ZOdiv; simpl; destruct Pdiv_eucl; auto.
-Qed.
-
-Lemma Nmod_Z0mod : forall a b:N,
-  Z_of_N (a mod b) = (Z_of_N a) mod (Z_of_N b).
-Proof.
-  intros.
-  destruct a; destruct b; simpl; auto.
-  unfold Nmod, ZOmod; simpl; destruct Pdiv_eucl; auto.
-Qed.
-
-(** * Characterization of this euclidean division. *)
-
-(** First, the usual equation [a=q*b+r]. Notice that [a mod 0]
-   has been chosen to be [a], so this equation holds even for [b=0].
-*)
-
-Theorem N_div_mod_eq : forall a b,
-  a = (b * (Ndiv a b) + (Nmod a b))%N.
-Proof.
-  intros; generalize (Ndiv_eucl_correct a b).
-  unfold Ndiv, Nmod; destruct Ndiv_eucl; simpl.
-  intro H; rewrite H; rewrite Nmult_comm; auto.
-Qed.
-
-Theorem ZO_div_mod_eq : forall a b,
-  a = b * (ZOdiv a b) + (ZOmod a b).
-Proof.
-  intros; generalize (ZOdiv_eucl_correct a b).
-  unfold ZOdiv, ZOmod; destruct ZOdiv_eucl; simpl.
-  intro H; rewrite H; rewrite Zmult_comm; auto.
-Qed.
-
-(** Then, the inequalities constraining the remainder. *)
-
-Theorem Pdiv_eucl_remainder : forall a b:positive,
-  Z_of_N (snd (Pdiv_eucl a b)) < Zpos b.
-Proof.
-  induction a; cbv beta iota delta [Pdiv_eucl]; fold Pdiv_eucl; cbv zeta.
-  intros b; generalize (IHa b); case Pdiv_eucl.
-    intros q1 r1 Hr1; simpl in Hr1.
-    case_eq (NPgeb (2*r1+1) b); intros; unfold snd.
-    romega with *.
-    apply NPgeb_Zlt; auto.
-  intros b; generalize (IHa b); case Pdiv_eucl.
-    intros q1 r1 Hr1; simpl in Hr1.
-    case_eq (NPgeb (2*r1) b); intros; unfold snd.
-    romega with *.
-    apply NPgeb_Zlt; auto.
-  destruct b; simpl; romega with *.
-Qed.
-
-Theorem Nmod_lt : forall (a b:N), b<>0%N ->
-  (a mod b < b)%N.
-Proof.
-  destruct b as [ |b]; intro H; try solve [elim H;auto].
-  destruct a as [ |a]; try solve [compute;auto]; unfold Nmod, Ndiv_eucl.
-  generalize (Pdiv_eucl_remainder a b); destruct Pdiv_eucl; simpl.
-  romega with *.
-Qed.
-
-(** The remainder is bounded by the divisor, in term of absolute values *)
-
-Theorem ZOmod_lt : forall a b:Z, b<>0 ->
-  Zabs (a mod b) < Zabs b.
-Proof.
-  destruct b as [ |b|b]; intro H; try solve [elim H;auto];
-  destruct a as [ |a|a]; try solve [compute;auto]; unfold ZOmod, ZOdiv_eucl;
-  generalize (Pdiv_eucl_remainder a b); destruct Pdiv_eucl; simpl;
-  try rewrite Zabs_Zopp; rewrite Zabs_eq; auto; apply Z_of_N_le_0.
-Qed.
-
-(** The sign of the remainder is the one of [a]. Due to the possible
-   nullity of [a], a general result is to be stated in the following form:
-*)
-
-Theorem ZOmod_sgn : forall a b:Z,
-  0 <= Zsgn (a mod b) * Zsgn a.
-Proof.
-  destruct b as [ |b|b]; destruct a as [ |a|a]; simpl; auto with zarith;
-  unfold ZOmod, ZOdiv_eucl; destruct Pdiv_eucl;
-  simpl; destruct n0; simpl; auto with zarith.
-Qed.
-
-(** This can also be said in a simplier way: *)
-
-Theorem Zsgn_pos_iff : forall z, 0 <= Zsgn z <-> 0 <= z.
-Proof.
- destruct z; simpl; intuition auto with zarith.
-Qed.
-
-Theorem ZOmod_sgn2 : forall a b:Z,
-  0 <= (a mod b) * a.
-Proof.
-  intros; rewrite <-Zsgn_pos_iff, Zsgn_Zmult; apply ZOmod_sgn.
-Qed.
-
-(** Reformulation of [ZOdiv_lt] and [ZOmod_sgn] in 2
-  then 4 particular cases. *)
-
-Theorem ZOmod_lt_pos : forall a b:Z, 0<=a -> b<>0 ->
-  0 <= a mod b < Zabs b.
-Proof.
-  intros.
-  assert (0 <= a mod b).
-   generalize (ZOmod_sgn a b).
-   destruct (Zle_lt_or_eq 0 a H).
-   rewrite <- Zsgn_pos in H1; rewrite H1; romega with *.
-   subst a; simpl; auto.
-  generalize (ZOmod_lt a b H0); romega with *.
-Qed.
-
-Theorem ZOmod_lt_neg : forall a b:Z, a<=0 -> b<>0 ->
-  -Zabs b < a mod b <= 0.
-Proof.
-  intros.
-  assert (a mod b <= 0).
-   generalize (ZOmod_sgn a b).
-   destruct (Zle_lt_or_eq a 0 H).
-   rewrite <- Zsgn_neg in H1; rewrite H1; romega with *.
-   subst a; simpl; auto.
-  generalize (ZOmod_lt a b H0); romega with *.
-Qed.
-
-Theorem ZOmod_lt_pos_pos : forall a b:Z, 0<=a -> 0<b -> 0 <= a mod b < b.
-Proof.
-  intros; generalize (ZOmod_lt_pos a b); romega with *.
-Qed.
-
-Theorem ZOmod_lt_pos_neg : forall a b:Z, 0<=a -> b<0 -> 0 <= a mod b < -b.
-Proof.
-  intros; generalize (ZOmod_lt_pos a b); romega with *.
-Qed.
-
-Theorem ZOmod_lt_neg_pos : forall a b:Z, a<=0 -> 0<b -> -b < a mod b <= 0.
-Proof.
-  intros; generalize (ZOmod_lt_neg a b); romega with *.
-Qed.
-
-Theorem ZOmod_lt_neg_neg : forall a b:Z, a<=0 -> b<0 -> b < a mod b <= 0.
-Proof.
-  intros; generalize (ZOmod_lt_neg a b); romega with *.
-Qed.
-
-(** * Division and Opposite *)
-
-(* The precise equalities that are invalid with "historic" Zdiv. *)
-
-Theorem ZOdiv_opp_l : forall a b:Z, (-a)/b = -(a/b).
-Proof.
- destruct a; destruct b; simpl; auto;
-  unfold ZOdiv, ZOdiv_eucl; destruct Pdiv_eucl; simpl; auto with zarith.
-Qed.
-
-Theorem ZOdiv_opp_r : forall a b:Z, a/(-b) = -(a/b).
-Proof.
- destruct a; destruct b; simpl; auto;
-  unfold ZOdiv, ZOdiv_eucl; destruct Pdiv_eucl; simpl; auto with zarith.
-Qed.
-
-Theorem ZOmod_opp_l : forall a b:Z, (-a) mod b = -(a mod b).
-Proof.
- destruct a; destruct b; simpl; auto;
-  unfold ZOmod, ZOdiv_eucl; destruct Pdiv_eucl; simpl; auto with zarith.
-Qed.
-
-Theorem ZOmod_opp_r : forall a b:Z, a mod (-b) = a mod b.
-Proof.
- destruct a; destruct b; simpl; auto;
-  unfold ZOmod, ZOdiv_eucl; destruct Pdiv_eucl; simpl; auto with zarith.
-Qed.
-
-Theorem ZOdiv_opp_opp : forall a b:Z, (-a)/(-b) = a/b.
-Proof.
- destruct a; destruct b; simpl; auto;
-  unfold ZOdiv, ZOdiv_eucl; destruct Pdiv_eucl; simpl; auto with zarith.
-Qed.
-
-Theorem ZOmod_opp_opp : forall a b:Z, (-a) mod (-b) = -(a mod b).
-Proof.
- destruct a; destruct b; simpl; auto;
-  unfold ZOmod, ZOdiv_eucl; destruct Pdiv_eucl; simpl; auto with zarith.
-Qed.
-
-(** * Unicity results *)
-
-Definition Remainder a b r :=
-  (0 <= a /\ 0 <= r < Zabs b) \/ (a <= 0 /\ -Zabs b < r <= 0).
-
-Definition Remainder_alt a b r :=
-  Zabs r < Zabs b /\ 0 <= r * a.
-
-Lemma Remainder_equiv : forall a b r,
- Remainder a b r <-> Remainder_alt a b r.
-Proof.
-  unfold Remainder, Remainder_alt; intuition.
-  romega with *.
-  romega with *.
-  rewrite <-(Zmult_opp_opp).
-  apply Zmult_le_0_compat; romega.
-  assert (0 <= Zsgn r * Zsgn a) by (rewrite <-Zsgn_Zmult, Zsgn_pos_iff; auto).
-  destruct r; simpl Zsgn in *; romega with *.
-Qed.
-
-Theorem ZOdiv_mod_unique_full:
- forall a b q r, Remainder a b r ->
-   a = b*q + r -> q = a/b /\ r = a mod b.
-Proof.
-  destruct 1 as [(H,H0)|(H,H0)]; intros.
-  apply Zdiv.Zdiv_mod_unique with b; auto.
-  apply ZOmod_lt_pos; auto.
-  romega with *.
-  rewrite <- H1; apply ZO_div_mod_eq.
-
-  rewrite <- (Zopp_involutive a).
-  rewrite ZOdiv_opp_l, ZOmod_opp_l.
-  generalize (Zdiv.Zdiv_mod_unique b (-q) (-a/b) (-r) (-a mod b)).
-  generalize (ZOmod_lt_pos (-a) b).
-  rewrite <-ZO_div_mod_eq, <-Zopp_mult_distr_r, <-Zopp_plus_distr, <-H1.
-  romega with *.
-Qed.
-
-Theorem ZOdiv_unique_full:
- forall a b q r, Remainder a b r ->
-  a = b*q + r -> q = a/b.
-Proof.
- intros; destruct (ZOdiv_mod_unique_full a b q r); auto.
-Qed.
-
-Theorem ZOdiv_unique:
- forall a b q r, 0 <= a -> 0 <= r < b ->
-   a = b*q + r -> q = a/b.
-Proof.
-  intros; eapply ZOdiv_unique_full; eauto.
-  red; romega with *.
-Qed.
-
-Theorem ZOmod_unique_full:
- forall a b q r, Remainder a b r ->
-  a = b*q + r -> r = a mod b.
-Proof.
- intros; destruct (ZOdiv_mod_unique_full a b q r); auto.
-Qed.
-
-Theorem ZOmod_unique:
- forall a b q r, 0 <= a -> 0 <= r < b ->
-   a = b*q + r -> r = a mod b.
-Proof.
-  intros; eapply ZOmod_unique_full; eauto.
-  red; romega with *.
-Qed.
-
-(** * Basic values of divisions and modulo. *)
-
-Lemma ZOmod_0_l: forall a, 0 mod a = 0.
-Proof.
-  destruct a; simpl; auto.
-Qed.
-
-Lemma ZOmod_0_r: forall a, a mod 0 = a.
-Proof.
-  destruct a; simpl; auto.
-Qed.
-
-Lemma ZOdiv_0_l: forall a, 0/a = 0.
-Proof.
-  destruct a; simpl; auto.
-Qed.
-
-Lemma ZOdiv_0_r: forall a, a/0 = 0.
-Proof.
-  destruct a; simpl; auto.
-Qed.
-
-Lemma ZOmod_1_r: forall a, a mod 1 = 0.
-Proof.
-  intros; symmetry; apply ZOmod_unique_full with a; auto with zarith.
-  rewrite Remainder_equiv; red; simpl; auto with zarith.
-Qed.
-
-Lemma ZOdiv_1_r: forall a, a/1 = a.
-Proof.
-  intros; symmetry; apply ZOdiv_unique_full with 0; auto with zarith.
-  rewrite Remainder_equiv; red; simpl; auto with zarith.
-Qed.
-
-Hint Resolve ZOmod_0_l ZOmod_0_r ZOdiv_0_l ZOdiv_0_r ZOdiv_1_r ZOmod_1_r
- : zarith.
-
-Lemma ZOdiv_1_l: forall a, 1 < a -> 1/a = 0.
-Proof.
-  intros; symmetry; apply ZOdiv_unique with 1; auto with zarith.
-Qed.
-
-Lemma ZOmod_1_l: forall a, 1 < a ->  1 mod a = 1.
-Proof.
-  intros; symmetry; apply ZOmod_unique with 0; auto with zarith.
-Qed.
-
-Lemma ZO_div_same : forall a:Z, a<>0 -> a/a = 1.
-Proof.
-  intros; symmetry; apply ZOdiv_unique_full with 0; auto with *.
-  rewrite Remainder_equiv; red; simpl; romega with *.
-Qed.
-
-Lemma ZO_mod_same : forall a, a mod a = 0.
-Proof.
-  destruct a; intros; symmetry.
-  compute; auto.
-  apply ZOmod_unique with 1; auto with *; romega with *.
-  apply ZOmod_unique_full with 1; auto with *; red; romega with *.
-Qed.
-
-Lemma ZO_mod_mult : forall a b, (a*b) mod b = 0.
-Proof.
-  intros a b; destruct (Z_eq_dec b 0) as [Hb|Hb].
-  subst; simpl; rewrite ZOmod_0_r; auto with zarith.
-  symmetry; apply ZOmod_unique_full with a; [ red; romega with * | ring ].
-Qed.
-
-Lemma ZO_div_mult : forall a b:Z, b <> 0 -> (a*b)/b = a.
-Proof.
-  intros; symmetry; apply ZOdiv_unique_full with 0; auto with zarith;
-   [ red; romega with * | ring].
-Qed.
-
-(** * Order results about ZOmod and ZOdiv *)
-
-(* Division of positive numbers is positive. *)
-
-Lemma ZO_div_pos: forall a b, 0 <= a -> 0 <= b -> 0 <= a/b.
-Proof.
-  intros.
-  destruct (Zle_lt_or_eq 0 b H0).
-  assert (H2:=ZOmod_lt_pos_pos a b H H1).
-  rewrite (ZO_div_mod_eq a b) in H.
-  destruct (Z_lt_le_dec (a/b) 0); auto.
-  assert (b*(a/b) <= -b).
-   replace (-b) with (b*-1); [ | ring].
-   apply Zmult_le_compat_l; auto with zarith.
-  romega.
-  subst b; rewrite ZOdiv_0_r; auto.
-Qed.
-
-(** As soon as the divisor is greater or equal than 2,
-    the division is strictly decreasing. *)
-
-Lemma ZO_div_lt : forall a b:Z, 0 < a -> 2 <= b -> a/b < a.
-Proof.
-  intros.
-  assert (Hb : 0 < b) by romega.
-  assert (H1 : 0 <= a/b) by (apply ZO_div_pos; auto with zarith).
-  assert (H2 : 0 <= a mod b < b) by (apply ZOmod_lt_pos_pos; auto with zarith).
-  destruct (Zle_lt_or_eq 0 (a/b) H1) as [H3|H3]; [ | rewrite <- H3; auto].
-  pattern a at 2; rewrite (ZO_div_mod_eq a b).
-  apply Zlt_le_trans with (2*(a/b)).
-  romega.
-  apply Zle_trans with (b*(a/b)).
-  apply Zmult_le_compat_r; auto.
-  romega.
-Qed.
-
-(** A division of a small number by a bigger one yields zero. *)
-
-Theorem ZOdiv_small: forall a b, 0 <= a < b -> a/b = 0.
-Proof.
-  intros a b H; apply sym_equal; apply ZOdiv_unique with a; auto with zarith.
-Qed.
-
-(** Same situation, in term of modulo: *)
-
-Theorem ZOmod_small: forall a n, 0 <= a < n -> a mod n = a.
-Proof.
-  intros a b H; apply sym_equal; apply ZOmod_unique with 0; auto with zarith.
-Qed.
-
-(** [Zge] is compatible with a positive division. *)
-
-Lemma ZO_div_monotone_pos : forall a b c:Z, 0<=c -> 0<=a<=b -> a/c <= b/c.
-Proof.
-  intros.
-  destruct H0.
-  destruct (Zle_lt_or_eq 0 c H);
-   [ clear H | subst c; do 2 rewrite ZOdiv_0_r; auto].
-  generalize (ZO_div_mod_eq a c).
-  generalize (ZOmod_lt_pos_pos a c H0 H2).
-  generalize (ZO_div_mod_eq b c).
-  generalize (ZOmod_lt_pos_pos b c (Zle_trans _ _ _ H0 H1) H2).
-  intros.
-  elim (Z_le_gt_dec (a / c) (b / c)); auto with zarith.
-  intro.
-  absurd (a - b >= 1).
-  omega.
-  replace (a-b) with (c * (a/c-b/c) + a mod c - b mod c) by
-    (symmetry; pattern a at 1; rewrite H5; pattern b at 1; rewrite H3; ring).
-  assert (c * (a / c - b / c) >= c * 1).
-  apply Zmult_ge_compat_l.
-  omega.
-  omega.
-  assert (c * 1 = c).
-  ring.
-  omega.
-Qed.
-
-Lemma ZO_div_monotone : forall a b c, 0<=c -> a<=b -> a/c <= b/c.
-Proof.
-  intros.
-  destruct (Z_le_gt_dec 0 a).
-  apply ZO_div_monotone_pos; auto with zarith.
-  destruct (Z_le_gt_dec 0 b).
-  apply Zle_trans with 0.
-  apply Zle_left_rev.
-  simpl.
-  rewrite <- ZOdiv_opp_l.
-  apply ZO_div_pos; auto with zarith.
-  apply ZO_div_pos; auto with zarith.
-  rewrite <-(Zopp_involutive a), (ZOdiv_opp_l (-a)).
-  rewrite <-(Zopp_involutive b), (ZOdiv_opp_l (-b)).
-  generalize (ZO_div_monotone_pos (-b) (-a) c H).
-  romega.
-Qed.
-
-(** With our choice of division, rounding of (a/b) is always done toward zero: *)
-
-Lemma ZO_mult_div_le : forall a b:Z, 0 <= a -> 0 <= b*(a/b) <= a.
-Proof.
-  intros a b Ha.
-  destruct b as [ |b|b].
-  simpl; auto with zarith.
-  split.
-  apply Zmult_le_0_compat; auto with zarith.
-  apply ZO_div_pos; auto with zarith.
-  generalize (ZO_div_mod_eq a (Zpos b)) (ZOmod_lt_pos_pos a (Zpos b) Ha); romega with *.
-  change (Zneg b) with (-Zpos b); rewrite ZOdiv_opp_r, Zmult_opp_opp.
-  split.
-  apply Zmult_le_0_compat; auto with zarith.
-  apply ZO_div_pos; auto with zarith.
-  generalize (ZO_div_mod_eq a (Zpos b)) (ZOmod_lt_pos_pos a (Zpos b) Ha); romega with *.
-Qed.
-
-Lemma ZO_mult_div_ge : forall a b:Z, a <= 0 -> a <= b*(a/b) <= 0.
-Proof.
-  intros a b Ha.
-  destruct b as [ |b|b].
-  simpl; auto with zarith.
-  split.
-  generalize (ZO_div_mod_eq a (Zpos b)) (ZOmod_lt_neg_pos a (Zpos b) Ha); romega with *.
-  apply Zle_left_rev; unfold Zplus.
-  rewrite Zopp_mult_distr_r, <-ZOdiv_opp_l.
-  apply Zmult_le_0_compat; auto with zarith.
-  apply ZO_div_pos; auto with zarith.
-  change (Zneg b) with (-Zpos b); rewrite ZOdiv_opp_r, Zmult_opp_opp.
-  split.
-  generalize (ZO_div_mod_eq a (Zpos b)) (ZOmod_lt_neg_pos a (Zpos b) Ha); romega with *.
-  apply Zle_left_rev; unfold Zplus.
-  rewrite Zopp_mult_distr_r, <-ZOdiv_opp_l.
-  apply Zmult_le_0_compat; auto with zarith.
-  apply ZO_div_pos; auto with zarith.
-Qed.
-
-(** The previous inequalities between [b*(a/b)] and [a] are exact
-    iff the modulo is zero. *)
-
-Lemma ZO_div_exact_full_1 : forall a b:Z, a = b*(a/b) -> a mod b = 0.
-Proof.
-  intros; generalize (ZO_div_mod_eq a b); romega.
-Qed.
-
-Lemma ZO_div_exact_full_2 : forall a b:Z, a mod b = 0 -> a = b*(a/b).
-Proof.
-  intros; generalize (ZO_div_mod_eq a b); romega.
-Qed.
-
-(** A modulo cannot grow beyond its starting point. *)
-
-Theorem ZOmod_le: forall a b, 0 <= a -> 0 <= b -> a mod b <= a.
-Proof.
-  intros a b H1 H2.
-  destruct (Zle_lt_or_eq _ _ H2).
-  case (Zle_or_lt b a); intros H3.
-  case (ZOmod_lt_pos_pos a b); auto with zarith.
-  rewrite ZOmod_small; auto with zarith.
-  subst; rewrite ZOmod_0_r; auto with zarith.
-Qed.
-
-(** Some additionnal inequalities about Zdiv. *)
-
-Theorem ZOdiv_le_upper_bound:
-  forall a b q, 0 < b -> a <= q*b -> a/b <= q.
-Proof.
-  intros.
-  rewrite <- (ZO_div_mult q b); auto with zarith.
-  apply ZO_div_monotone; auto with zarith.
-Qed.
-
-Theorem ZOdiv_lt_upper_bound:
-  forall a b q, 0 <= a -> 0 < b -> a < q*b -> a/b < q.
-Proof.
-  intros a b q H1 H2 H3.
-  apply Zmult_lt_reg_r with b; auto with zarith.
-  apply Zle_lt_trans with (2 := H3).
-  pattern a at 2; rewrite (ZO_div_mod_eq a b); auto with zarith.
-  rewrite (Zmult_comm b); case (ZOmod_lt_pos_pos a b); auto with zarith.
-Qed.
-
-Theorem ZOdiv_le_lower_bound:
-  forall a b q, 0 < b -> q*b <= a -> q <= a/b.
-Proof.
-  intros.
-  rewrite <- (ZO_div_mult q b); auto with zarith.
-  apply ZO_div_monotone; auto with zarith.
-Qed.
-
-Theorem ZOdiv_sgn: forall a b,
-  0 <= Zsgn (a/b) * Zsgn a * Zsgn b.
-Proof.
-  destruct a as [ |a|a]; destruct b as [ |b|b]; simpl; auto with zarith;
-  unfold ZOdiv; simpl; destruct Pdiv_eucl; simpl; destruct n; simpl; auto with zarith.
-Qed.
-
-(** * Relations between usual operations and Zmod and Zdiv *)
-
-(** First, a result that used to be always valid with Zdiv,
-    but must be restricted here.
-    For instance, now (9+(-5)*2) mod 2 = -1 <> 1 = 9 mod 2 *)
-
-Lemma ZO_mod_plus : forall a b c:Z,
- 0 <= (a+b*c) * a ->
- (a + b * c) mod c = a mod c.
-Proof.
-  intros; destruct (Z_eq_dec a 0) as [Ha|Ha].
-  subst; simpl; rewrite ZOmod_0_l; apply ZO_mod_mult.
-  intros; destruct (Z_eq_dec c 0) as [Hc|Hc].
-  subst; do 2 rewrite ZOmod_0_r; romega.
-  symmetry; apply ZOmod_unique_full with (a/c+b); auto with zarith.
-  rewrite Remainder_equiv; split.
-  apply ZOmod_lt; auto.
-  apply Zmult_le_0_reg_r with (a*a); eauto.
-  destruct a; simpl; auto with zarith.
-  replace ((a mod c)*(a+b*c)*(a*a)) with (((a mod c)*a)*((a+b*c)*a)) by ring.
-  apply Zmult_le_0_compat; auto.
-  apply ZOmod_sgn2.
-  rewrite Zmult_plus_distr_r, Zmult_comm.
-  generalize (ZO_div_mod_eq a c); romega.
-Qed.
-
-Lemma ZO_div_plus : forall a b c:Z,
- 0 <= (a+b*c) * a -> c<>0 ->
- (a + b * c) / c = a / c + b.
-Proof.
-  intros; destruct (Z_eq_dec a 0) as [Ha|Ha].
-  subst; simpl; apply ZO_div_mult; auto.
-  symmetry.
-  apply ZOdiv_unique_full with (a mod c); auto with zarith.
-  rewrite Remainder_equiv; split.
-  apply ZOmod_lt; auto.
-  apply Zmult_le_0_reg_r with (a*a); eauto.
-  destruct a; simpl; auto with zarith.
-  replace ((a mod c)*(a+b*c)*(a*a)) with (((a mod c)*a)*((a+b*c)*a)) by ring.
-  apply Zmult_le_0_compat; auto.
-  apply ZOmod_sgn2.
-  rewrite Zmult_plus_distr_r, Zmult_comm.
-  generalize (ZO_div_mod_eq a c); romega.
-Qed.
-
-Theorem ZO_div_plus_l: forall a b c : Z,
- 0 <= (a*b+c)*c -> b<>0 ->
- b<>0 -> (a * b + c) / b = a + c / b.
-Proof.
-  intros a b c; rewrite Zplus_comm; intros; rewrite ZO_div_plus;
-  try apply Zplus_comm; auto with zarith.
-Qed.
-
-(** Cancellations. *)
-
-Lemma ZOdiv_mult_cancel_r : forall a b c:Z,
- c<>0 -> (a*c)/(b*c) = a/b.
-Proof.
- intros a b c Hc.
- destruct (Z_eq_dec b 0).
- subst; simpl; do 2 rewrite ZOdiv_0_r; auto.
- symmetry.
- apply ZOdiv_unique_full with ((a mod b)*c); auto with zarith.
- rewrite Remainder_equiv.
- split.
- do 2 rewrite Zabs_Zmult.
- apply Zmult_lt_compat_r.
- romega with *.
- apply ZOmod_lt; auto.
- replace ((a mod b)*c*(a*c)) with (((a mod b)*a)*(c*c)) by ring.
- apply Zmult_le_0_compat.
- apply ZOmod_sgn2.
- destruct c; simpl; auto with zarith.
- pattern a at 1; rewrite (ZO_div_mod_eq a b); ring.
-Qed.
-
-Lemma ZOdiv_mult_cancel_l : forall a b c:Z,
- c<>0 -> (c*a)/(c*b) = a/b.
-Proof.
-  intros.
-  rewrite (Zmult_comm c a); rewrite (Zmult_comm c b).
-  apply ZOdiv_mult_cancel_r; auto.
-Qed.
-
-Lemma ZOmult_mod_distr_l: forall a b c,
-  (c*a) mod (c*b) = c * (a mod b).
-Proof.
-  intros; destruct (Z_eq_dec c 0) as [Hc|Hc].
-  subst; simpl; rewrite ZOmod_0_r; auto.
-  destruct (Z_eq_dec b 0) as [Hb|Hb].
-  subst; repeat rewrite Zmult_0_r || rewrite ZOmod_0_r; auto.
-  assert (c*b <> 0).
-   contradict Hc; eapply Zmult_integral_l; eauto.
-  rewrite (Zplus_minus_eq _ _ _ (ZO_div_mod_eq (c*a) (c*b))).
-  rewrite (Zplus_minus_eq _ _ _ (ZO_div_mod_eq a b)).
-  rewrite ZOdiv_mult_cancel_l; auto with zarith.
-  ring.
-Qed.
-
-Lemma ZOmult_mod_distr_r: forall a b c,
-  (a*c) mod (b*c) = (a mod b) * c.
-Proof.
-  intros; repeat rewrite (fun x => (Zmult_comm x c)).
-  apply ZOmult_mod_distr_l; auto.
-Qed.
-
-(** Operations modulo. *)
-
-Theorem ZOmod_mod: forall a n, (a mod n) mod n = a mod n.
-Proof.
-  intros.
-  generalize (ZOmod_sgn2 a n).
-  pattern a at 2 4; rewrite (ZO_div_mod_eq a n); auto with zarith.
-  rewrite Zplus_comm; rewrite (Zmult_comm n).
-  intros.
-  apply sym_equal; apply ZO_mod_plus; auto with zarith.
-  rewrite Zmult_comm; auto.
-Qed.
-
-Theorem ZOmult_mod: forall a b n,
- (a * b) mod n = ((a mod n) * (b mod n)) mod n.
-Proof.
-  intros.
-  generalize (Zmult_le_0_compat _ _ (ZOmod_sgn2 a n) (ZOmod_sgn2 b n)).
-  pattern a at 2 3; rewrite (ZO_div_mod_eq a n); auto with zarith.
-  pattern b at 2 3; rewrite (ZO_div_mod_eq b n); auto with zarith.
-  set (A:=a mod n); set (B:=b mod n); set (A':=a/n); set (B':=b/n).
-  replace (A*(n*A'+A)*(B*(n*B'+B))) with (((n*A' + A) * (n*B' + B))*(A*B))
-   by ring.
-  replace ((n*A' + A) * (n*B' + B))
-   with (A*B + (A'*B+B'*A+n*A'*B')*n) by ring.
-  intros.
-  apply ZO_mod_plus; auto with zarith.
-Qed.
-
-(** addition and modulo
-
-  Generally speaking, unlike with Zdiv, we don't have
-       (a+b) mod n = (a mod n + b mod n) mod n
-  for any a and b.
-  For instance, take (8 + (-10)) mod 3 = -2 whereas
-  (8 mod 3 + (-10 mod 3)) mod 3 = 1. *)
-
-Theorem ZOplus_mod: forall a b n,
- 0 <= a * b ->
- (a + b) mod n = (a mod n + b mod n) mod n.
-Proof.
-  assert (forall a b n, 0<a -> 0<b ->
-           (a + b) mod n = (a mod n + b mod n) mod n).
-  intros a b n Ha Hb.
-  assert (H : 0<=a+b) by (romega with * ); revert H.
-  pattern a at 1 2; rewrite (ZO_div_mod_eq a n); auto with zarith.
-  pattern b at 1 2; rewrite (ZO_div_mod_eq b n); auto with zarith.
-  replace ((n * (a / n) + a mod n) + (n * (b / n) + b mod n))
-     with ((a mod n + b mod n) + (a / n + b / n) * n) by ring.
-  intros.
-  apply ZO_mod_plus; auto with zarith.
-  apply Zmult_le_0_compat; auto with zarith.
-  apply Zplus_le_0_compat.
-  apply Zmult_le_reg_r with a; auto with zarith.
-  simpl; apply ZOmod_sgn2; auto.
-  apply Zmult_le_reg_r with b; auto with zarith.
-  simpl; apply ZOmod_sgn2; auto.
-  (* general situation *)
-  intros a b n Hab.
-  destruct (Z_eq_dec a 0).
-  subst; simpl; symmetry; apply ZOmod_mod.
-  destruct (Z_eq_dec b 0).
-  subst; simpl; do 2 rewrite Zplus_0_r; symmetry; apply ZOmod_mod.
-  assert (0<a /\ 0<b \/ a<0 /\ b<0).
-   destruct a; destruct b; simpl in *; intuition; romega with *.
-  destruct H0.
-  apply H; intuition.
-  rewrite <-(Zopp_involutive a), <-(Zopp_involutive b).
-  rewrite <- Zopp_plus_distr; rewrite ZOmod_opp_l.
-  rewrite (ZOmod_opp_l (-a)),(ZOmod_opp_l (-b)).
-  match goal with |- _ = (-?x+-?y) mod n =>
-   rewrite <-(Zopp_plus_distr x y), ZOmod_opp_l end.
-  f_equal; apply H; auto with zarith.
-Qed.
-
-Lemma ZOplus_mod_idemp_l: forall a b n,
- 0 <= a * b ->
- (a mod n + b) mod n = (a + b) mod n.
-Proof.
-  intros.
-  rewrite ZOplus_mod.
-  rewrite ZOmod_mod.
-  symmetry.
-  apply ZOplus_mod; auto.
-  destruct (Z_eq_dec a 0).
-  subst; rewrite ZOmod_0_l; auto.
-  destruct (Z_eq_dec b 0).
-  subst; rewrite Zmult_0_r; auto with zarith.
-  apply Zmult_le_reg_r with (a*b).
-  assert (a*b <> 0).
-   intro Hab.
-   rewrite (Zmult_integral_l _ _ n1 Hab) in n0; auto with zarith.
-  auto with zarith.
-  simpl.
-  replace (a mod n * b * (a*b)) with ((a mod n * a)*(b*b)) by ring.
-  apply Zmult_le_0_compat.
-  apply ZOmod_sgn2.
-  destruct b; simpl; auto with zarith.
-Qed.
-
-Lemma ZOplus_mod_idemp_r: forall a b n,
- 0 <= a*b ->
- (b + a mod n) mod n = (b + a) mod n.
-Proof.
-  intros.
-  rewrite Zplus_comm, (Zplus_comm b a).
-  apply ZOplus_mod_idemp_l; auto.
-Qed.
-
-Lemma ZOmult_mod_idemp_l: forall a b n, (a mod n * b) mod n = (a * b) mod n.
-Proof.
-  intros; rewrite ZOmult_mod, ZOmod_mod, <- ZOmult_mod; auto.
-Qed.
-
-Lemma ZOmult_mod_idemp_r: forall a b n, (b * (a mod n)) mod n = (b * a) mod n.
-Proof.
-  intros; rewrite ZOmult_mod, ZOmod_mod, <- ZOmult_mod; auto.
-Qed.
-
-(** Unlike with Zdiv, the following result is true without restrictions. *)
-
-Lemma ZOdiv_ZOdiv : forall a b c, (a/b)/c = a/(b*c).
-Proof.
-  (* particular case: a, b, c positive *)
-  assert (forall a b c, a>0 -> b>0 -> c>0 -> (a/b)/c = a/(b*c)).
-   intros a b c H H0 H1.
-   pattern a at 2;rewrite (ZO_div_mod_eq a b).
-   pattern (a/b) at 2;rewrite (ZO_div_mod_eq (a/b) c).
-   replace (b * (c * (a / b / c) + (a / b) mod c) + a mod b) with
-    ((a / b / c)*(b * c)  + (b * ((a / b) mod c) + a mod b)) by ring.
-   assert (b*c<>0).
-    intro H2;
-    assert (H3: c <> 0) by auto with zarith;
-    rewrite (Zmult_integral_l _ _ H3 H2) in H0; auto with zarith.
-   assert (0<=a/b) by (apply (ZO_div_pos a b); auto with zarith).
-   assert (0<=a mod b < b) by (apply ZOmod_lt_pos_pos; auto with zarith).
-   assert (0<=(a/b) mod c < c) by
-    (apply ZOmod_lt_pos_pos; auto with zarith).
-   rewrite ZO_div_plus_l; auto with zarith.
-   rewrite (ZOdiv_small (b * ((a / b) mod c) + a mod b)).
-   ring.
-   split.
-   apply Zplus_le_0_compat;auto with zarith.
-   apply Zle_lt_trans with (b * ((a / b) mod c) + (b-1)).
-   apply Zplus_le_compat;auto with zarith.
-   apply Zle_lt_trans with (b * (c-1) + (b - 1)).
-   apply Zplus_le_compat;auto with zarith.
-   replace (b * (c - 1) + (b - 1)) with (b*c-1);try ring;auto with zarith.
-   repeat (apply Zmult_le_0_compat || apply Zplus_le_0_compat); auto with zarith.
-   apply (ZO_div_pos (a/b) c); auto with zarith.
-  (* b c positive, a general *)
-  assert (forall a b c, b>0 -> c>0 -> (a/b)/c = a/(b*c)).
-   intros; destruct a as [ |a|a]; try reflexivity.
-   apply H; auto with zarith.
-   change (Zneg a) with (-Zpos a); repeat rewrite ZOdiv_opp_l.
-   f_equal; apply H; auto with zarith.
-  (* c positive, a b general *)
-  assert (forall a b c, c>0 -> (a/b)/c = a/(b*c)).
-   intros; destruct b as [ |b|b].
-   repeat rewrite ZOdiv_0_r; reflexivity.
-   apply H0; auto with zarith.
-   change (Zneg b) with (-Zpos b);
-   repeat (rewrite ZOdiv_opp_r || rewrite ZOdiv_opp_l || rewrite <- Zopp_mult_distr_l).
-   f_equal; apply H0; auto with zarith.
-  (* a b c general *)
-  intros; destruct c as [ |c|c].
-  rewrite Zmult_0_r; repeat rewrite ZOdiv_0_r; reflexivity.
-  apply H1; auto with zarith.
-  change (Zneg c) with (-Zpos c);
-  rewrite <- Zopp_mult_distr_r; do 2 rewrite ZOdiv_opp_r.
-  f_equal; apply H1; auto with zarith.
-Qed.
-
-(** A last inequality: *)
-
-Theorem ZOdiv_mult_le:
- forall a b c, 0<=a -> 0<=b -> 0<=c -> c*(a/b) <= (c*a)/b.
-Proof.
-  intros a b c Ha Hb Hc.
-  destruct (Zle_lt_or_eq _ _ Ha);
-   [ | subst; rewrite ZOdiv_0_l, Zmult_0_r, ZOdiv_0_l; auto].
-  destruct (Zle_lt_or_eq _ _ Hb);
-   [ | subst; rewrite ZOdiv_0_r, ZOdiv_0_r, Zmult_0_r; auto].
-  destruct (Zle_lt_or_eq _ _ Hc);
-   [ | subst; rewrite ZOdiv_0_l; auto].
-  case (ZOmod_lt_pos_pos a b); auto with zarith; intros Hu1 Hu2.
-  case (ZOmod_lt_pos_pos c b); auto with zarith; intros Hv1 Hv2.
-  apply Zmult_le_reg_r with b; auto with zarith.
-  rewrite <- Zmult_assoc.
-  replace (a / b * b) with (a - a mod b).
-  replace (c * a / b * b) with (c * a - (c * a) mod b).
-  rewrite Zmult_minus_distr_l.
-  unfold Zminus; apply Zplus_le_compat_l.
-  match goal with |- - ?X <= -?Y => assert (Y <= X); auto with zarith end.
-  apply Zle_trans with ((c mod b) * (a mod b)); auto with zarith.
-  rewrite ZOmult_mod; auto with zarith.
-  apply (ZOmod_le ((c mod b) * (a mod b)) b); auto with zarith.
-  apply Zmult_le_compat_r; auto with zarith.
-  apply (ZOmod_le c b); auto.
-  pattern (c * a) at 1; rewrite (ZO_div_mod_eq (c * a) b); try ring;
-    auto with zarith.
-  pattern a at 1; rewrite (ZO_div_mod_eq a b); try ring; auto with zarith.
-Qed.
-
-(** ZOmod is related to divisibility (see more in Znumtheory) *)
-
-Lemma ZOmod_divides : forall a b,
- a mod b = 0 <-> exists c, a = b*c.
-Proof.
- split; intros.
- exists (a/b).
- pattern a at 1; rewrite (ZO_div_mod_eq a b).
- rewrite H; auto with zarith.
- destruct H as [c Hc].
- destruct (Z_eq_dec b 0).
- subst b; simpl in *; subst a; auto.
- symmetry.
- apply ZOmod_unique_full with c; auto with zarith.
- red; romega with *.
-Qed.
-
-(** * Interaction with "historic" Zdiv *)
-
-(** They agree at least on positive numbers: *)
-
-Theorem ZOdiv_eucl_Zdiv_eucl_pos : forall a b:Z, 0 <= a -> 0 < b ->
-  a/b = Zdiv.Zdiv a b /\ a mod b = Zdiv.Zmod a b.
-Proof.
-  intros.
-  apply Zdiv.Zdiv_mod_unique with b.
-  apply ZOmod_lt_pos; auto with zarith.
-  rewrite Zabs_eq; auto with *; apply Zdiv.Z_mod_lt; auto with *.
-  rewrite <- Zdiv.Z_div_mod_eq; auto with *.
-  symmetry; apply ZO_div_mod_eq; auto with *.
-Qed.
-
-Theorem ZOdiv_Zdiv_pos : forall a b, 0 <= a -> 0 <= b ->
-  a/b = Zdiv.Zdiv a b.
-Proof.
- intros a b Ha Hb.
- destruct (Zle_lt_or_eq _ _ Hb).
- generalize (ZOdiv_eucl_Zdiv_eucl_pos a b Ha H); intuition.
- subst; rewrite ZOdiv_0_r, Zdiv.Zdiv_0_r; reflexivity.
-Qed.
-
-Theorem ZOmod_Zmod_pos : forall a b, 0 <= a -> 0 < b ->
-  a mod b = Zdiv.Zmod a b.
-Proof.
- intros a b Ha Hb; generalize (ZOdiv_eucl_Zdiv_eucl_pos a b Ha Hb);
- intuition.
-Qed.
-
-(** Modulos are null at the same places *)
-
-Theorem ZOmod_Zmod_zero : forall a b, b<>0 ->
- (a mod b = 0 <-> Zdiv.Zmod a b = 0).
-Proof.
- intros.
- rewrite ZOmod_divides, Zdiv.Zmod_divides; intuition.
-Qed.