add continuous_within_itvcyP/ycP

[IshiguroYoshihiro]

Motivation for this change

add unbound interval version of continuous_within_itvP,
which is used in my other work.

Checklist

• added corresponding entries in CHANGELOG_UNRELEASED.md

• added corresponding documentation in the headers

Reference: How to document

Reminder to reviewers

• Read this Checklist
• Put a milestone if possible
• Check labels

[affeldt-aist]

The last commits factorize out redundant code snippets. @zstone1 do you think we should make more efforts to simplify the proofs?

[zstone1]

With a software engineering perspective, it's annoying that the proofs for left-convergence and right-convergence are basically copy-pasted (modulo a few opprKs). But things are now pretty short, so I think this is acceptable