With Sophie Quinton during ECRTS 2022

The other direction doesn't hold since we only register completions
in network calculus derived curves.

An overapproximation is provided in one direction,
the converse direction works only for periodic clocks.

The new definition uses a left-closed interval, as in the book.
The (wrong) theorem in the book is fixed by assuming the service curve
beta is left continuous.

The definition was specialized to non empty intervals
open on the left and closed on the right (l, r].

* Compile with MathCOmp 1.13
* NC-Coq doesn't need CoqEAL since Minerve is now separated

The two definitions are proved equivalent, the older one was more
"computational" but this one is closer from the mathematical
definition.

The two definitions are proved equivalent, the older one was more
"computational" but this one is closer from the mathematical
definition.

Now including dual extended real addition.

It requires minerve to compile (which itself requires NCCoq,
creating some kind of deadlock).