Definition clipFrameCountLoopRange
  (c  : clip)
  (lr : loopRange) 
: Prop :=
  (lrFrameEndInclusive lr) < (clipFrameCount c).
