Definition isS16 (z : Z) : Prop :=
  (s16Min <= z) /\ (z <= s16Max).
