Definition isS32 (z : Z) : Prop :=
  (s32Min <= z) /\ (z <= s32Max).
