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
.