Some more cleanups (Zeven, auxiliary, Zbool, Zmisc, ZArith_base)

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

5 files changed, 238 insertions, 328 deletions

diff --git a/theories/ZArith/ZArith_base.v b/theories/ZArith/ZArith_base.v
index 05df86880..8eeca3b9a 100644
--- a/theories/ZArith/ZArith_base.v
+++ b/theories/ZArith/ZArith_base.v
@@ -28,8 +28,8 @@ Require Export Zbool.
 Require Export Zmisc.
 Require Export Wf_Z.
 
-Hint Resolve Zle_refl Zplus_comm Zplus_assoc Zmult_comm Zmult_assoc Zplus_0_l
-  Zplus_0_r Zmult_1_l Zplus_opp_l Zplus_opp_r Zmult_plus_distr_l
-  Zmult_plus_distr_r: zarith.
+Hint Resolve Z.le_refl Z.add_comm Z.add_assoc Z.mul_comm Z.mul_assoc Z.add_0_l
+  Z.add_0_r Z.mul_1_l Z.add_opp_diag_l Z.add_opp_diag_r Z.mul_add_distr_l
+  Z.mul_add_distr_r: zarith.
 
 Require Export Zhints.
diff --git a/theories/ZArith/Zbool.v b/theories/ZArith/Zbool.v
index d91843aef..d09012820 100644
--- a/theories/ZArith/Zbool.v
+++ b/theories/ZArith/Zbool.v
@@ -38,6 +38,9 @@ Notation Zge_bool := Z.geb (only parsing).
 Notation Zlt_bool := Z.ltb (only parsing).
 Notation Zgt_bool := Z.gtb (only parsing).
 
+(** We now provide a direct [Z.eqb] that doesn't refer to [Z.compare].
+   The old [Zeq_bool] is kept for compatibility. *)
+
 Definition Zeq_bool (x y:Z) :=
   match x ?= y with
     | Eq => true
@@ -52,162 +55,130 @@ Definition Zneq_bool (x y:Z) :=
 
 (** Properties in term of [if ... then ... else ...] *)
 
-Lemma Zle_cases :
-  forall n m:Z, if Zle_bool n m then (n <= m) else (n > m).
+Lemma Zle_cases n m : if n <=? m then n <= m else n > m.
 Proof.
-  intros x y; unfold Zle_bool, Zle, Zgt in |- *.
-  case (x ?= y); auto; discriminate.
+ case Z.leb_spec; now Z.swap_greater.
 Qed.
 
-Lemma Zlt_cases :
-  forall n m:Z, if Zlt_bool n m then (n < m) else (n >= m).
+Lemma Zlt_cases n m : if n <? m then n < m else n >= m.
 Proof.
-  intros x y; unfold Zlt_bool, Zlt, Zge in |- *.
-  case (x ?= y); auto; discriminate.
+ case Z.ltb_spec; now Z.swap_greater.
 Qed.
 
-Lemma Zge_cases :
-  forall n m:Z, if Zge_bool n m then (n >= m) else (n < m).
+Lemma Zge_cases n m : if n >=? m then n >= m else n < m.
 Proof.
-  intros x y; unfold Zge_bool, Zge, Zlt in |- *.
-  case (x ?= y); auto; discriminate.
+ rewrite Z.geb_leb. case Z.leb_spec; now Z.swap_greater.
 Qed.
 
-Lemma Zgt_cases :
-  forall n m:Z, if Zgt_bool n m then (n > m) else (n <= m).
+Lemma Zgt_cases n m : if n >? m then n > m else n <= m.
 Proof.
-  intros x y; unfold Zgt_bool, Zgt, Zle in |- *.
-  case (x ?= y); auto; discriminate.
+ rewrite Z.gtb_ltb. case Z.ltb_spec; now Z.swap_greater.
 Qed.
 
-(** Lemmas on [Zle_bool] used in contrib/graphs *)
+(** Lemmas on [Z.leb] used in contrib/graphs *)
 
-Lemma Zle_bool_imp_le : forall n m:Z, Zle_bool n m = true -> (n <= m).
+Lemma Zle_bool_imp_le n m : (n <=? m) = true -> (n <= m).
 Proof.
-  unfold Zle_bool, Zle in |- *. intros x y. unfold not in |- *.
-  case (x ?= y); intros; discriminate.
+ apply Z.leb_le.
 Qed.
 
-Lemma Zle_imp_le_bool : forall n m:Z, (n <= m) -> Zle_bool n m = true.
+Lemma Zle_imp_le_bool n m : (n <= m) -> (n <=? m) = true.
 Proof.
-  unfold Zle, Zle_bool in |- *. intros x y. case (x ?= y); trivial. intro. elim (H (refl_equal _)).
+ apply Z.leb_le.
 Qed.
 
-Lemma Zle_bool_refl : forall n:Z, Zle_bool n n = true.
-Proof.
-  intro. apply Zle_imp_le_bool. apply Zeq_le. reflexivity.
-Qed.
+Notation Zle_bool_refl := Z.leb_refl (only parsing).
 
-Lemma Zle_bool_antisym :
-  forall n m:Z, Zle_bool n m = true -> Zle_bool m n = true -> n = m.
+Lemma Zle_bool_antisym n m :
+ (n <=? m) = true -> (m <=? n) = true -> n = m.
 Proof.
-  intros. apply Zle_antisym. apply Zle_bool_imp_le. assumption.
-  apply Zle_bool_imp_le. assumption.
+ rewrite !Z.leb_le. apply Z.le_antisymm.
 Qed.
 
