Among notable changes, we can ow use + and * notations in scope
ring_scope on semirings, including the semiring of functions Fd.

This also changes the UPP definition from [T, T+d) periods
to (T, T+d] periods, and all the changes that this implies.

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).

Update name in nc file and update old comment about previous S6 (now S5_2).

Replace UIB_departure with maximal_departure

It was using sequpp_min instead of sequpp_min' and was failing for
instance on :

sequpp_min
	{|
        sequpp_T := (12987 # 3125);
        sequpp_d := 1;
        sequpp_c := 20000;
        sequpp_js :=
          [:: (0, (0%:E, (0, 0%:E)));
              ((3612 # 3125), (0%:E, (20000, 8000%:E)))]
      |}%bigQ
      {|
        sequpp_T := 2;
        sequpp_d := 1;
        sequpp_c := 0;
        sequpp_js :=
          [:: (0, (0%:E, (0, 0%:E)));
              ((3612 / 3125), (0%:E, (0, +oo)))]
      |}%bigQ

Variables match with thesis. Min with delta 0 added to match with
minerve.

To avoid having usual_functions depend on deviations.