Require Import BinInt Zcompare Zorder.

Local Open Scope Z_scope.

Definition Zmin_case := Z.min_case.
Definition Zmin_case_strong := Z.min_case_strong.

Lemma Zmin_spec x y :
  x <= y /\ Z.min x y = x \/ x > y /\ Z.min x y = y.

Lemma Zle_min_l : forall n m, Z.min n m <= n. Lemma Zle_min_r : forall n m, Z.min n m <= m. Lemma Zmin_glb : forall n m p, p <= n -> p <= m -> p <= Z.min n m.
Lemma Zmin_glb_lt : forall n m p, p < n -> p < m -> p < Z.min n m.

Lemma Zle_min_compat_r : forall n m p, n <= m -> Z.min n p <= Z.min m p.
Lemma Zle_min_compat_l : forall n m p, n <= m -> Z.min p n <= Z.min p m.

Lemma Zmin_idempotent : forall n, Z.min n n = n. Notation Zmin_n_n := Z.min_id (only parsing).
Lemma Zmin_comm : forall n m, Z.min n m = Z.min m n. Lemma Zmin_assoc : forall n m p, Z.min n (Z.min m p) = Z.min (Z.min n m) p.

Lemma Zmin_irreducible_inf : forall n m, {Z.min n m = n} + {Z.min n m = m}.
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 Zsucc_min_distr :
 forall n m, Z.succ (Z.min n m) = Z.min (Z.succ n) (Z.succ m).
Notation Zmin_SS := Z.succ_min_distr (only parsing).
Lemma Zplus_min_distr_r :
 forall n m p, Z.min (n + p) (m + p) = Z.min n m + p.
Notation Zmin_plus := Z.add_min_distr_r (only parsing).

Lemma Zpos_min p q : Zpos (Pos.min p q) = Z.min (Zpos p) (Zpos q).

Lemma Zpos_min_1 p : Z.min 1 (Zpos p) = 1.