summaryrefslogtreecommitdiff
path: root/theories/ZArith
diff options
context:
space:
mode:
Diffstat (limited to 'theories/ZArith')
-rw-r--r--theories/ZArith/BinInt.v56
-rw-r--r--theories/ZArith/BinIntDef.v15
-rw-r--r--theories/ZArith/ZArith_dec.v2
-rw-r--r--theories/ZArith/Zabs.v8
-rw-r--r--theories/ZArith/Zcompare.v14
-rw-r--r--theories/ZArith/Zdiv.v6
-rw-r--r--theories/ZArith/Zeven.v4
-rw-r--r--theories/ZArith/Zmax.v18
-rw-r--r--theories/ZArith/Zmin.v18
-rw-r--r--theories/ZArith/Znumtheory.v28
-rw-r--r--theories/ZArith/Zorder.v28
-rw-r--r--theories/ZArith/Zpow_facts.v4
-rw-r--r--theories/ZArith/Zquot.v46
13 files changed, 129 insertions, 118 deletions
diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v
index cf7397b5..12413453 100644
--- a/theories/ZArith/BinInt.v
+++ b/theories/ZArith/BinInt.v
@@ -1248,6 +1248,8 @@ Bind Scope Z_scope with Z.t Z.
(** Re-export Notations *)
+Numeral Notation Z Z.of_int Z.to_int : Z_scope.
+
Infix "+" := Z.add : Z_scope.
Notation "- x" := (Z.opp x) : Z_scope.
Infix "-" := Z.sub : Z_scope.
@@ -1569,40 +1571,40 @@ End Z2Pos.
Notation Zdouble_plus_one := Z.succ_double (only parsing).
Notation Zdouble_minus_one := Z.pred_double (only parsing).
-Notation Zdouble := Z.double (compat "8.6").
+Notation Zdouble := Z.double (compat "8.7").
Notation ZPminus := Z.pos_sub (only parsing).
-Notation Zsucc' := Z.succ (compat "8.6").
-Notation Zpred' := Z.pred (compat "8.6").
-Notation Zplus' := Z.add (compat "8.6").
+Notation Zsucc' := Z.succ (compat "8.7").
+Notation Zpred' := Z.pred (compat "8.7").
+Notation Zplus' := Z.add (compat "8.7").
Notation Zplus := Z.add (only parsing). (* Slightly incompatible *)
-Notation Zopp := Z.opp (compat "8.6").
-Notation Zsucc := Z.succ (compat "8.6").
-Notation Zpred := Z.pred (compat "8.6").
+Notation Zopp := Z.opp (compat "8.7").
+Notation Zsucc := Z.succ (compat "8.7").
+Notation Zpred := Z.pred (compat "8.7").
Notation Zminus := Z.sub (only parsing).
Notation Zmult := Z.mul (only parsing).
-Notation Zcompare := Z.compare (compat "8.6").
-Notation Zsgn := Z.sgn (compat "8.6").
-Notation Zle := Z.le (compat "8.6").
-Notation Zge := Z.ge (compat "8.6").
-Notation Zlt := Z.lt (compat "8.6").
-Notation Zgt := Z.gt (compat "8.6").
-Notation Zmax := Z.max (compat "8.6").
-Notation Zmin := Z.min (compat "8.6").
-Notation Zabs := Z.abs (compat "8.6").
-Notation Zabs_nat := Z.abs_nat (compat "8.6").
-Notation Zabs_N := Z.abs_N (compat "8.6").
+Notation Zcompare := Z.compare (compat "8.7").
+Notation Zsgn := Z.sgn (compat "8.7").
+Notation Zle := Z.le (compat "8.7").
+Notation Zge := Z.ge (compat "8.7").
+Notation Zlt := Z.lt (compat "8.7").
+Notation Zgt := Z.gt (compat "8.7").
+Notation Zmax := Z.max (compat "8.7").
+Notation Zmin := Z.min (compat "8.7").
+Notation Zabs := Z.abs (compat "8.7").
+Notation Zabs_nat := Z.abs_nat (compat "8.7").
+Notation Zabs_N := Z.abs_N (compat "8.7").
Notation Z_of_nat := Z.of_nat (only parsing).
Notation Z_of_N := Z.of_N (only parsing).
Notation Zind := Z.peano_ind (only parsing).
-Notation Zopp_0 := Z.opp_0 (compat "8.6").
-Notation Zopp_involutive := Z.opp_involutive (compat "8.6").
-Notation Zopp_inj := Z.opp_inj (compat "8.6").
+Notation Zopp_0 := Z.opp_0 (compat "8.7").
+Notation Zopp_involutive := Z.opp_involutive (compat "8.7").
+Notation Zopp_inj := Z.opp_inj (compat "8.7").
Notation Zplus_0_l := Z.add_0_l (only parsing).
Notation Zplus_0_r := Z.add_0_r (only parsing).
Notation Zplus_comm := Z.add_comm (only parsing).
Notation Zopp_plus_distr := Z.opp_add_distr (only parsing).
-Notation Zopp_succ := Z.opp_succ (compat "8.6").
+Notation Zopp_succ := Z.opp_succ (compat "8.7").
Notation Zplus_opp_r := Z.add_opp_diag_r (only parsing).
Notation Zplus_opp_l := Z.add_opp_diag_l (only parsing).
Notation Zplus_assoc := Z.add_assoc (only parsing).
@@ -1611,11 +1613,11 @@ Notation Zplus_reg_l := Z.add_reg_l (only parsing).
Notation Zplus_succ_l := Z.add_succ_l (only parsing).
Notation Zplus_succ_comm := Z.add_succ_comm (only parsing).
Notation Zsucc_discr := Z.neq_succ_diag_r (only parsing).
-Notation Zsucc_inj := Z.succ_inj (compat "8.6").
-Notation Zsucc'_inj := Z.succ_inj (compat "8.6").
-Notation Zsucc'_pred' := Z.succ_pred (compat "8.6").
-Notation Zpred'_succ' := Z.pred_succ (compat "8.6").
-Notation Zpred'_inj := Z.pred_inj (compat "8.6").
+Notation Zsucc_inj := Z.succ_inj (compat "8.7").
+Notation Zsucc'_inj := Z.succ_inj (compat "8.7").
+Notation Zsucc'_pred' := Z.succ_pred (compat "8.7").
+Notation Zpred'_succ' := Z.pred_succ (compat "8.7").
+Notation Zpred'_inj := Z.pred_inj (compat "8.7").
Notation Zsucc'_discr := Z.neq_succ_diag_r (only parsing).
Notation Zminus_0_r := Z.sub_0_r (only parsing).
Notation Zminus_diag := Z.sub_diag (only parsing).
diff --git a/theories/ZArith/BinIntDef.v b/theories/ZArith/BinIntDef.v
index db4de0b9..8cb62622 100644
--- a/theories/ZArith/BinIntDef.v
+++ b/theories/ZArith/BinIntDef.v
@@ -14,6 +14,10 @@ Require Import BinPos BinNat.
Local Open Scope Z_scope.
+Local Notation "0" := Z0.
+Local Notation "1" := (Zpos 1).
+Local Notation "2" := (Zpos 2).
+
(***********************************************************)
(** * Binary Integers, Definitions of Operations *)
(***********************************************************)
@@ -53,7 +57,7 @@ Definition succ_double x :=
Definition pred_double x :=
match x with
- | 0 => -1
+ | 0 => neg 1
| neg p => neg p~1
| pos p => pos (Pos.pred_double p)
end.
@@ -104,7 +108,7 @@ Definition succ x := x + 1.
(** ** Predecessor *)
-Definition pred x := x + -1.
+Definition pred x := x + neg 1.
(** ** Subtraction *)
@@ -171,7 +175,7 @@ Definition sgn z :=
match z with
| 0 => 0
| pos p => 1
- | neg p => -1
+ | neg p => neg 1
end.
(** Boolean equality and comparisons *)
@@ -635,4 +639,9 @@ Definition lxor a b :=
| neg a, neg b => of_N (N.lxor (Pos.pred_N a) (Pos.pred_N b))
end.
+Numeral Notation Z of_int to_int : Z_scope.
+
End Z.
+
+(** Re-export the notation for those who just [Import BinIntDef] *)
+Numeral Notation Z Z.of_int Z.to_int : Z_scope.
diff --git a/theories/ZArith/ZArith_dec.v b/theories/ZArith/ZArith_dec.v
index 9bcdb73a..6cadf30f 100644
--- a/theories/ZArith/ZArith_dec.v
+++ b/theories/ZArith/ZArith_dec.v
@@ -34,7 +34,7 @@ Lemma Zcompare_rec (P:Set) (n m:Z) :
((n ?= m) = Eq -> P) -> ((n ?= m) = Lt -> P) -> ((n ?= m) = Gt -> P) -> P.
Proof. apply Zcompare_rect. Defined.
-Notation Z_eq_dec := Z.eq_dec (compat "8.6").
+Notation Z_eq_dec := Z.eq_dec (compat "8.7").
Section decidability.
diff --git a/theories/ZArith/Zabs.v b/theories/ZArith/Zabs.v
index 0d8450e3..057eb499 100644
--- a/theories/ZArith/Zabs.v
+++ b/theories/ZArith/Zabs.v
@@ -29,17 +29,17 @@ Local Open Scope Z_scope.
(**********************************************************************)
(** * Properties of absolute value *)
-Notation Zabs_eq := Z.abs_eq (compat "8.6").
+Notation Zabs_eq := Z.abs_eq (compat "8.7").
Notation Zabs_non_eq := Z.abs_neq (only parsing).
Notation Zabs_Zopp := Z.abs_opp (only parsing).
Notation Zabs_pos := Z.abs_nonneg (only parsing).
-Notation Zabs_involutive := Z.abs_involutive (compat "8.6").
+Notation Zabs_involutive := Z.abs_involutive (compat "8.7").
Notation Zabs_eq_case := Z.abs_eq_cases (only parsing).
-Notation Zabs_triangle := Z.abs_triangle (compat "8.6").
+Notation Zabs_triangle := Z.abs_triangle (compat "8.7").
Notation Zsgn_Zabs := Z.sgn_abs (only parsing).
Notation Zabs_Zsgn := Z.abs_sgn (only parsing).
Notation Zabs_Zmult := Z.abs_mul (only parsing).
-Notation Zabs_square := Z.abs_square (compat "8.6").
+Notation Zabs_square := Z.abs_square (compat "8.7").
(** * Proving a property of the absolute value by cases *)
diff --git a/theories/ZArith/Zcompare.v b/theories/ZArith/Zcompare.v
index c8432e27..6ccb0153 100644
--- a/theories/ZArith/Zcompare.v
+++ b/theories/ZArith/Zcompare.v
@@ -183,15 +183,15 @@ Qed.
(** Compatibility notations *)
-Notation Zcompare_refl := Z.compare_refl (compat "8.6").
+Notation Zcompare_refl := Z.compare_refl (compat "8.7").
Notation Zcompare_Eq_eq := Z.compare_eq (only parsing).
Notation Zcompare_Eq_iff_eq := Z.compare_eq_iff (only parsing).
-Notation Zcompare_spec := Z.compare_spec (compat "8.6").
-Notation Zmin_l := Z.min_l (compat "8.6").
-Notation Zmin_r := Z.min_r (compat "8.6").
-Notation Zmax_l := Z.max_l (compat "8.6").
-Notation Zmax_r := Z.max_r (compat "8.6").
-Notation Zabs_eq := Z.abs_eq (compat "8.6").
+Notation Zcompare_spec := Z.compare_spec (compat "8.7").
+Notation Zmin_l := Z.min_l (compat "8.7").
+Notation Zmin_r := Z.min_r (compat "8.7").
+Notation Zmax_l := Z.max_l (compat "8.7").
+Notation Zmax_r := Z.max_r (compat "8.7").
+Notation Zabs_eq := Z.abs_eq (compat "8.7").
Notation Zabs_non_eq := Z.abs_neq (only parsing).
Notation Zsgn_0 := Z.sgn_null (only parsing).
Notation Zsgn_1 := Z.sgn_pos (only parsing).
diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v
index 15d0e487..74614e11 100644
--- a/theories/ZArith/Zdiv.v
+++ b/theories/ZArith/Zdiv.v
@@ -21,11 +21,11 @@ Local Open Scope Z_scope.
specifications and properties are in [BinInt]. *)
Notation Zdiv_eucl_POS := Z.pos_div_eucl (only parsing).
-Notation Zdiv_eucl := Z.div_eucl (compat "8.6").
-Notation Zdiv := Z.div (compat "8.6").
+Notation Zdiv_eucl := Z.div_eucl (compat "8.7").
+Notation Zdiv := Z.div (compat "8.7").
Notation Zmod := Z.modulo (only parsing).
-Notation Zdiv_eucl_eq := Z.div_eucl_eq (compat "8.6").
+Notation Zdiv_eucl_eq := Z.div_eucl_eq (compat "8.7").
Notation Z_div_mod_eq_full := Z.div_mod (only parsing).
Notation Zmod_POS_bound := Z.pos_div_eucl_bound (only parsing).
Notation Zmod_pos_bound := Z.mod_pos_bound (only parsing).
diff --git a/theories/ZArith/Zeven.v b/theories/ZArith/Zeven.v
index 00a58b51..9e83bfc1 100644
--- a/theories/ZArith/Zeven.v
+++ b/theories/ZArith/Zeven.v
@@ -141,8 +141,8 @@ Notation Zodd_bool_pred := Z.odd_pred (only parsing).
(** * Definition of [Z.quot2], [Z.div2] and properties wrt [Zeven]
and [Zodd] *)
-Notation Zdiv2 := Z.div2 (compat "8.6").
-Notation Zquot2 := Z.quot2 (compat "8.6").
+Notation Zdiv2 := Z.div2 (compat "8.7").
+Notation Zquot2 := Z.quot2 (compat "8.7").
(** Properties of [Z.div2] *)
diff --git a/theories/ZArith/Zmax.v b/theories/ZArith/Zmax.v
index 7f595fcf..26bd9e81 100644
--- a/theories/ZArith/Zmax.v
+++ b/theories/ZArith/Zmax.v
@@ -18,22 +18,22 @@ Local Open Scope Z_scope.
(** Exact compatibility *)
-Notation Zmax_case := Z.max_case (compat "8.6").
-Notation Zmax_case_strong := Z.max_case_strong (compat "8.6").
+Notation Zmax_case := Z.max_case (compat "8.7").
+Notation Zmax_case_strong := Z.max_case_strong (compat "8.7").
Notation Zmax_right := Z.max_r (only parsing).
-Notation Zle_max_l := Z.le_max_l (compat "8.6").
-Notation Zle_max_r := Z.le_max_r (compat "8.6").
-Notation Zmax_lub := Z.max_lub (compat "8.6").
-Notation Zmax_lub_lt := Z.max_lub_lt (compat "8.6").
+Notation Zle_max_l := Z.le_max_l (compat "8.7").
+Notation Zle_max_r := Z.le_max_r (compat "8.7").
+Notation Zmax_lub := Z.max_lub (compat "8.7").
+Notation Zmax_lub_lt := Z.max_lub_lt (compat "8.7").
Notation Zle_max_compat_r := Z.max_le_compat_r (only parsing).
Notation Zle_max_compat_l := Z.max_le_compat_l (only parsing).
Notation Zmax_idempotent := Z.max_id (only parsing).
Notation Zmax_n_n := Z.max_id (only parsing).
-Notation Zmax_comm := Z.max_comm (compat "8.6").
-Notation Zmax_assoc := Z.max_assoc (compat "8.6").
+Notation Zmax_comm := Z.max_comm (compat "8.7").
+Notation Zmax_assoc := Z.max_assoc (compat "8.7").
Notation Zmax_irreducible_dec := Z.max_dec (only parsing).
Notation Zmax_le_prime := Z.max_le (only parsing).
-Notation Zsucc_max_distr := Z.succ_max_distr (compat "8.6").
+Notation Zsucc_max_distr := Z.succ_max_distr (compat "8.7").
Notation Zmax_SS := Z.succ_max_distr (only parsing).
Notation Zplus_max_distr_l := Z.add_max_distr_l (only parsing).
Notation Zplus_max_distr_r := Z.add_max_distr_r (only parsing).
diff --git a/theories/ZArith/Zmin.v b/theories/ZArith/Zmin.v
index 6bc72227..5509ee78 100644
--- a/theories/ZArith/Zmin.v
+++ b/theories/ZArith/Zmin.v
@@ -18,20 +18,20 @@ Local Open Scope Z_scope.
(** Exact compatibility *)
-Notation Zmin_case := Z.min_case (compat "8.6").
-Notation Zmin_case_strong := Z.min_case_strong (compat "8.6").
-Notation Zle_min_l := Z.le_min_l (compat "8.6").
-Notation Zle_min_r := Z.le_min_r (compat "8.6").
-Notation Zmin_glb := Z.min_glb (compat "8.6").
-Notation Zmin_glb_lt := Z.min_glb_lt (compat "8.6").
+Notation Zmin_case := Z.min_case (compat "8.7").
+Notation Zmin_case_strong := Z.min_case_strong (compat "8.7").
+Notation Zle_min_l := Z.le_min_l (compat "8.7").
+Notation Zle_min_r := Z.le_min_r (compat "8.7").
+Notation Zmin_glb := Z.min_glb (compat "8.7").
+Notation Zmin_glb_lt := Z.min_glb_lt (compat "8.7").
Notation Zle_min_compat_r := Z.min_le_compat_r (only parsing).
Notation Zle_min_compat_l := Z.min_le_compat_l (only parsing).
Notation Zmin_idempotent := Z.min_id (only parsing).
Notation Zmin_n_n := Z.min_id (only parsing).
-Notation Zmin_comm := Z.min_comm (compat "8.6").
-Notation Zmin_assoc := Z.min_assoc (compat "8.6").
+Notation Zmin_comm := Z.min_comm (compat "8.7").
+Notation Zmin_assoc := Z.min_assoc (compat "8.7").
Notation Zmin_irreducible_inf := Z.min_dec (only parsing).
-Notation Zsucc_min_distr := Z.succ_min_distr (compat "8.6").
+Notation Zsucc_min_distr := Z.succ_min_distr (compat "8.7").
Notation Zmin_SS := Z.succ_min_distr (only parsing).
Notation Zplus_min_distr_r := Z.add_min_distr_r (only parsing).
Notation Zmin_plus := Z.add_min_distr_r (only parsing).
diff --git a/theories/ZArith/Znumtheory.v b/theories/ZArith/Znumtheory.v
index f5444c31..e6066d53 100644
--- a/theories/ZArith/Znumtheory.v
+++ b/theories/ZArith/Znumtheory.v
@@ -27,20 +27,20 @@ Open Scope Z_scope.
- properties of the efficient [Z.gcd] function
*)
-Notation Zgcd := Z.gcd (compat "8.6").
-Notation Zggcd := Z.ggcd (compat "8.6").
-Notation Zggcd_gcd := Z.ggcd_gcd (compat "8.6").
-Notation Zggcd_correct_divisors := Z.ggcd_correct_divisors (compat "8.6").
-Notation Zgcd_divide_l := Z.gcd_divide_l (compat "8.6").
-Notation Zgcd_divide_r := Z.gcd_divide_r (compat "8.6").
-Notation Zgcd_greatest := Z.gcd_greatest (compat "8.6").
-Notation Zgcd_nonneg := Z.gcd_nonneg (compat "8.6").
-Notation Zggcd_opp := Z.ggcd_opp (compat "8.6").
+Notation Zgcd := Z.gcd (compat "8.7").
+Notation Zggcd := Z.ggcd (compat "8.7").
+Notation Zggcd_gcd := Z.ggcd_gcd (compat "8.7").
+Notation Zggcd_correct_divisors := Z.ggcd_correct_divisors (compat "8.7").
+Notation Zgcd_divide_l := Z.gcd_divide_l (compat "8.7").
+Notation Zgcd_divide_r := Z.gcd_divide_r (compat "8.7").
+Notation Zgcd_greatest := Z.gcd_greatest (compat "8.7").
+Notation Zgcd_nonneg := Z.gcd_nonneg (compat "8.7").
+Notation Zggcd_opp := Z.ggcd_opp (compat "8.7").
(** The former specialized inductive predicate [Z.divide] is now
a generic existential predicate. *)
-Notation Zdivide := Z.divide (compat "8.6").
+Notation Zdivide := Z.divide (compat "8.7").
(** Its former constructor is now a pseudo-constructor. *)
@@ -48,7 +48,7 @@ Definition Zdivide_intro a b q (H:b=q*a) : Z.divide a b := ex_intro _ q H.
(** Results concerning divisibility*)
-Notation Zdivide_refl := Z.divide_refl (compat "8.6").
+Notation Zdivide_refl := Z.divide_refl (compat "8.7").
Notation Zone_divide := Z.divide_1_l (only parsing).
Notation Zdivide_0 := Z.divide_0_r (only parsing).
Notation Zmult_divide_compat_l := Z.mul_divide_mono_l (only parsing).
@@ -97,8 +97,8 @@ Notation Zdivide_1 := Z.divide_1_r (only parsing).
(** If [a] divides [b] and [b] divides [a] then [a] is [b] or [-b]. *)
-Notation Zdivide_antisym := Z.divide_antisym (compat "8.6").
-Notation Zdivide_trans := Z.divide_trans (compat "8.6").
+Notation Zdivide_antisym := Z.divide_antisym (compat "8.7").
+Notation Zdivide_trans := Z.divide_trans (compat "8.7").
(** If [a] divides [b] and [b<>0] then [|a| <= |b|]. *)
@@ -800,7 +800,7 @@ Proof.
rewrite <- Zdivide_Zdiv_eq; auto.
Qed.
-Notation Zgcd_comm := Z.gcd_comm (compat "8.6").
+Notation Zgcd_comm := Z.gcd_comm (compat "8.7").
Lemma Zgcd_ass a b c : Z.gcd (Z.gcd a b) c = Z.gcd a (Z.gcd b c).
Proof.
diff --git a/theories/ZArith/Zorder.v b/theories/ZArith/Zorder.v
index a1ec4b35..208e84ae 100644
--- a/theories/ZArith/Zorder.v
+++ b/theories/ZArith/Zorder.v
@@ -66,10 +66,10 @@ Qed.
(** * Relating strict and large orders *)
-Notation Zgt_lt := Z.gt_lt (compat "8.6").
-Notation Zlt_gt := Z.lt_gt (compat "8.6").
-Notation Zge_le := Z.ge_le (compat "8.6").
-Notation Zle_ge := Z.le_ge (compat "8.6").
+Notation Zgt_lt := Z.gt_lt (compat "8.7").
+Notation Zlt_gt := Z.lt_gt (compat "8.7").
+Notation Zge_le := Z.ge_le (compat "8.7").
+Notation Zle_ge := Z.le_ge (compat "8.7").
Notation Zgt_iff_lt := Z.gt_lt_iff (only parsing).
Notation Zge_iff_le := Z.ge_le_iff (only parsing).
@@ -123,7 +123,7 @@ Qed.
(** Reflexivity *)
-Notation Zle_refl := Z.le_refl (compat "8.6").
+Notation Zle_refl := Z.le_refl (compat "8.7").
Notation Zeq_le := Z.eq_le_incl (only parsing).
Hint Resolve Z.le_refl: zarith.
@@ -143,7 +143,7 @@ Qed.
(** Irreflexivity *)
-Notation Zlt_irrefl := Z.lt_irrefl (compat "8.6").
+Notation Zlt_irrefl := Z.lt_irrefl (compat "8.7").
Notation Zlt_not_eq := Z.lt_neq (only parsing).
Lemma Zgt_irrefl n : ~ n > n.
@@ -167,7 +167,7 @@ Notation Zle_or_lt := Z.le_gt_cases (only parsing).
(** Transitivity of strict orders *)
-Notation Zlt_trans := Z.lt_trans (compat "8.6").
+Notation Zlt_trans := Z.lt_trans (compat "8.7").
Lemma Zgt_trans n m p : n > m -> m > p -> n > p.
Proof.
@@ -176,8 +176,8 @@ Qed.
(** Mixed transitivity *)
-Notation Zlt_le_trans := Z.lt_le_trans (compat "8.6").
-Notation Zle_lt_trans := Z.le_lt_trans (compat "8.6").
+Notation Zlt_le_trans := Z.lt_le_trans (compat "8.7").
+Notation Zle_lt_trans := Z.le_lt_trans (compat "8.7").
Lemma Zle_gt_trans n m p : m <= n -> m > p -> n > p.
Proof.
@@ -191,7 +191,7 @@ Qed.
(** Transitivity of large orders *)
-Notation Zle_trans := Z.le_trans (compat "8.6").
+Notation Zle_trans := Z.le_trans (compat "8.7").
Lemma Zge_trans n m p : n >= m -> m >= p -> n >= p.
Proof.
@@ -257,8 +257,8 @@ Qed.
(** Relating strict and large order using successor or predecessor *)
-Notation Zlt_succ_r := Z.lt_succ_r (compat "8.6").
-Notation Zle_succ_l := Z.le_succ_l (compat "8.6").
+Notation Zlt_succ_r := Z.lt_succ_r (compat "8.7").
+Notation Zle_succ_l := Z.le_succ_l (compat "8.7").
Lemma Zgt_le_succ n m : m > n -> Z.succ n <= m.
Proof.
@@ -336,8 +336,8 @@ Qed.
(** Special cases of ordered integers *)
-Notation Zlt_0_1 := Z.lt_0_1 (compat "8.6").
-Notation Zle_0_1 := Z.le_0_1 (compat "8.6").
+Notation Zlt_0_1 := Z.lt_0_1 (compat "8.7").
+Notation Zle_0_1 := Z.le_0_1 (compat "8.7").
Lemma Zle_neg_pos : forall p q:positive, Zneg p <= Zpos q.
Proof.
diff --git a/theories/ZArith/Zpow_facts.v b/theories/ZArith/Zpow_facts.v
index a9bc5bd0..881ead1c 100644
--- a/theories/ZArith/Zpow_facts.v
+++ b/theories/ZArith/Zpow_facts.v
@@ -233,7 +233,7 @@ Qed.
(** * Z.square: a direct definition of [z^2] *)
-Notation Psquare := Pos.square (compat "8.6").
-Notation Zsquare := Z.square (compat "8.6").
+Notation Psquare := Pos.square (compat "8.7").
+Notation Zsquare := Z.square (compat "8.7").
Notation Psquare_correct := Pos.square_spec (only parsing).
Notation Zsquare_correct := Z.square_spec (only parsing).
diff --git a/theories/ZArith/Zquot.v b/theories/ZArith/Zquot.v
index e93ebb1a..264109dc 100644
--- a/theories/ZArith/Zquot.v
+++ b/theories/ZArith/Zquot.v
@@ -8,7 +8,7 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-Require Import Nnat ZArith_base ROmega ZArithRing Zdiv Morphisms.
+Require Import Nnat ZArith_base Lia ZArithRing Zdiv Morphisms.
Local Open Scope Z_scope.
@@ -37,17 +37,17 @@ Notation Ndiv_Zquot := N2Z.inj_quot (only parsing).
Notation Nmod_Zrem := N2Z.inj_rem (only parsing).
Notation Z_quot_rem_eq := Z.quot_rem' (only parsing).
Notation Zrem_lt := Z.rem_bound_abs (only parsing).
-Notation Zquot_unique := Z.quot_unique (compat "8.6").
-Notation Zrem_unique := Z.rem_unique (compat "8.6").
-Notation Zrem_1_r := Z.rem_1_r (compat "8.6").
-Notation Zquot_1_r := Z.quot_1_r (compat "8.6").
-Notation Zrem_1_l := Z.rem_1_l (compat "8.6").
-Notation Zquot_1_l := Z.quot_1_l (compat "8.6").
-Notation Z_quot_same := Z.quot_same (compat "8.6").
+Notation Zquot_unique := Z.quot_unique (compat "8.7").
+Notation Zrem_unique := Z.rem_unique (compat "8.7").
+Notation Zrem_1_r := Z.rem_1_r (compat "8.7").
+Notation Zquot_1_r := Z.quot_1_r (compat "8.7").
+Notation Zrem_1_l := Z.rem_1_l (compat "8.7").
+Notation Zquot_1_l := Z.quot_1_l (compat "8.7").
+Notation Z_quot_same := Z.quot_same (compat "8.7").
Notation Z_quot_mult := Z.quot_mul (only parsing).
-Notation Zquot_small := Z.quot_small (compat "8.6").
-Notation Zrem_small := Z.rem_small (compat "8.6").
-Notation Zquot2_quot := Zquot2_quot (compat "8.6").
+Notation Zquot_small := Z.quot_small (compat "8.7").
+Notation Zrem_small := Z.rem_small (compat "8.7").
+Notation Zquot2_quot := Zquot2_quot (compat "8.7").
(** Particular values taken for [a÷0] and [(Z.rem a 0)].
We avise to not rely on these arbitrary values. *)
@@ -129,33 +129,33 @@ Qed.
Theorem Zrem_lt_pos a b : 0<=a -> b<>0 -> 0 <= Z.rem a b < Z.abs b.
Proof.
intros; generalize (Z.rem_nonneg a b) (Z.rem_bound_abs a b);
- romega with *.
+ lia.
Qed.
Theorem Zrem_lt_neg a b : a<=0 -> b<>0 -> -Z.abs b < Z.rem a b <= 0.
Proof.
intros; generalize (Z.rem_nonpos a b) (Z.rem_bound_abs a b);
- romega with *.
+ lia.
Qed.
Theorem Zrem_lt_pos_pos a b : 0<=a -> 0<b -> 0 <= Z.rem a b < b.
Proof.
- intros; generalize (Zrem_lt_pos a b); romega with *.
+ intros; generalize (Zrem_lt_pos a b); lia.
Qed.
Theorem Zrem_lt_pos_neg a b : 0<=a -> b<0 -> 0 <= Z.rem a b < -b.
Proof.
- intros; generalize (Zrem_lt_pos a b); romega with *.
+ intros; generalize (Zrem_lt_pos a b); lia.
Qed.
Theorem Zrem_lt_neg_pos a b : a<=0 -> 0<b -> -b < Z.rem a b <= 0.
Proof.
- intros; generalize (Zrem_lt_neg a b); romega with *.
+ intros; generalize (Zrem_lt_neg a b); lia.
Qed.
Theorem Zrem_lt_neg_neg a b : a<=0 -> b<0 -> b < Z.rem a b <= 0.
Proof.
- intros; generalize (Zrem_lt_neg a b); romega with *.
+ intros; generalize (Zrem_lt_neg a b); lia.
Qed.
@@ -171,12 +171,12 @@ 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 <-(Z.mul_opp_opp). apply Z.mul_nonneg_nonneg; romega.
+ - lia.
+ - lia.
+ - rewrite <-(Z.mul_opp_opp). apply Z.mul_nonneg_nonneg; lia.
- assert (0 <= Z.sgn r * Z.sgn a).
{ rewrite <-Z.sgn_mul, Z.sgn_nonneg; auto. }
- destruct r; simpl Z.sgn in *; romega with *.
+ destruct r; simpl Z.sgn in *; lia.
Qed.
Theorem Zquot_mod_unique_full a b q r :
@@ -185,7 +185,7 @@ Proof.
destruct 1 as [(H,H0)|(H,H0)]; intros.
apply Zdiv_mod_unique with b; auto.
apply Zrem_lt_pos; auto.
- romega with *.
+ lia.
rewrite <- H1; apply Z.quot_rem'.
rewrite <- (Z.opp_involutive a).
@@ -193,7 +193,7 @@ Proof.
generalize (Zdiv_mod_unique b (-q) (-a÷b) (-r) (Z.rem (-a) b)).
generalize (Zrem_lt_pos (-a) b).
rewrite <-Z.quot_rem', Z.mul_opp_r, <-Z.opp_add_distr, <-H1.
- romega with *.
+ lia.
Qed.
Theorem Zquot_unique_full a b q r :
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-18 08:55:08 +0000