Missing notations in `itv.v`?

[affeldt-aist]

https://github.com/math-comp/analysis/blob/5d4db09b412ac521d67830bd1ba507aed567056c/theories/itv.v#L35-L40

I can find [itv of ...] but not [lb of ...], etc.

[affeldt-aist]

By the way, I was looking for a way to infer a {nonneg R} from a {i01 R}.

[proux01]

I can find [itv of ...] but not [lb of ...], etc.

Indeed, they are apparently missing.

By the way, I was looking for a way to infer a {nonneg R} from a {i01 R}.

I guess the simplest solution would be to add a Canonical to be able to write x%:inum%:nng but the uncomfortable thing is: why would that instance take the lower bound rather than the upper bound? (other than the fact it is probably what one wants most fo the time)