Worst-case risk dominates Expected Shortfall at every depth

RETIRED. This statement is subsumed by CoherentRisk.es_antitone, which proves that Expected Shortfall is decreasing in the depth for every pair of depths. Taking the shallower depth to be $0$ and combining with CoherentRisk.es_zero_eq_worstCase, which identifies Expected Shortfall at depth $0$ with the worst-case measure, recovers exactly the bound below. It is retired as redundant rather than as incorrect: the statement is true and its proof stands. Prefer CoherentRisk.es_antitone for new work.

At every depth $m$, Expected Shortfall reports at most as much risk as the worst-case measure. Averaging the losses over a group of $m+1$ bad states can never exceed the single largest loss, so worstCase is the most conservative member of the family.

When this was published, full monotonicity in the depth was not yet proved, and the statement recorded explicitly that it was the weaker claim. That gap has since been closed by CoherentRisk.es_antitone.

As throughout CoherentRisk, the development counts states and refers to no probability measure, so $m$ is an integer depth rather than a confidence level.