Library Coq.ZArith.Zmin
THIS FILE IS DEPRECATED.
Require
Import
BinInt
Zcompare
Zorder
.
Local Open
Scope
Z_scope
.
Definition
Z.min
is now
BinInt.Z.min
.
Exact compatibility
Notation
Zle_min_compat_r
:=
Z.min_le_compat_r
(
only
parsing
).
Notation
Zle_min_compat_l
:=
Z.min_le_compat_l
(
only
parsing
).
Notation
Zmin_idempotent
:=
Z.min_id
(
only
parsing
).
Notation
Zmin_n_n
:=
Z.min_id
(
only
parsing
).
Notation
Zmin_irreducible_inf
:=
Z.min_dec
(
only
parsing
).
Notation
Zmin_SS
:=
Z.succ_min_distr
(
only
parsing
).
Notation
Zplus_min_distr_r
:=
Z.add_min_distr_r
(
only
parsing
).
Notation
Zmin_plus
:=
Z.add_min_distr_r
(
only
parsing
).
Notation
Zpos_min
:=
Pos2Z.inj_min
(
only
parsing
).
Slightly different lemmas
Lemma
Zmin_spec
x
y
:
x
<=
y
/\
Z.min
x
y
=
x
\/
x
>
y
/\
Z.min
x
y
=
y
.
Lemma
Zmin_irreducible
n
m
:
Z.min
n
m
=
n
\/
Z.min
n
m
=
m
.
Notation
Zmin_or
:=
Zmin_irreducible
(
only
parsing
).
Lemma
Zmin_le_prime_inf
n
m
p
:
Z.min
n
m
<=
p
->
{
n
<=
p
}
+
{
m
<=
p
}
.
Lemma
Zpos_min_1
p
:
Z.min
1 (
Zpos
p
)
=
1.