Library Coq.NArith.Pminmax
Local Open Scope positive_scope.
The functions Pmax and Pmin implement indeed
a maximum and a minimum
Lemma Pmax_l : forall x y, y<=x -> Pmax x y = x.
Lemma Pmax_r : forall x y, x<=y -> Pmax x y = y.
Lemma Pmin_l : forall x y, x<=y -> Pmin x y = x.
Lemma Pmin_r : forall x y, y<=x -> Pmin x y = y.
Module PositiveHasMinMax <: HasMinMax Positive_as_OT.
Definition max := Pmax.
Definition min := Pmin.
Definition max_l := Pmax_l.
Definition max_r := Pmax_r.
Definition min_l := Pmin_l.
Definition min_r := Pmin_r.
End PositiveHasMinMax.
Module P.
We obtain hence all the generic properties of max and min.
Simplifications
Lemma max_1_l : forall n, Pmax 1 n = n.
Lemma max_1_r : forall n, Pmax n 1 = n.
Lemma min_1_l : forall n, Pmin 1 n = 1.
Lemma min_1_r : forall n, Pmin n 1 = 1.
Compatibilities (consequences of monotonicity)
Lemma succ_max_distr :
forall n m, Psucc (Pmax n m) = Pmax (Psucc n) (Psucc m).
Lemma succ_min_distr : forall n m, Psucc (Pmin n m) = Pmin (Psucc n) (Psucc m).
Lemma plus_max_distr_l : forall n m p, Pmax (p + n) (p + m) = p + Pmax n m.
Lemma plus_max_distr_r : forall n m p, Pmax (n + p) (m + p) = Pmax n m + p.
Lemma plus_min_distr_l : forall n m p, Pmin (p + n) (p + m) = p + Pmin n m.
Lemma plus_min_distr_r : forall n m p, Pmin (n + p) (m + p) = Pmin n m + p.
End P.