Definition interpolate
  (x : R)
  (y : R)
  (f : R)
: R :=
  (x * (1 - f)) + (y * f).
