On nat, the sets {0..n} and {..n} are the same, which can be irksome.
Hence I discourage the use of {..n}. However, there are notations such
as "SUM k<=n. t" which stand for "setsum (%k. t) {..n}" and introduce
{..n} by the backdoor.I am tempted to get rid of this and related notations and restrict to the canonical "SUM k=a..b. t". Would anybody miss the "k<=n" variant? Potential problem: for other types, eg int, k<=i cannot be replaced by some "k=a..i". But "SUM k<=i", "UN k<=i" over int (let alone real) seem unusual. Feelings? Tobias
