Continuous functions are dense in L1

[zstone1]

Motivation for this change

The last piece of track B for #965.
The proof starts with an integrable function f

1. Approximate that with a simple function g via approximation_sfun_integrable
2. Use lusin's to get a compact region on which g is continuous.
3. Use tietzes (and simple -> bounded) to extend g over to a continuous approximation, h.
4. Chain these approximations together.

The proof could be factored out into more reusable components. However, having the topology for L1 is pretty important to make that work. Then we can circumvent most of the the boiler plate with

• A filter convergences in a metric spaces <-> a corresponding sequence converges
• Dense is transitive
  But without the Lp spaces defined, there's no great way to do this. I'm happy with things as they are now, mostly because I want to keep pushing towards FTC.

@affeldt-aist Is this phrasing of density ok? It's pretty easy to convert to one about (forall eps, exists N, ...) by applying cvg_ballP and fine_fcvg if that's easier for you.

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.

[affeldt-aist]

@affeldt-aist Is this phrasing of density ok?

I have yet to use the lemma in a complete application to be sure but so far it looks ok.