InnerSimplify​(System.​Boolean)

The expansion first, because it answers any summand at all where the range is
short, and the closed form only a polynomial one. What the closed form then
reaches is the two cases the expansion declines: a symbolic bound, and a concrete
range too long to write out — where it is not a fallback but the better answer,
since it computes rather than expands.

A count comes before all of them: a sum of an Iverson bracket is the number of
indices its statement holds for, which is computed however long the range is, and in
a nested sum the count of the inner one is what the outer one sums.