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