Inductive cubeOffsetsSorted : list cubeMipMap -> Prop :=
  | CMMSizeOne  : forall m,
    cubeFaceExtent (cubeMapFaceXPos m) < cubeFaceOffset (cubeMapFaceXNeg m) ->
    cubeFaceExtent (cubeMapFaceXNeg m) < cubeFaceOffset (cubeMapFaceYPos m) ->
    cubeFaceExtent (cubeMapFaceYPos m) < cubeFaceOffset (cubeMapFaceYNeg m) ->
    cubeFaceExtent (cubeMapFaceYNeg m) < cubeFaceOffset (cubeMapFaceZPos m) ->
    cubeFaceExtent (cubeMapFaceZPos m) < cubeFaceOffset (cubeMapFaceZNeg m) ->
      cubeOffsetsSorted [m]
  | CMMSizeCons : forall mm0 mm1 mxs,
    cubeFaceExtent (cubeMapFaceZNeg mm1) < cubeFaceOffset (cubeMapFaceXPos mm0) ->
      cubeOffsetsSorted (mm0 :: mxs) ->
        cubeOffsetsSorted (mm1 :: mm0 :: mxs).
