Definition cubeMipMapImageDataSizeTotal (m : cubeMipMapList) : nat :=
  cubeMipMapImageDataSizeTotalAux (cubeMipMaps m).
