Definition keyAssignmentEvaluateAmplitudeForVelocity
  (velocity   : R)
  (assignment : keyAssignment)
: R :=
  let kLow := kaAtVelocityStart assignment in
  let kMid := kaAtVelocityCenter assignment in
  let kTop := kaAtVelocityEnd assignment in
    match Rcompare velocity kMid with
    | Eq => kaAmplitudeAtVelocityCenter assignment
    | Lt =>
      match Rlt_dec kLow kMid with
      | left _ =>
        let f := between velocity kLow kMid in
          interpolate
            (kaAmplitudeAtVelocityStart assignment)
            (kaAmplitudeAtVelocityCenter assignment)
            f
      | right _ =>
          (kaAmplitudeAtVelocityCenter assignment)
      end
    | Gt =>
      match Rlt_dec kMid kTop with
      | left _ =>
        let f := between velocity kMid kTop in
          interpolate
            (kaAmplitudeAtVelocityCenter assignment)
            (kaAmplitudeAtVelocityEnd assignment)
            f
      | right _ =>
          (kaAmplitudeAtVelocityCenter assignment)
      end
    end.
