Library Coq.ZArith.Zminmax
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.
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