Theorem betweenNorm : forall x lo hi,
  lo < hi
    -> lo <= x <= hi
      -> isNormalized (between x lo hi).
Proof.
  (* Proof omitted for brevity; see Interpolation.v for proofs. *)
Qed.
