General reasoning principle for interval bounds
The following discussion from !363 (merged) should be addressed:
-
@bbb started a discussion: (+2 comments)
General comment: We keep re-proving statements like this in problem-specific contexts. This feels quite repetitive. In the end, the arguments always follows similar lines: if we're some bounds on predicates holding in an interval, if the interval is long enough, eventually the predicate must not hold at some point. I think there should be an underlying generic theorem about this reasoning principle, i.e., at the level of generic bounds on the number of instants that satisfy some predicate(s) in a given interval.