Library Coq.ZArith.Zmin
Initial version from Pierre Crégut (CNET, Lannion, France), 1996.
Further extensions by the Coq development team, with suggestions
from Russell O'Connor (Radbout U., Nijmegen, The Netherlands).
Minimum on binary integer numbers
Characterization of the minimum on binary integer numbers
Lemma Zmin_case_strong :
forall (
n m:Z) (
P:Z ->
Type),
(
n<=m ->
P n) -> (
m<=n ->
P m) ->
P (
Zmin n m).
Lemma Zmin_case :
forall (
n m:Z) (
P:Z ->
Type),
P n ->
P m ->
P (
Zmin n m).
Lemma Zmin_spec :
forall x y:Z,
x <=
y /\
Zmin x y =
x \/
x >
y /\
Zmin x y =
y.
Greatest lower bound properties of min
Semi-lattice properties of min
Additional properties of min
Operations preserving min