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