shorten proof about monotonic functions

[affeldt-aist]

https://github.com/math-comp/analysis/blob/8e4ae6df5ca7bd004df6c9ba07199a98633f2cc6/theories/realfun.v#L240

"the proofs might be shorter by doing a wlog that goes back to the previous statement. (The wlog should change f with a patch of f with a small enough value after the new bound, not to affect the local behaviour around a^+.)"

see the conversation of PR #1147