# Library Coq.ZArith.Zminmax

Require Import Orders BinInt Zcompare Zorder ZOrderedType
GenericMinMax.

# Maximum and Minimum of two Z numbers

Local Open Scope Z_scope.
The functions Zmax and Zmin implement indeed a maximum and a minimum
Lemma Zmax_l : forall x y, y <= x -> Zmax x y = x.
Lemma Zmax_r : forall x y, x <= y -> Zmax x y = y.
Lemma Zmin_l : forall x y, x <= y -> Zmin x y = x.
Lemma Zmin_r : forall x y, y <= x -> Zmin x y = y.
Module ZHasMinMax <: HasMinMax Z_as_OT.
Definition max := Zmax.
Definition min := Zmin.
Definition max_l := Zmax_l.
Definition max_r := Zmax_r.
Definition min_l := Zmin_l.
Definition min_r := Zmin_r.
End ZHasMinMax.
Module Z.
We obtain hence all the generic properties of max and min.
Include UsualMinMaxProperties Z_as_OT ZHasMinMax.

# Properties specific to the Z domain

Compatibilities (consequences of monotonicity)
Lemma plus_max_distr_l : forall n m p, Zmax (p + n) (p + m) = p + Zmax n m.
Lemma plus_max_distr_r : forall n m p, Zmax (n + p) (m + p) = Zmax n m + p.
Lemma plus_min_distr_l : forall n m p, Zmin (p + n) (p + m) = p + Zmin n m.
Lemma plus_min_distr_r : forall n m p, Zmin (n + p) (m + p) = Zmin n m + p.
Lemma succ_max_distr : forall n m, Zsucc (Zmax n m) = Zmax (Zsucc n) (Zsucc m).
Lemma succ_min_distr : forall n m, Zsucc (Zmin n m) = Zmin (Zsucc n) (Zsucc m).
Lemma pred_max_distr : forall n m, Zpred (Zmax n m) = Zmax (Zpred n) (Zpred m).
Lemma pred_min_distr : forall n m, Zsucc (Zmin n m) = Zmin (Zsucc n) (Zsucc m).
Anti-monotonicity swaps the role of min and max
Lemma opp_max_distr : forall n m : Z, -( Zmax n m ) = Zmin (- n) (- m).
Lemma opp_min_distr : forall n m : Z, - ( Zmin n m ) = Zmax (- n) (- m).
Lemma minus_max_distr_l : forall n m p, Zmax (p - n) (p - m) = p - Zmin n m.
Lemma minus_max_distr_r : forall n m p, Zmax (n - p) (m - p) = Zmax n m - p.
Lemma minus_min_distr_l : forall n m p, Zmin (p - n) (p - m) = p - Zmax n m.
Lemma minus_min_distr_r : forall n m p, Zmin (n - p) (m - p) = Zmin n m - p.
Compatibility with Zpos
Lemma pos_max : forall p q, Zpos (Pmax p q) = Zmax (Zpos p) (Zpos q).
Lemma pos_min : forall p q, Zpos (Pmin p q) = Zmin (Zpos p) (Zpos q).
Lemma pos_max_1 : forall p, Zmax 1 (Zpos p) = Zpos p.
Lemma pos_min_1 : forall p, Zmin 1 (Zpos p) = 1.
End Z.

# Characterization of Pminus in term of Zminus and Zmax

Lemma Zpos_minus : forall p q, Zpos (Pminus p q) = Zmax 1 (Zpos p - Zpos q).