diff options
Diffstat (limited to 'theories/ZArith/Zmax.v')
-rw-r--r-- | theories/ZArith/Zmax.v | 38 |
1 files changed, 19 insertions, 19 deletions
diff --git a/theories/ZArith/Zmax.v b/theories/ZArith/Zmax.v index e6582a775..53c40ae7d 100644 --- a/theories/ZArith/Zmax.v +++ b/theories/ZArith/Zmax.v @@ -20,13 +20,13 @@ Open Local Scope Z_scope. (** * Characterization of maximum on binary integer numbers *) -Definition Zmax_case := Zmax_case. -Definition Zmax_case_strong := Zmax_case_strong. +Definition Zmax_case := Z.max_case. +Definition Zmax_case_strong := Z.max_case_strong. Lemma Zmax_spec : forall x y, x >= y /\ Zmax x y = x \/ x < y /\ Zmax x y = y. Proof. - intros x y. rewrite Zge_iff_le. destruct (Zmax_spec x y); auto. + intros x y. rewrite Zge_iff_le. destruct (Z.max_spec x y); auto. Qed. Lemma Zmax_left : forall n m, n>=m -> Zmax n m = n. @@ -36,60 +36,60 @@ Definition Zmax_right : forall n m, n<=m -> Zmax n m = m := Zmax_r. (** * Least upper bound properties of max *) -Definition Zle_max_l : forall n m, n <= Zmax n m := Zle_max_l. -Definition Zle_max_r : forall n m, m <= Zmax n m := Zle_max_r. +Definition Zle_max_l : forall n m, n <= Zmax n m := Z.le_max_l. +Definition Zle_max_r : forall n m, m <= Zmax n m := Z.le_max_r. Definition Zmax_lub : forall n m p, n <= p -> m <= p -> Zmax n m <= p - := Zmax_lub. + := Z.max_lub. Definition Zmax_lub_lt : forall n m p:Z, n < p -> m < p -> Zmax n m < p - := Zmax_lub_lt. + := Z.max_lub_lt. (** * Compatibility with order *) Definition Zle_max_compat_r : forall n m p, n <= m -> Zmax n p <= Zmax m p - := Zmax_le_compat_r. + := Z.max_le_compat_r. Definition Zle_max_compat_l : forall n m p, n <= m -> Zmax p n <= Zmax p m - := Zmax_le_compat_l. + := Z.max_le_compat_l. (** * Semi-lattice properties of max *) -Definition Zmax_idempotent : forall n, Zmax n n = n := Zmax_id. -Definition Zmax_comm : forall n m, Zmax n m = Zmax m n := Zmax_comm. +Definition Zmax_idempotent : forall n, Zmax n n = n := Z.max_id. +Definition Zmax_comm : forall n m, Zmax n m = Zmax m n := Z.max_comm. Definition Zmax_assoc : forall n m p, Zmax n (Zmax m p) = Zmax (Zmax n m) p - := Zmax_assoc. + := Z.max_assoc. (** * Additional properties of max *) Lemma Zmax_irreducible_dec : forall n m, {Zmax n m = n} + {Zmax n m = m}. -Proof. exact Zmax_dec. Qed. +Proof. exact Z.max_dec. Qed. Definition Zmax_le_prime : forall n m p, p <= Zmax n m -> p <= n \/ p <= m - := Zmax_le. + := Z.max_le. (** * Operations preserving max *) Definition Zsucc_max_distr : forall n m:Z, Zsucc (Zmax n m) = Zmax (Zsucc n) (Zsucc m) - := Zsucc_max_distr. + := Z.succ_max_distr. Definition Zplus_max_distr_l : forall n m p:Z, Zmax (p + n) (p + m) = p + Zmax n m - := Zplus_max_distr_l. + := Z.plus_max_distr_l. Definition Zplus_max_distr_r : forall n m p:Z, Zmax (n + p) (m + p) = Zmax n m + p - := Zplus_max_distr_r. + := Z.plus_max_distr_r. (** * Maximum and Zpos *) Definition Zpos_max : forall p q, Zpos (Pmax p q) = Zmax (Zpos p) (Zpos q) - := Zpos_max. + := Z.pos_max. Definition Zpos_max_1 : forall p, Zmax 1 (Zpos p) = Zpos p - := Zpos_max_1. + := Z.pos_max_1. (** * Characterization of Pminus in term of Zminus and Zmax *) |