tentative formalization of Vitali's lemma

[affeldt-aist]

Motivation for this change

track C of issue #965

(statements are being tested in other branches, to clean as soon as it stabilized)

Things done/to do

• added corresponding entries in CHANGELOG_UNRELEASED.md

• added corresponding documentation in the headers

Compatibility with MathComp 2.0

• I added the label TODO: HB port to make sure someone ports this PR to
  the hierarchy-builder branch or I already opened an issue or PR (please cross reference).

Automatic note to reviewers

Read this Checklist and put a milestone if possible.

[zstone1]

Overall this looks great. I've posted a couple questions here, but nothing deep. And I haven't looked thoroughly at the vitali lemma proof itself. But the structure seems fairly reasonable.

[affeldt-aist]

I still have to write the changelog and double-check the documentation,
but, modulo these two points, I'd like to have some light-review asap and
an approval to merge: if there are minor problems we will still have an
opportunity to fix them soon since at least two forthcoming PRs depend
on this one (and it is painful to systematically rebased PRs on PR for me...).

[affeldt-aist]

The main change with the original version is that we have introduced
a predicate is_ball so that family of balls can be represented by the
datatype I -> set R. That hasn't changed the structure of proofs, but
thanks to that we now have a function scall_ball from set to set
and we use closure to denote closed balls, which is closer to what
paper proofs look like.