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.

Avoids having to local open scope after importing NCCoq.computation.tactic.

CoqEAL 1.0.6 has a bug making typeclass search expensive.

Use abstract + vm_cast_no_check to avoid redoing the full check a
second time during Qed.

For instance, on the example below, f was extended to period 40000 by
duplicating its period 40000 times, now it is done by just keeping its
jump sequence unchanged since the function is affine after its initial
segment.

Require Import mathcomp.ssreflect.ssrbool mathcomp.ssreflect.order.
Require Import NCCoq.computation.tactic.
Local Open Scope ereal_scope.
Local Open Scope order_scope.
Local Open Scope F_scope.
Let f := F_of_sequpp {|
  (* Conversion of upp([(0,0)0(1,0)[, period([(1,0)0(2,0)[), 0, 1) *)
  sequpp_T := 1;
  sequpp_d := 1;
  sequpp_c := 0;
  sequpp_js := [::
  (0, ( (0)%:E, (0, (0)%:E)));
  (1, ( (0)%:E, (0, (0)%:E)))]
|}%bigQ.
Let g := F_of_sequpp {|
  (* Conversion of upp([(0,0)0(0,0)], period(](0,2560)0(40000,2560)]), 2560, 40000) *)
  sequpp_T := 20000;
  sequpp_d := 40000;
  sequpp_c := 2560;
  sequpp_js := [::
  (0, ( (0)%:E, (0, (2560)%:E)));
  (20000, ( (2560)%:E, (0, (2560)%:E)));
  (40000, ( (2560)%:E, (0, (5120)%:E)))]
|}%bigQ.
Let h := F_of_sequpp {|
  (* Conversion of upp([(0,0)0(0,0)], period(](0,2560)0(40000,2560)]), 2560, 40000) *)
  sequpp_T := 20000;
  sequpp_d := 40000;
  sequpp_c := 2560;
  sequpp_js := [::
  (0, ( (0)%:E, (0, (2560)%:E)));
  (20000, ( (2560)%:E, (0, (2560)%:E)));
  (40000, ( (2560)%:E, (0, (5120)%:E)))]
|}%bigQ.
Goal h = f + g.
Proof. nccoq. Qed.