-Lemma Zle_bool_trans :
-  forall n m p:Z,
-    Zle_bool n m = true -> Zle_bool m p = true -> Zle_bool n p = true.
+Lemma Zle_bool_trans n m p :
+ (n <=? m) = true -> (m <=? p) = true -> (n <=? p) = true.
 Proof.
-  intros x y z; intros. apply Zle_imp_le_bool. apply Zle_trans with (m := y). apply Zle_bool_imp_le. assumption.
-  apply Zle_bool_imp_le. assumption.
+ rewrite !Z.leb_le. apply Z.le_trans.
 Qed.
 
-Definition Zle_bool_total :
-  forall x y:Z, {Zle_bool x y = true} + {Zle_bool y x = true}.
+Definition Zle_bool_total x y :
+  { x <=? y = true } + { y <=? x = true }.
 Proof.
-  intros x y; intros. unfold Zle_bool in |- *. cut ((x ?= y) = Gt <-> (y ?= x) = Lt).
-  case (x ?= y). left. reflexivity.
-  left. reflexivity.
-  right. rewrite (proj1 H (refl_equal _)). reflexivity.
-  apply Zcompare_Gt_Lt_antisym.
+ case_eq (x <=? y); intros H.
+ - left; trivial.
+ - right. apply Z.leb_gt in H. now apply Z.leb_le, Z.lt_le_incl.
 Defined.
 
-Lemma Zle_bool_plus_mono :
-  forall n m p q:Z,
-    Zle_bool n m = true ->
-    Zle_bool p q = true -> Zle_bool (n + p) (m + q) = true.
+Lemma Zle_bool_plus_mono n m p q :
+ (n <=? m) = true ->
+ (p <=? q) = true ->
+ (n + p <=? m + q) = true.
 Proof.
-  intros. apply Zle_imp_le_bool. apply Zplus_le_compat. apply Zle_bool_imp_le. assumption.
-  apply Zle_bool_imp_le. assumption.
+ rewrite !Z.leb_le. apply Z.add_le_mono.
 Qed.
 
-Lemma Zone_pos : Zle_bool 1 0 = false.
+Lemma Zone_pos : 1 <=? 0 = false.
 Proof.
-  reflexivity.
+ reflexivity.
 Qed.
 
-Lemma Zone_min_pos : forall n:Z, Zle_bool n 0 = false -> Zle_bool 1 n = true.
+Lemma Zone_min_pos n : (n <=? 0) = false -> (1 <=? n) = true.
 Proof.
-  intros x; intros. apply Zle_imp_le_bool. change (Zsucc 0 <= x) in |- *. apply Zgt_le_succ. generalize H.
-  unfold Zle_bool, Zgt in |- *. case (x ?= 0). intro H0. discriminate H0.
-  intro H0. discriminate H0.
-  reflexivity.
+ rewrite Z.leb_le, Z.leb_gt. apply Z.le_succ_l.
 Qed.
 
 (** Properties in term of [iff] *)
 
-Lemma Zle_is_le_bool : forall n m:Z, (n <= m) <-> Zle_bool n m = true.
+Lemma Zle_is_le_bool n m : (n <= m) <-> (n <=? m) = true.
 Proof.
-  intros. split. intro. apply Zle_imp_le_bool. assumption.
-  intro. apply Zle_bool_imp_le. assumption.
+ symmetry. apply Z.leb_le.
 Qed.
 
-Lemma Zge_is_le_bool : forall n m:Z, (n >= m) <-> Zle_bool m n = true.
+Lemma Zge_is_le_bool n m : (n >= m) <-> (m <=? n) = true.
 Proof.
-  intros. split. intro. apply Zle_imp_le_bool. apply Zge_le. assumption.
-  intro. apply Zle_ge. apply Zle_bool_imp_le. assumption.
+ Z.swap_greater. symmetry. apply Z.leb_le.
 Qed.
 
-Lemma Zlt_is_lt_bool : forall n m:Z, (n < m) <-> Zlt_bool n m = true.
+Lemma Zlt_is_lt_bool n m : (n < m) <-> (n <? m) = true.
 Proof.
-intros n m; unfold Zlt_bool, Zlt.
-destruct (n ?= m); simpl; split; now intro.
+ symmetry. apply Z.ltb_lt.
 Qed.
 
-Lemma Zgt_is_gt_bool : forall n m:Z, (n > m) <-> Zgt_bool n m = true.
+Lemma Zgt_is_gt_bool n m : (n > m) <-> (n >? m) = true.
 Proof.
-intros n m; unfold Zgt_bool, Zgt.
-destruct (n ?= m); simpl; split; now intro.
+ Z.swap_greater. rewrite Z.gtb_ltb. symmetry. apply Z.ltb_lt.
 Qed.
 
-Lemma Zlt_is_le_bool :
-  forall n m:Z, (n < m) <-> Zle_bool n (m - 1) = true.
+Lemma Zlt_is_le_bool n m : (n < m) <-> (n <=? m - 1) = true.
 Proof.
-  intros x y. split. intro. apply Zle_imp_le_bool. apply Zlt_succ_le. rewrite (Zsucc_pred y) in H.
-  assumption.
-  intro. rewrite (Zsucc_pred y). apply Zle_lt_succ. apply Zle_bool_imp_le. assumption.
+ rewrite Z.leb_le. apply Z.lt_le_pred.
 Qed.
 
-Lemma Zgt_is_le_bool :
-  forall n m:Z, (n > m) <-> Zle_bool m (n - 1) = true.
+Lemma Zgt_is_le_bool n m : (n > m) <-> (m <=? n - 1) = true.
 Proof.
