of the Lebesgue scheme that is now obsolete.

Add measurability or not?

(This is presumably its only application.)

Define meas_swap and prove LInt_p_swap by using LInt_p_meas_image.

(measurable_fun.v) Add incr_fun_seq, measurable_fun_seq_Rbar,
  Mplus, Mplus_finite, Mplus_seq, Mplus_ext, Mplus_seq_ext,
  many Mplus_* lemmas.

(simple_fun.v) Add SFplus_Mplus.

And use them!

(Locally) define and use predicates P0 and P.
Compact some proof using previous results.

_ge_0 _empty -> _nonneg
_False -> _emptyset

Use emptyset and nonneg.

Section for iterated integrals (but without a proper definition).

meas_prod -> muX1xX2 (local def).

Proofs of diffuseness.

Use already defined property is_product_measure.
Proofs remain basically unchanged (only one unfold of each had to be added).

Add minimal doc for each section.

Some renaming.
Properties of XXX have a name starting with prefix XXX_.
meas_prod -> prod_meas.
_measurable_fun -> _measurable.

Proofs of Tonelli_aux1 are now crystal clear! ;)

*_seq'* -> *_seq_Rbar*

Diff' -> Compl_loc
_iff -> _equiv

for all 3 cases.