Itv

[proux01]

Motivation for this change

I wanted to merge intervals with signed but clearly don't have time to pursue that path currently. Since it seems already useful as it is, let's PR it now, we could always try to improve later.

The multiplication only works for realDomainType (and not for numDomainType), for relatively bad reasons.
The proof of the multiplication could probably be improved using wlog.

Things done/to do

• added corresponding entries in CHANGELOG_UNRELEASED.md
  (do not edit former entries, only append new ones, be careful:
  merge and rebase have a tendency to mess up CHANGELOG_UNRELEASED.md)
• added corresponding documentation in the headers

Automatic note to reviewers

Read this Checklist and put a milestone if possible.

[affeldt-aist]

Thanks for the PR.
I have tried to use it in PR #873 and it seems to work as intended (in the sense that it seems to replace the prob type that was used in PR #794). It is likely that we will be able to use it to port previous work on convexity.
About the contents of the PR, I have minor comments.
Class infer, lemma inferP, class unify, unify', instance unify'P already appear in signed.v which is Require Imported, so maybe they can be removed (maybe they were duplicated to make the file self-contained?).
The identifiers top_typ_subproof and top_typ appear in both signed.v and itv.v, maybe they can be distinguished? (Similar comment for lemmas bottom, gt0, le0F, lt0, ge0F, ge0, lt0F, le0, gt0F.)

[proux01]

Class infer, lemma inferP, class unify, unify', instance unify'P already appear in signed.v which is Require Imported, so maybe they can be removed (maybe they were duplicated to make the file self-contained?).

Yes, since the hint and instances are #[global], the Require Import is enough and they can be removed.

The identifiers top_typ_subproof and top_typ appear in both signed.v and itv.v, maybe they can be distinguished? (Similar comment for lemmas bottom, gt0, le0F, lt0, ge0F, ge0, lt0F, le0, gt0F.)

If we may import both (which seems likely), they indeed should be distinguished, maybe just prefix them with itv_?

[affeldt-aist]

We could maybe issue about these two comments when merging:

The multiplication only works for realDomainType (and not for numDomainType), for relatively bad reasons.
The proof of the multiplication could probably be improved using wlog.
And maybe also issue about the future removal of the trailing tests.