Inductive mipMapOffsetsSorted : list mipMap -> Prop :=
  | MMSizeOne  : forall m, mipMapOffsetsSorted [m]
  | MMSizeCons : forall mm0 mm1 mxs,
    ((mipMapOffset mm1) + (mipMapSizeCompressed mm1)) < (mipMapOffset mm0) ->
      mipMapOffsetsSorted (mm0 :: mxs) ->
        mipMapOffsetsSorted (mm1 :: mm0 :: mxs).
