Library Coq.ZArith.Zminmax


Require Import Zmin Zmax.
Require Import BinInt Zorder.

Open Local Scope Z_scope.

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

Lemma max_min_disassoc : forall n m p, Zmin n (Zmax m p) <= Zmax (Zmin n m) p.