notation for intervals

[affeldt-aist]

We have been using intervals with extended real numbers but this has the consequence that `[0%E, +oo] = `[0%E, +oo[. How can we handle that? @hoheinzollern @t6s

[t6s]

Is it difficult to modify the notation on the LHS to `[_, +oo[ to be consistent?

[CohenCyril]

I suggest you overload notations in ereal scope and print `[x, +oo[%O for ereals differently.

[CohenCyril]

Or one could implement a latticeWithNoTop in the same way as
https://github.com/coq/coq/blob/master/theories/ssr/ssreflect.v#L30-L34