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