Theorem indexWithinRangeDecidable : forall e s,
  {0 <= e /\ e < s}+{~(0 <= e /\ e < s)}.
Proof.
  (** Proof omitted for brevity. *)
Qed.
