proposition: Theorem Zle_n_Zpred : forall z1 z2 : Z, (Z.pred z1 <= Z.pred z2)%Z -> (z1 <= z2)%Z.
proof: Proof. intros z1 z2 H; rewrite (Zsucc_pred z1); rewrite (Zsucc_pred z2); auto with zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz