Library Coq.ZArith.Zminmax
Lattice properties of min and max on Z
Absorption
Lemma Zmin_max_absorption_r_r : forall n m, Zmax n (Zmin n m) = n.
Lemma Zmax_min_absorption_r_r : forall n m, Zmin n (Zmax n m) = n.
Distributivity
Lemma Zmax_min_distr_r :
forall n m p, Zmax n (Zmin m p) = Zmin (Zmax n m) (Zmax n p).
Lemma Zmin_max_distr_r :
forall n m p, Zmin n (Zmax m p) = Zmax (Zmin n m) (Zmin n p).
Modularity
Lemma Zmax_min_modular_r :
forall n m p, Zmax n (Zmin m (Zmax n p)) = Zmin (Zmax n m) (Zmax n p).
Lemma Zmin_max_modular_r :
forall n m p, Zmin n (Zmax m (Zmin n p)) = Zmax (Zmin n m) (Zmin n p).
Disassociativity