use set instead of fset in esum

[affeldt-aist]

Motivation for this change

This PR defines esum using finite_set instead of fset.

TODO: ~- rename fsets~ (not sure anymore... maybe fsubsets?)

some small proofs become useless but on the other hand the following proofs got a bit longer esum_esum, nneseries_esum, reindex_esum, infinite_card_dirac

fyi @CohenCyril

also contains unrelated proofs shortenings related to {x,y}section

Things done/to do

• [x] added corresponding entries in CHANGELOG_UNRELEASED.md (do not edit former entries, only append new ones, be careful: merge and rebase have a tendency to mess up CHANGELOG_UNRELEASED.md)
• [ ] added corresponding documentation in the headers

Automatic note to reviewers

Read this Checklist and put a milestone if possible.