Definition keyAssignmentMatches
  (key        : nat)
  (velocity   : R)
  (assignment : keyAssignment)
: Prop :=
  let p0 := ((kaValueStart assignment) <= key)%nat in
  let p1 := (key <= (kaValueEnd assignment))%nat in
  let p2 := ((kaAtVelocityStart assignment) <= velocity)%R in
  let p3 := (velocity <= (kaAtVelocityEnd assignment))%R in
    p0 /\ p1 /\ p2 /\ p3.
