Library Coq.NArith.Nminmax
Local Open Scope N_scope.
The functions Nmax and Nmin implement indeed
a maximum and a minimum
Lemma Nmax_l : forall x y, y<=x -> Nmax x y = x.
Lemma Nmax_r : forall x y, x<=y -> Nmax x y = y.
Lemma Nmin_l : forall x y, x<=y -> Nmin x y = x.
Lemma Nmin_r : forall x y, y<=x -> Nmin x y = y.
Module NHasMinMax <: HasMinMax N_as_OT.
Definition max := Nmax.
Definition min := Nmin.
Definition max_l := Nmax_l.
Definition max_r := Nmax_r.
Definition min_l := Nmin_l.
Definition min_r := Nmin_r.
End NHasMinMax.
Module N.
We obtain hence all the generic properties of max and min.
Simplifications
Lemma max_0_l : forall n, Nmax 0 n = n.
Lemma max_0_r : forall n, Nmax n 0 = n.
Lemma min_0_l : forall n, Nmin 0 n = 0.
Lemma min_0_r : forall n, Nmin n 0 = 0.
Compatibilities (consequences of monotonicity)
Lemma succ_max_distr :
forall n m, Nsucc (Nmax n m) = Nmax (Nsucc n) (Nsucc m).
Lemma succ_min_distr : forall n m, Nsucc (Nmin n m) = Nmin (Nsucc n) (Nsucc m).
Lemma plus_max_distr_l : forall n m p, Nmax (p + n) (p + m) = p + Nmax n m.
Lemma plus_max_distr_r : forall n m p, Nmax (n + p) (m + p) = Nmax n m + p.
Lemma plus_min_distr_l : forall n m p, Nmin (p + n) (p + m) = p + Nmin n m.
Lemma plus_min_distr_r : forall n m p, Nmin (n + p) (m + p) = Nmin n m + p.
End N.