Require Export BinInt Zcompare Zorder.

Local Open Scope Z_scope.

Definition Zmax_case := Z.max_case.
Definition Zmax_case_strong := Z.max_case_strong.

Lemma Zmax_spec x y :
  x >= y /\ Z.max x y = x \/ x < y /\ Z.max x y = y.

Lemma Zmax_left n m : n>=m -> Z.max n m = n.

Lemma Zmax_right : forall n m, n<=m -> Z.max n m = m.

Lemma Zle_max_l : forall n m, n <= Z.max n m. Lemma Zle_max_r : forall n m, m <= Z.max n m. Lemma Zmax_lub : forall n m p, n <= p -> m <= p -> Z.max n m <= p.
Lemma Zmax_lub_lt : forall n m p:Z, n < p -> m < p -> Z.max n m < p.

Lemma Zle_max_compat_r : forall n m p, n <= m -> Z.max n p <= Z.max m p.
Lemma Zle_max_compat_l : forall n m p, n <= m -> Z.max p n <= Z.max p m.

Lemma Zmax_idempotent : forall n, Z.max n n = n. Lemma Zmax_comm : forall n m, Z.max n m = Z.max m n. Lemma Zmax_assoc : forall n m p, Z.max n (Z.max m p) = Z.max (Z.max n m) p.

Lemma Zmax_irreducible_dec : forall n m, {Z.max n m = n} + {Z.max n m = m}.
Lemma Zmax_le_prime : forall n m p, p <= Z.max n m -> p <= n \/ p <= m.

Lemma Zsucc_max_distr :
  forall n m, Z.succ (Z.max n m) = Z.max (Z.succ n) (Z.succ m).
Lemma Zplus_max_distr_l : forall n m p, Z.max (p + n) (p + m) = p + Z.max n m.
Lemma Zplus_max_distr_r : forall n m p, Z.max (n + p) (m + p) = Z.max n m + p.

Lemma Zpos_max p q : Zpos (Pos.max p q) = Z.max (Zpos p) (Zpos q).

Lemma Zpos_max_1 p : Z.max 1 (Zpos p) = Zpos p.

Lemma Zpos_minus p q : Zpos (p - q) = Z.max 1 (Zpos p - Zpos q).