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).

Require Import Arith_base.
Require Import BinInt.
Require Import Zcompare.
Require Import Zorder.

Open Local Scope Z_scope.

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


Lemma Zle_min_l : forall n m:Z, Zmin n m <= n.

Lemma Zle_min_r : forall n m:Z, Zmin n m <= m.

Lemma Zmin_glb : forall n m p:Z, p <= n -> p <= m -> p <= Zmin n m.

Semi-lattice properties of min


Lemma Zmin_idempotent : forall n:Z, Zmin n n = n.

Notation Zmin_n_n := Zmin_idempotent (only parsing).

Lemma Zmin_comm : forall n m:Z, Zmin n m = Zmin m n.

Lemma Zmin_assoc : forall n m p:Z, Zmin n (Zmin m p) = Zmin (Zmin n m) p.

Additional properties of min


Lemma Zmin_irreducible_inf : forall n m:Z, {Zmin n m = n} + {Zmin n m = m}.

Lemma Zmin_irreducible : forall n m:Z, Zmin n m = n \/ Zmin n m = m.

Notation Zmin_or := Zmin_irreducible (only parsing).

Lemma Zmin_le_prime_inf : forall n m p:Z, Zmin n m <= p -> {n <= p} + {m <= p}.

Operations preserving min


Lemma Zsucc_min_distr :
  forall n m:Z, Zsucc (Zmin n m) = Zmin (Zsucc n) (Zsucc m).

Notation Zmin_SS := Zsucc_min_distr (only parsing).

Lemma Zplus_min_distr_r : forall n m p:Z, Zmin (n + p) (m + p) = Zmin n m + p.

Notation Zmin_plus := Zplus_min_distr_r (only parsing).

Minimum and Zpos


Lemma Zpos_min : forall p q, Zpos (Pmin p q) = Zmin (Zpos p) (Zpos q).