Inductive clipsListOffsetIsSorted : list clip -> Prop :=
  | ClipOffsetOne : forall s,
    clipsListOffsetIsSorted [s]
  | ClipOffsetCons : forall s0 s1 ss,
    ((clipOffset s1) + (clipSize s1)) < clipOffset s0 ->
      clipsListOffsetIsSorted (s0 :: ss) ->
        clipsListOffsetIsSorted (s1 :: s0 :: ss).
