Fixpoint mipMapImageDataSizeTotalAux (m : list mipMap) : nat :=
  match m with
  | []        => 0
  | (x :: []) => (mipMapOffset x) + (mipMapSizeCompressed x)
  | (x :: xs) => mipMapImageDataSizeTotalAux xs
  end.
