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