Definition isS8 (z : Z) : Prop :=
  (s8Min <= z) /\ (z <= s8Max).
