Sharp bounds for sums of bounded finsets of integers #
The sum of a finset of integers with cardinality s
where all elements are at most c
can be given
a sharper upper bound than #s * c
, because the elements are distinct.
This file provides these sharp bounds, both in the upper-bounded and analogous lower-bounded cases.