proposition: Theorem ZmaxLe1 : forall z1 z2 : Z, (z1 <= Zmax z1 z2)%Z.
proof: Proof. intros z1 z2; unfold Zmax in |- *; CaseEq (z1 ?= z2)%Z; simpl in |- *; auto with zarith. unfold Z.le in |- *; intros H; rewrite H; red in |- *; intros; discriminate. rewrite Z.compare_lt_iff; auto with zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz