Change the definition of is_interval to rely on large inequalities

[ybertot]

The previous definition, based on strict inequalities, is less practical

The impact of this change has been tested against two other pull requests that use the is_interval concept

• A generic lemma to prove the continuity of inverse functions #385 : porting this PR leads to branch ctinv-itv
• Lebesgue measure and integral #371 : porting this PR leads to branch ctv-itv-meas (actually this branch contains both 385 and 371).

[CohenCyril]

Hi @ybertot, I do not understand what 793badc are 3aa4fe5 doing here. Did I miss something?

[ybertot]

I don't understand either. I did a rebase, and all of a sudden these commits were included in the branch. Maybe I goofed one of my rebase, and then I had to do force push, but people usually have to do a force push after a rebase, so that you are really working without a safety net at this point.

Maybe the solution will be to remake the branch from scratch and cherry-pick the commits. I am not too fluent, but I may be able to repair that.

[CohenCyril]

I did a rebase, and all of a sudden these commits were included in the branch.

Well, it looks like you rebased master on top of is_itv and then added a commit...

[ybertot]

should be fixed now.

[CohenCyril]

OK, I'm 100% of the benefits of this change.
@affeldt-aist do you agree?

[affeldt-aist]

OK, I'm 100% of the benefits of this change.
@affeldt-aist do you agree?

Yes, no problem.

[CohenCyril]

nitpicking

[CohenCyril]

LGTM