Library Stdlib.ZArith.Zmax

From Stdlib Require Export BinInt Zcompare Zorder.

#[local] Open Scope Z_scope.

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 Zpos_max_1 p : Z.max 1 (Z.pos p) = Z.pos p.