Inductive arrayMipMapOffsetsSorted : list arrayMipMap -> Prop :=
  | AMMSizeOne  : forall m, arrayMipMapOffsetsSorted [m]
  | AMMSizeCons : forall mm0 mm1 mxs,
    ((arrayMipMapOffset mm1) + (arrayMipMapSizeCompressed mm1)) < (arrayMipMapOffset mm0) ->
      arrayMipMapOffsetsSorted (mm0 :: mxs) ->
        arrayMipMapOffsetsSorted (mm1 :: mm0 :: mxs).
