@affeldt-aist, after thinking a bit more, we could reprove `nondecreasing_cvg`

thanks to:

```
Lemma nondecreasing_cvg (u_ : {ereal R}^nat) (M : R) : nondecreasing_seq u_ -> u_ --> esup (u_ @` setT).
```

on one hand and `lim_le`

on the other hand.

Last updated: Aug 19 2022 at 20:03 UTC