Definition mipMapImageDataSizeTotal (m : mipMapList) : nat :=
  mipMapImageDataSizeTotalAux (mipMaps m).
