Fixpoint arrayMipMapImageDataSizeTotalAux (m : list arrayMipMap) : nat :=
  match m with
  | []        => 0
  | (x :: []) => (arrayMipMapOffset x) + (arrayMipMapSizeCompressed x)
  | (x :: xs) => arrayMipMapImageDataSizeTotalAux xs
  end.
