Fixpoint cubeMipMapImageDataSizeTotalAux (m : list cubeMipMap) : nat :=
  match m with
  | []        => 0
  | (x :: []) => cubeFaceExtent (cubeMapFaceZNeg x)
  | (x :: xs) => cubeMipMapImageDataSizeTotalAux xs
  end.
