Lemma interpolateRange1 : forall x y f,
  x <= y
    -> isNormalized f
      -> x <= interpolate x y f <= y.
Proof.
  (* Proof omitted for brevity; see Interpolation.v for proofs. *)
Qed.
