Add new Mp for full Rbar functions (still admitted).

chain: simple_fun -> Mp -> Lint_p.

(Could be moved to simple_fun.v and measurable_fun.v.)

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