proposition: Theorem Zmin_Zmax : forall z1 z2 : Z, (Z.min z1 z2 <= Zmax z1 z2)%Z.
proof: Proof. intros z1 z2; case (Zle_or_lt z1 z2); unfold Z.le, Z.lt, Z.min, Zmax in |- *; CaseEq (z1 ?= z2)%Z; auto; intros H1 H2; try rewrite H1; try rewrite H2; red in |- *; intros; discriminate. Qed.
imports: Reals ZArith List PeanoNat Psatz