Definition arrayMipMapSize
  (level      : nat)
  (imageSize  : imageSize3D)
  (levelRange : 0 < level)
: option arrayMipMapImageSize :=
  let sx  := (sizeX imageSize) / 2 ^ level  in
  let sy  := (sizeY imageSize) / 2 ^ level  in
    match (Nat.ltb_spec0 1 sx, Nat.ltb_spec0 1 sy) with
    | (ReflectT _ xt, ReflectT _ yt) => Some (ArrayMipMapImageSize sx sy xt yt)
    | (_, _)                         => None
    end.
