(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!

*_seq'* -> *_seq_Rbar*

Remove old scories...

eb9897ee (FC, 2021/10/27 20:09:32), and then replay changes of
2021/10/26-27 by Houda and Sylvie.
(Comment proof of LInt_Rbar_dominated_convergence to make LInt.v compile.)

Incorporate contents of file_lebesgue.v into sum_Rbar_nonneg.v and
LInt_p.v. Rename file_tonelli.v into Tonelli.v.

Update _CoqProject.

This reverts commit ab8689c9, reversing
changes made to eb9897ee.

sigma_algebra_R_Rbar_new.v -> sigma_algebra_R_Rbar.v

Problème du type de LInt (E->R/Rbar) -> R/Rbar