Detailed proofs of Lebesgue integration, to be formalized in Coq.

The full code is downloadable here for Coq >= 8.8.2 .

Browsable files below.