Definition arrayMipMapImageDataSizeTotal (m : arrayMipMapList) : nat :=
  arrayMipMapImageDataSizeTotalAux (arrayMipMaps m).
