# 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.

# 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).