chain: simple_fun -> Mp -> Lint_p.

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!

_ge_0 _empty -> _nonneg
_False -> _emptyset

Use emptyset and nonneg.

gen1 -> genE (gen2 useless).

Use genUxV local defs.
Use new swap.

Add equivalence between hypotheses of old and new versions of the Lebesgue scheme.
Prove old version from the new one using the equivalence (temporarily into Lebesgue_scheme').
Use new version to prove LInt_p_swap (bof-minus).

LInt_p_meas_imag_blop was actually measurable_fun_composition.
Mv LInt_p_Dirac at the end.

Cleaning.
Prove Lebesgue_scheme_step2 from Lebesgue_scheme_step2_alt.
Lebesgue_scheme_alt -> Lebesgue_scheme_new_alt.
Add lemma Lebesgue_scheme_new.

*_seq'* -> *_seq_Rbar*

Equivalence between hypotheses of both forms.

LInt_p_meas_imag_blop and LInt_p_meas_imag lemmas.

-add non negativity of f2 in LInt_p_meas_imag lemma.