-  intros x y. apply iff_trans with (y < x). split. exact (Zgt_lt x y).
-  exact (Zlt_gt y x).
-  exact (Zlt_is_le_bool y x).
+ Z.swap_greater. rewrite Z.leb_le. apply Z.lt_le_pred.
 Qed.
 
-Lemma Zeq_is_eq_bool : forall x y, x = y <-> Zeq_bool x y = true.
+(** Properties of the deprecated [Zeq_bool] *)
+
+Lemma Zeq_is_eq_bool x y : x = y <-> Zeq_bool x y = true.
 Proof.
-  intros; unfold Zeq_bool.
-  generalize (Zcompare_Eq_iff_eq x y); destruct Zcompare; intuition;
-   try discriminate.
+ unfold Zeq_bool.
+ rewrite <- Z.compare_eq_iff. destruct Z.compare; now split.
 Qed.
 
-Lemma Zeq_bool_eq : forall x y, Zeq_bool x y = true -> x = y.
+Lemma Zeq_bool_eq x y : Zeq_bool x y = true -> x = y.
 Proof.
-  intros x y H; apply <- Zeq_is_eq_bool; auto.
+ apply Zeq_is_eq_bool.
 Qed.
 
-Lemma Zeq_bool_neq : forall x y, Zeq_bool x y = false -> x <> y.
+Lemma Zeq_bool_neq x y : Zeq_bool x y = false -> x <> y.
 Proof.
-  unfold Zeq_bool; red ; intros; subst.
-  rewrite Zcompare_refl in H.
-  discriminate.
+ rewrite Zeq_is_eq_bool; now destruct Zeq_bool.
 Qed.
 
-Lemma Zeq_bool_if : forall x y, if Zeq_bool x y then x=y else x<>y.
+Lemma Zeq_bool_if x y : if Zeq_bool x y then x=y else x<>y.
 Proof.
-  intros. generalize (Zeq_bool_eq x y)(Zeq_bool_neq x y).
-  destruct Zeq_bool; auto.
+ generalize (Zeq_bool_eq x y) (Zeq_bool_neq x y).
+ destruct Zeq_bool; auto.
 Qed.
diff --git a/theories/ZArith/Zeven.v b/theories/ZArith/Zeven.v
index d37a6a9c3..550b66f78 100644
--- a/theories/ZArith/Zeven.v
+++ b/theories/ZArith/Zeven.v
@@ -6,15 +6,20 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+(** Binary Integers : Parity and Division by Two *)
+(** Initial author : Pierre Crégut (CNET, Lannion, France) *)
+
+(** THIS FILE IS DEPRECATED.
+    It is now almost entirely made of compatibility formulations
+    for results already present in BinInt.Z. *)
+
 Require Import BinInt.
 
 Open Scope Z_scope.
 
-(*******************************************************************)
-(** About parity: even and odd predicates on Z, division by 2 on Z *)
-
-(***************************************************)
-(** * [Zeven], [Zodd] and their related properties *)
+(** Historical formulation of even and odd predicates, based on
+    case analysis. We now rather recommend using [Z.Even] and
+    [Z.Odd], which are based on the exist predicate. *)
 
 Definition Zeven (z:Z) :=
   match z with
@@ -33,128 +38,102 @@ Definition Zodd (z:Z) :=
     | _ => False
   end.
 
+Lemma Zeven_equiv z : Zeven z <-> Z.Even z.
+Proof.
+ rewrite <- Z.even_spec.
+ destruct z as [|p|p]; try destruct p; simpl; intuition.
+Qed.
+
+Lemma Zodd_equiv z : Zodd z <-> Z.Odd z.
+Proof.
+ rewrite <- Z.odd_spec.
+ destruct z as [|p|p]; try destruct p; simpl; intuition.
+Qed.
+
+Theorem Zeven_ex_iff n : Zeven n <-> exists m, n = 2*m.
+Proof (Zeven_equiv n).
+
+Theorem Zodd_ex_iff n : Zodd n <-> exists m, n = 2*m + 1.
+Proof (Zodd_equiv n).
+
+(** Boolean tests of parity (now in BinInt.Z) *)
+
 Notation Zeven_bool := Z.even (only parsing).
 Notation Zodd_bool := Z.odd (only parsing).
 
-Lemma Zeven_bool_iff : forall n, Zeven_bool n = true <-> Zeven n.
+Lemma Zeven_bool_iff n : Z.even n = true <-> Zeven n.
 Proof.
- destruct n as [|p|p]; try destruct p; simpl in *; split; easy.
+ now rewrite Z.even_spec, Zeven_equiv.
 Qed.
 
-Lemma Zodd_bool_iff : forall n, Zodd_bool n = true <-> Zodd n.
+Lemma Zodd_bool_iff n : Z.odd n = true <-> Zodd n.
 Proof.
- destruct n as [|p|p]; try destruct p; simpl in *; split; easy.
+ now rewrite Z.odd_spec, Zodd_equiv.
 Qed.
 
-Lemma Zodd_even_bool : forall n, Zodd_bool n = negb (Zeven_bool n).
+Ltac boolify_even_odd := rewrite <- ?Zeven_bool_iff, <- ?Zodd_bool_iff.
+
+Lemma Zodd_even_bool n : Z.odd n = negb (Z.even n).
 Proof.
- destruct n as [|p|p]; trivial; now destruct p.
+ symmetry. apply Z.negb_even.
 Qed.
 
