You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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^+.)"
analysis/theories/realfun.v
Line 240 in 8e4ae6d
"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
The text was updated successfully, but these errors were encountered: