proposition: Theorem Zmin_Zle : forall z1 z2 z3 : Z, (z1 <= z2)%Z -> (z1 <= z3)%Z -> (z1 <= Z.min z2 z3)%Z.
proof: Proof. intros z1 z2 z3 H' H'0; unfold Z.min in |- *. case (z2 ?= z3)%Z; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz