|
Lemma nonincreasing_at_right_cvgr f a (b : itv_bound R) : (BRight a < b)%O -> |
"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