-Lemma Zeven_odd_bool : forall n, Zeven_bool n = negb (Zodd_bool n).
+Lemma Zeven_odd_bool n : Z.even n = negb (Z.odd n).
 Proof.
- destruct n as [|p|p]; trivial; now destruct p.
+ symmetry. apply Z.negb_odd.
 Qed.
 
-Definition Zeven_odd_dec : forall z:Z, {Zeven z} + {Zodd z}.
+Definition Zeven_odd_dec n : {Zeven n} + {Zodd n}.
 Proof.
-  intro z. case z;
-  [ left; compute; trivial
-    | intro p; case p; intros;
-      (right; compute; exact I) || (left; compute; exact I)
-    | intro p; case p; intros;
-      (right; compute; exact I) || (left; compute; exact I) ].
+ destruct n as [|p|p]; try destruct p; simpl; (now left) || (now right).
 Defined.
 
-Definition Zeven_dec : forall z:Z, {Zeven z} + {~ Zeven z}.
+Definition Zeven_dec n : {Zeven n} + {~ Zeven n}.
 Proof.
-  intro z. case z;
-  [ left; compute; trivial
-    | intro p; case p; intros;
-      (left; compute; exact I) || (right; compute; trivial)
-    | intro p; case p; intros;
-      (left; compute; exact I) || (right; compute; trivial) ].
+ destruct n as [|p|p]; try destruct p; simpl; (now left) || (now right).
 Defined.
 
-Definition Zodd_dec : forall z:Z, {Zodd z} + {~ Zodd z}.
+Definition Zodd_dec n : {Zodd n} + {~ Zodd n}.
 Proof.
-  intro z. case z;
-  [ right; compute; trivial
-    | intro p; case p; intros;
-      (left; compute; exact I) || (right; compute; trivial)
-    | intro p; case p; intros;
-      (left; compute; exact I) || (right; compute; trivial) ].
+ destruct n as [|p|p]; try destruct p; simpl; (now left) || (now right).
 Defined.
 
-Lemma Zeven_not_Zodd : forall n:Z, Zeven n -> ~ Zodd n.
+Lemma Zeven_not_Zodd n : Zeven n -> ~ Zodd n.
 Proof.
-  intro z; destruct z; [ idtac | destruct p | destruct p ]; compute;
-    trivial.
+ boolify_even_odd. rewrite <- Z.negb_odd. destruct Z.odd; intuition.
 Qed.
 
-Lemma Zodd_not_Zeven : forall n:Z, Zodd n -> ~ Zeven n.
+Lemma Zodd_not_Zeven n : Zodd n -> ~ Zeven n.
 Proof.
-  intro z; destruct z; [ idtac | destruct p | destruct p ]; compute;
-    trivial.
+ boolify_even_odd. rewrite <- Z.negb_odd. destruct Z.odd; intuition.
 Qed.
 
-Lemma Zeven_Sn : forall n:Z, Zodd n -> Zeven (Zsucc n).
+Lemma Zeven_Sn n : Zodd n -> Zeven (Z.succ n).
 Proof.
-  intro z; destruct z; unfold Zsucc;
-    [ idtac | destruct p | destruct p ]; simpl;
-      trivial.
-  unfold Pdouble_minus_one; case p; simpl; auto.
+ boolify_even_odd. now rewrite Z.even_succ.
 Qed.
 
-Lemma Zodd_Sn : forall n:Z, Zeven n -> Zodd (Zsucc n).
+Lemma Zodd_Sn n : Zeven n -> Zodd (Z.succ n).
 Proof.
-  intro z; destruct z; unfold Zsucc;
-    [ idtac | destruct p | destruct p ]; simpl;
-      trivial.
-  unfold Pdouble_minus_one; case p; simpl; auto.
+ boolify_even_odd. now rewrite Z.odd_succ.
 Qed.
 
-Lemma Zeven_pred : forall n:Z, Zodd n -> Zeven (Zpred n).
+Lemma Zeven_pred n : Zodd n -> Zeven (Z.pred n).
 Proof.
-  intro z; destruct z; unfold Zpred;
-    [ idtac | destruct p | destruct p ]; simpl;
-      trivial.
-  unfold Pdouble_minus_one; case p; simpl; auto.
+ boolify_even_odd. now rewrite Z.even_pred.
 Qed.
 
-Lemma Zodd_pred : forall n:Z, Zeven n -> Zodd (Zpred n).
+Lemma Zodd_pred n : Zeven n -> Zodd (Z.pred n).
 Proof.
-  intro z; destruct z; unfold Zpred;
-    [ idtac | destruct p | destruct p ]; simpl;
-      trivial.
-  unfold Pdouble_minus_one; case p; simpl; auto.
+ boolify_even_odd. now rewrite Z.odd_pred.
 Qed.
 
 Hint Unfold Zeven Zodd: zarith.
 
