Definition isS64 (z : Z) : Prop :=
  (s64Min <= z) /\ (z <= s64Max).