-Lemma Zeven_bool_succ : forall n, Zeven_bool (Zsucc n) = Zodd_bool n.
-Proof.
- destruct n as [ |p|p]; trivial; destruct p as [p|p| ]; trivial.
- now destruct p.
-Qed.
-
-Lemma Zeven_bool_pred : forall n, Zeven_bool (Zpred n) = Zodd_bool n.
-Proof.
- destruct n as [ |p|p]; trivial; destruct p as [p|p| ]; trivial.
- now destruct p.
-Qed.
-
-Lemma Zodd_bool_succ : forall n, Zodd_bool (Zsucc n) = Zeven_bool n.
-Proof.
- destruct n as [ |p|p]; trivial; destruct p as [p|p| ]; trivial.
- now destruct p.
-Qed.
-
-Lemma Zodd_bool_pred : forall n, Zodd_bool (Zpred n) = Zeven_bool n.
-Proof.
- destruct n as [ |p|p]; trivial; destruct p as [p|p| ]; trivial.
- now destruct p.
-Qed.
+Notation Zeven_bool_succ := Z.even_succ (only parsing).
+Notation Zeven_bool_pred := Z.even_pred (only parsing).
+Notation Zodd_bool_succ := Z.odd_succ (only parsing).
+Notation Zodd_bool_pred := Z.odd_pred (only parsing).
 
 (******************************************************************)
 (** * Definition of [Zquot2], [Zdiv2] and properties wrt [Zeven]
@@ -163,172 +142,149 @@ Qed.
 Notation Zdiv2 := Z.div2 (only parsing).
 Notation Zquot2 := Z.quot2 (only parsing).
 
-(** Properties of [Zdiv2] *)
+(** Properties of [Z.div2] *)
 
-Lemma Zdiv2_odd_eqn : forall n,
- n = 2*(Zdiv2 n) + if Zodd_bool n then 1 else 0.
-Proof.
- intros [ |[p|p| ]|[p|p|  ]]; simpl; trivial.
- f_equal. symmetry. apply Pos.pred_double_succ.
-Qed.
+Lemma Zdiv2_odd_eqn n : n = 2*(Z.div2 n) + if Z.odd n then 1 else 0.
+Proof (Z.div2_odd n).
 
-Lemma Zeven_div2 : forall n:Z, Zeven n -> n = 2 * Zdiv2 n.
+Lemma Zeven_div2 n : Zeven n -> n = 2 * Z.div2 n.
 Proof.
- intros n Hn. apply Zeven_bool_iff in Hn.
- pattern n at 1.
- now rewrite (Zdiv2_odd_eqn n), Zodd_even_bool, Hn, Zplus_0_r.
+ boolify_even_odd. rewrite <- Z.negb_odd, Bool.negb_true_iff.
+ intros Hn. rewrite (Zdiv2_odd_eqn n) at 1. now rewrite Hn, Z.add_0_r.
 Qed.
 
-Lemma Zodd_div2 : forall n:Z, Zodd n -> n = 2 * Zdiv2 n + 1.
+Lemma Zodd_div2 n : Zodd n -> n = 2 * Z.div2 n + 1.
 Proof.
- intros n Hn. apply Zodd_bool_iff in Hn.
- pattern n at 1. now rewrite (Zdiv2_odd_eqn n), Hn.
+ boolify_even_odd.
+ intros Hn. rewrite (Zdiv2_odd_eqn n) at 1. now rewrite Hn.
 Qed.
 
-(** Properties of [Zquot2] *)
+(** Properties of [Z.quot2] *)
+
+(** TODO: move to Numbers someday *)
 
-Lemma Zquot2_odd_eqn : forall n,
- n = 2*(Zquot2 n) + if Zodd_bool n then Zsgn n else 0.
+Lemma Zquot2_odd_eqn n : n = 2*(Z.quot2 n) + if Z.odd n then Z.sgn n else 0.
 Proof.
- intros [ |[p|p| ]|[p|p|  ]]; simpl; trivial.
+ now destruct n as [ |[p|p| ]|[p|p| ]].
 Qed.
 
-Lemma Zeven_quot2 : forall n:Z, Zeven n -> n = 2 * Zquot2 n.
+Lemma Zeven_quot2 n : Zeven n -> n = 2 * Z.quot2 n.
 Proof.
- intros n Hn. apply Zeven_bool_iff in Hn.
- pattern n at 1.
- now rewrite (Zquot2_odd_eqn n), Zodd_even_bool, Hn, Zplus_0_r.
+ intros Hn. apply Zeven_bool_iff in Hn.
+ rewrite (Zquot2_odd_eqn n) at 1.
+ now rewrite Zodd_even_bool, Hn, Z.add_0_r.
 Qed.
 
-Lemma Zodd_quot2 : forall n:Z, n >= 0 -> Zodd n -> n = 2 * Zquot2 n + 1.
+Lemma Zodd_quot2 n : n >= 0 -> Zodd n -> n = 2 * Z.quot2 n + 1.
 Proof.
- intros n Hn Hn'. apply Zodd_bool_iff in Hn'.
- pattern n at 1. rewrite (Zquot2_odd_eqn n), Hn'. f_equal.
+ intros Hn Hn'. apply Zodd_bool_iff in Hn'.
+ rewrite (Zquot2_odd_eqn n) at 1. rewrite Hn'. f_equal.
  destruct n; (now destruct Hn) || easy.
 Qed.
 
-Lemma Zodd_quot2_neg :
-  forall n:Z, n <= 0 -> Zodd n -> n = 2 * Zquot2 n - 1.
+Lemma Zodd_quot2_neg n : n <= 0 -> Zodd n -> n = 2 * Z.quot2 n - 1.
 Proof.
- intros n Hn Hn'. apply Zodd_bool_iff in Hn'.
- pattern n at 1. rewrite (Zquot2_odd_eqn n), Hn'. unfold Zminus. f_equal.
+ intros Hn Hn'. apply Zodd_bool_iff in Hn'.
+ rewrite (Zquot2_odd_eqn n) at 1; rewrite Hn'. unfold Z.sub. f_equal.
  destruct n; (now destruct Hn) || easy.
 Qed.
 
-(** More properties of parity *)
-
-Lemma Z_modulo_2 :
-  forall n:Z, {y : Z | n = 2 * y} + {y : Z | n = 2 * y + 1}.
+Lemma Zquot2_opp n : Z.quot2 (-n) = - Z.quot2 n.
 Proof.
- intros n.
- destruct (Zeven_odd_dec n) as [Hn|Hn].
- left. exists (Zdiv2 n). exact (Zeven_div2 n Hn).
- right. exists (Zdiv2 n). exact (Zodd_div2 n Hn).
+ now destruct n as [ |[p|p| ]|[p|p| ]].
 Qed.
 
-Lemma Zsplit2 :
-  forall n:Z,
-    {p : Z * Z |
-      let (x1, x2) := p in n = x1 + x2 /\ (x1 = x2 \/ x2 = x1 + 1)}.
+Lemma Zquot2_quot n : Z.quot2 n = n ÷ 2.
 Proof.
- intros n.
- destruct (Z_modulo_2 n) as [(y,Hy)|(y,Hy)];
-  rewrite Zmult_comm, <- Zplus_diag_eq_mult_2 in Hy.
- exists (y, y). split. assumption. now left.
- exists (y, y + 1). split. now rewrite Zplus_assoc. now right.
+ assert (AUX : forall m, 0 < m -> Z.quot2 m = m ÷ 2).
+  BeginSubproof.
+   intros m Hm.
+   apply Z.quot_unique with (if Z.odd m then Z.sgn m else 0).
+   now apply Z.lt_le_incl.
+   rewrite Z.sgn_pos by trivial.
+   destruct (Z.odd m); now split.
+   apply Zquot2_odd_eqn.
+  EndSubproof.
+ destruct (Z.lt_trichotomy 0 n) as [POS|[NUL|NEG]].
+ - now apply AUX.
+ - now subst.
+ - apply Z.opp_inj. rewrite <- Z.quot_opp_l, <- Zquot2_opp.
+   apply AUX. now destruct n. easy.
 Qed.
 
-Theorem Zeven_ex: forall n, Zeven n -> exists m, n = 2 * m.
+(** More properties of parity *)
+
+Lemma Z_modulo_2 n : {y | n = 2 * y} + {y | n = 2 * y + 1}.
 Proof.
-  intro n; exists (Zdiv2 n); apply Zeven_div2; auto.
+ destruct (Zeven_odd_dec n) as [Hn|Hn].
+ - left. exists (Z.div2 n). exact (Zeven_div2 n Hn).
+ - right. exists (Z.div2 n). exact (Zodd_div2 n Hn).
 Qed.
 
-Theorem Zodd_ex: forall n, Zodd n -> exists m, n = 2 * m + 1.
+Lemma Zsplit2 n :
+ {p : Z * Z | let (x1, x2) := p in n = x1 + x2 /\ (x1 = x2 \/ x2 = x1 + 1)}.
 Proof.
-  intro n; exists (Zdiv2 n); apply Zodd_div2; auto.
+ destruct (Z_modulo_2 n) as [(y,Hy)|(y,Hy)];
+  rewrite Z.mul_comm, <- Zplus_diag_eq_mult_2 in Hy.
+ - exists (y, y). split. assumption. now left.
+ - exists (y, y + 1). split. now rewrite Z.add_assoc. now right.
 Qed.
 
-Theorem Zeven_2p: forall p, Zeven (2 * p).
+Theorem Zeven_ex n : Zeven n -> exists m, n = 2 * m.
 Proof.
-  destruct p; simpl; auto.
+ exists (Z.div2 n); apply Zeven_div2; auto.
 Qed.
 
-Theorem Zodd_2p_plus_1: forall p, Zodd (2 * p + 1).
+Theorem Zodd_ex n : Zodd n -> exists m, n = 2 * m + 1.
 Proof.
-  destruct p; simpl; auto.
-  destruct p; simpl; auto.
+ exists (Z.div2 n); apply Zodd_div2; auto.
 Qed.
 
-Theorem Zeven_ex_iff : forall n, Zeven n <-> exists m, n = 2*m.
+Theorem Zeven_2p p : Zeven (2 * p).
 Proof.
- split. apply Zeven_ex. intros (m,->). apply Zeven_2p.
+ now destruct p.
 Qed.
 
-Theorem Zodd_ex_iff : forall n, Zodd n <-> exists m, n = 2*m + 1.
+Theorem Zodd_2p_plus_1 p : Zodd (2 * p + 1).
 Proof.
- split. apply Zodd_ex. intros (m,->). apply Zodd_2p_plus_1.
+ destruct p as [|p|p]; now try destruct p.
 Qed.
 
-Theorem Zeven_plus_Zodd: forall a b,
- Zeven a -> Zodd b -> Zodd (a + b).
+Theorem Zeven_plus_Zodd a b : Zeven a -> Zodd b -> Zodd (a + b).
 Proof.
-  intros a b Ha Hb.
-  destruct (Zeven_ex a) as (x,->), (Zodd_ex b) as (y,->); trivial.
-  rewrite Zplus_assoc, <- Zmult_plus_distr_r.
-  apply Zodd_2p_plus_1.
+ boolify_even_odd. rewrite <- Z.negb_odd, Bool.negb_true_iff.
+ intros Ha Hb. now rewrite Z.odd_add, Ha, Hb.
 Qed.
 
-Theorem Zeven_plus_Zeven: forall a b,
- Zeven a -> Zeven b -> Zeven (a + b).
+Theorem Zeven_plus_Zeven a b : Zeven a -> Zeven b -> Zeven (a + b).
 Proof.
-  intros a b Ha Hb.
-  destruct (Zeven_ex a) as (x,->), (Zeven_ex b) as (y,->); trivial.
-  rewrite <- Zmult_plus_distr_r.
-  apply Zeven_2p.
+ boolify_even_odd. intros Ha Hb. now rewrite Z.even_add, Ha, Hb.
 Qed.
 
-Theorem Zodd_plus_Zeven: forall a b,
- Zodd a -> Zeven b -> Zodd (a + b).
+Theorem Zodd_plus_Zeven a b : Zodd a -> Zeven b -> Zodd (a + b).
 Proof.
-  intros a b Ha Hb; rewrite Zplus_comm; apply Zeven_plus_Zodd; auto.
+ intros. rewrite Z.add_comm. now apply Zeven_plus_Zodd.
 Qed.
 
-Theorem Zodd_plus_Zodd: forall a b,
- Zodd a -> Zodd b -> Zeven (a + b).
+Theorem Zodd_plus_Zodd a b : Zodd a -> Zodd b -> Zeven (a + b).
 Proof.
-  intros a b Ha Hb.
-  destruct (Zodd_ex a) as (x,->), (Zodd_ex b) as (y,->); trivial.
-  rewrite <- Zplus_assoc, (Zplus_comm 1), <- Zplus_assoc.
-  change (1+1) with (2*1). rewrite <- 2 Zmult_plus_distr_r.
-  apply Zeven_2p.
+ boolify_even_odd. rewrite <- 2 Z.negb_even, 2 Bool.negb_true_iff.
+ intros Ha Hb. now rewrite Z.even_add, Ha, Hb.
 Qed.
 
-Theorem Zeven_mult_Zeven_l: forall a b,
- Zeven a -> Zeven (a * b).
+Theorem Zeven_mult_Zeven_l a b : Zeven a -> Zeven (a * b).
 Proof.
-  intros a b Ha.
-  destruct (Zeven_ex a) as (x,->); trivial.
-  rewrite <- Zmult_assoc.
-  apply Zeven_2p.
+ boolify_even_odd. intros Ha. now rewrite Z.even_mul, Ha.
 Qed.
 
-Theorem Zeven_mult_Zeven_r: forall a b,
- Zeven b -> Zeven (a * b).
+Theorem Zeven_mult_Zeven_r a b : Zeven b -> Zeven (a * b).
 Proof.
-  intros a b Hb. rewrite Zmult_comm. now apply Zeven_mult_Zeven_l.
+ intros. rewrite Z.mul_comm. now apply Zeven_mult_Zeven_l.
 Qed.
 
-Hint Rewrite Zmult_plus_distr_r Zmult_plus_distr_l
-     Zplus_assoc Zmult_1_r Zmult_1_l : Zexpand.
-
-Theorem Zodd_mult_Zodd: forall a b,
- Zodd a -> Zodd b -> Zodd (a * b).
+Theorem Zodd_mult_Zodd a b : Zodd a -> Zodd b -> Zodd (a * b).
 Proof.
-  intros a b Ha Hb.
-  destruct (Zodd_ex a) as (x,->), (Zodd_ex b) as (y,->); trivial.
-  rewrite Zmult_plus_distr_l, Zmult_1_l.
-  rewrite <- Zmult_assoc, Zplus_assoc, <- Zmult_plus_distr_r.
-  apply Zodd_2p_plus_1.
+ boolify_even_odd. intros Ha Hb. now rewrite Z.odd_mul, Ha, Hb.
 Qed.
 
 (* for compatibility *)
diff --git a/theories/ZArith/Zmisc.v b/theories/ZArith/Zmisc.v
index 6f512e4f3..ff844ec28 100644
--- a/theories/ZArith/Zmisc.v
+++ b/theories/ZArith/Zmisc.v
@@ -21,8 +21,8 @@ Open Local Scope Z_scope.
 Notation iter := @Z.iter (only parsing).
 
 Lemma iter_nat_of_Z : forall n A f x, 0 <= n ->
-  iter n A f x = iter_nat (Zabs_nat n) A f x.
+  iter n A f x = iter_nat (Z.abs_nat n) A f x.
 intros n A f x; case n; auto.
-intros p _; unfold Z.iter, Zabs_nat; apply iter_nat_of_P.
+intros p _; unfold Z.iter, Z.abs_nat; apply iter_nat_of_P.
 intros p abs; case abs; trivial.
 Qed.
diff --git a/theories/ZArith/auxiliary.v b/theories/ZArith/auxiliary.v
index 95d378785..742f4bde3 100644
--- a/theories/ZArith/auxiliary.v
+++ b/theories/ZArith/auxiliary.v
@@ -16,96 +16,79 @@ Require Import Decidable.
 Require Import Peano_dec.
 Require Export Compare_dec.
 
-Open Local Scope Z_scope.
+Local Open Scope Z_scope.
 
 (***************************************************************)
 (** * Moving terms from one side to the other of an inequality *)
 
-Theorem Zne_left : forall n m:Z, Zne n m -> Zne (n + - m) 0.
+Theorem Zne_left n m : Zne n m -> Zne (n + - m) 0.
 Proof.
-  intros x y; unfold Zne in |- *; unfold not in |- *; intros H1 H2; apply H1;
-    apply Zplus_reg_l with (- y); rewrite Zplus_opp_l;
-      rewrite Zplus_comm; trivial with arith.
+ unfold Zne. now rewrite <- Z.sub_move_0_r.
 Qed.
 
-Theorem Zegal_left : forall n m:Z, n = m -> n + - m = 0.
+Theorem Zegal_left n m : n = m -> n + - m = 0.
 Proof.
-  intros x y H; apply (Zplus_reg_l y); rewrite Zplus_permute;
-    rewrite Zplus_opp_r; do 2 rewrite Zplus_0_r; assumption.
+ apply Z.sub_move_0_r.
 Qed.
 
-Theorem Zle_left : forall n m:Z, n <= m -> 0 <= m + - n.
+Theorem Zle_left n m : n <= m -> 0 <= m + - n.
 Proof.
-  intros x y H; replace 0 with (x + - x).
-  apply Zplus_le_compat_r; trivial.
-  apply Zplus_opp_r.
+ apply Z.le_0_sub.
 Qed.
 
-Theorem Zle_left_rev : forall n m:Z, 0 <= m + - n -> n <= m.
+Theorem Zle_left_rev n m : 0 <= m + - n -> n <= m.
 Proof.
-  intros x y H; apply Zplus_le_reg_r with (- x).
-  rewrite Zplus_opp_r; trivial.
+ apply Z.le_0_sub.
 Qed.
 
-Theorem Zlt_left_rev : forall n m:Z, 0 < m + - n -> n < m.
+Theorem Zlt_left_rev n m : 0 < m + - n -> n < m.
 Proof.
-  intros x y H; apply Zplus_lt_reg_r with (- x).
-  rewrite Zplus_opp_r; trivial.
+ apply Z.lt_0_sub.
 Qed.
 
-Theorem Zlt_left : forall n m:Z, n < m -> 0 <= m + -1 + - n.
+Theorem Zlt_left_lt n m : n < m -> 0 < m + - n.
 Proof.
-  intros x y H; apply Zle_left; apply Zsucc_le_reg;
-    change (Zsucc x <= Zsucc (Zpred y)) in |- *; rewrite <- Zsucc_pred;
-      apply Zlt_le_succ; assumption.
+ apply Z.lt_0_sub.
 Qed.
 
-Theorem Zlt_left_lt : forall n m:Z, n < m -> 0 < m + - n.
+Theorem Zlt_left n m : n < m -> 0 <= m + -1 + - n.
 Proof.
-  intros x y H; replace 0 with (x + - x).
-  apply Zplus_lt_compat_r; trivial.
-  apply Zplus_opp_r.
+ intros. rewrite Z.add_shuffle0. change (-1) with (- Z.succ 0).
+ now apply Z.le_0_sub, Z.le_succ_l, Z.lt_0_sub.
 Qed.
 
-Theorem Zge_left : forall n m:Z, n >= m -> 0 <= n + - m.
+Theorem Zge_left n m : n >= m -> 0 <= n + - m.
 Proof.
-  intros x y H; apply Zle_left; apply Zge_le; assumption.
+ Z.swap_greater. apply Z.le_0_sub.
 Qed.
 
-Theorem Zgt_left : forall n m:Z, n > m -> 0 <= n + -1 + - m.
+Theorem Zgt_left n m : n > m -> 0 <= n + -1 + - m.
 Proof.
-  intros x y H; apply Zlt_left; apply Zgt_lt; assumption.
+ Z.swap_greater. apply Zlt_left.
 Qed.
 
-Theorem Zgt_left_gt : forall n m:Z, n > m -> n + - m > 0.
+Theorem Zgt_left_gt n m : n > m -> n + - m > 0.
 Proof.
-  intros x y H; replace 0 with (y + - y).
-  apply Zplus_gt_compat_r; trivial.
-  apply Zplus_opp_r.
+ Z.swap_greater. apply Z.lt_0_sub.
 Qed.
 
-Theorem Zgt_left_rev : forall n m:Z, n + - m > 0 -> n > m.
+Theorem Zgt_left_rev n m : n + - m > 0 -> n > m.
 Proof.
-  intros x y H; apply Zplus_gt_reg_r with (- y).
-  rewrite Zplus_opp_r; trivial.
+ Z.swap_greater. apply Z.lt_0_sub.
 Qed.
 
-Theorem Zle_mult_approx :
-  forall n m p:Z, n > 0 -> p > 0 -> 0 <= m -> 0 <= m * n + p.
+Theorem Zle_mult_approx n m p :
+  n > 0 -> p > 0 -> 0 <= m -> 0 <= m * n + p.
 Proof.
-  intros x y z H1 H2 H3; apply Zle_trans with (m := y * x);
-    [ apply Zmult_gt_0_le_0_compat; assumption
-      | pattern (y * x) at 1 in |- *; rewrite <- Zplus_0_r;
-	apply Zplus_le_compat_l; apply Zlt_le_weak; apply Zgt_lt;
-	  assumption ].
+ Z.swap_greater. intros. Z.order_pos.
 Qed.
 
-Theorem Zmult_le_approx :
-  forall n m p:Z, n > 0 -> n > p -> 0 <= m * n + p -> 0 <= m.
+Theorem Zmult_le_approx n m p :
+  n > 0 -> n > p -> 0 <= m * n + p -> 0 <= m.
 Proof.
-  intros x y z H1 H2 H3; apply Zlt_succ_le; apply Zmult_gt_0_lt_0_reg_r with x;
-    [ assumption
-      | apply Zle_lt_trans with (1 := H3); rewrite <- Zmult_succ_l_reverse;
-	apply Zplus_lt_compat_l; apply Zgt_lt; assumption ].
+ Z.swap_greater. intros. apply Z.lt_succ_r.
+ apply Z.mul_pos_cancel_r with n; trivial. Z.nzsimpl.
+ apply Z.le_lt_trans with (m*n+p); trivial.
+ now apply Z.add_lt_mono_l.
 Qed.