Require Export prosa.behavior.time.
Require Export prosa.util.all.
[Loading ML file ssrmatching_plugin.cmxs (using legacy method) ... done]
[Loading ML file ssreflect_plugin.cmxs (using legacy method) ... done]
[Loading ML file ring_plugin.cmxs (using legacy method) ... done]
Serlib plugin: coq-elpi.elpi is not available: serlib support is missing.
Incremental checking for commands in this plugin will be impacted.
[Loading ML file coq-elpi.elpi ... done]
[Loading ML file zify_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_core_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_plugin.cmxs (using legacy method) ... done]
[Loading ML file btauto_plugin.cmxs (using legacy method) ... done]
Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Require Export prosa.implementation.definitions.extrapolated_arrival_curve.

(** In this file, we prove basic properties of the arrival-curve
    prefix and the [extrapolated_arrival_curve] function. *)

(** We start with basic facts about the relations [ltn_steps] and [leq_steps]. *)
Section BasicFacts.

  (** We show that the relation [ltn_steps] is transitive. *)
  Lemma ltn_steps_is_transitive :
    transitive ltn_steps.
transitive (T:=nat * nat) ltn_steps
  Proof.
transitive (T:=nat * nat) ltn_steps
    move=> a b c /andP [FSTab SNDab] /andP [FSTbc SNDbc].
a, b, c: (nat * nat)%type
FSTab: b.1 < a.1
SNDab: b.2 < a.2
FSTbc: a.1 < c.1
SNDbc: a.2 < c.2
ltn_steps b c
    by apply /andP; split; lia.
  Qed.

  (** Next, we show that the relation [leq_steps] is reflexive... *)
  Lemma leq_steps_is_reflexive :
    reflexive leq_steps.
reflexive (T:=nat * nat) leq_steps
  Proof.
reflexive (T:=nat * nat) leq_steps
    move=> [l r].
l, r: nat
leq_steps (l, r) (l, r)
    rewrite /leq_steps.
l, r: nat
((l, r).1 <= (l, r).1) && ((l, r).2 <= (l, r).2)
    by apply /andP; split.
  Qed.

  (** ... and transitive. *)
  Lemma leq_steps_is_transitive :
    transitive leq_steps.
transitive (T:=nat * nat) leq_steps
  Proof.
transitive (T:=nat * nat) leq_steps
    move=> a b c /andP [FSTab SNDab] /andP [FSTbc SNDbc].
a, b, c: (nat * nat)%type
FSTab: b.1 <= a.1
SNDab: b.2 <= a.2
FSTbc: a.1 <= c.1
SNDbc: a.2 <= c.2
leq_steps b c
    by apply /andP; split; lia.
  Qed.

End BasicFacts.

(** In the following section, we prove a few properties of
    arrival-curve prefixes assuming that there are no infinite
    arrivals and that the list of steps is sorted according to the
    [leq_steps] relation. *)
Section ArrivalCurvePrefixSortedLeq.

  (** Consider an arbitrary [leq]-sorted arrival-curve prefix without
      infinite arrivals. *)
  Variable ac_prefix : ArrivalCurvePrefix.
  Hypothesis H_sorted_leq : sorted_leq_steps ac_prefix.
  Hypothesis H_no_inf_arrivals : no_inf_arrivals ac_prefix.

  (** We prove that [value_at] is monotone with respect to the relation [<=]. *)
  Lemma value_at_monotone :
    monotone leq (value_at ac_prefix).
ac_prefix: ArrivalCurvePrefix
H_sorted_leq: sorted_leq_steps ac_prefix
H_no_inf_arrivals: no_inf_arrivals ac_prefix
monotone leq (value_at ac_prefix)
  Proof.
ac_prefix: ArrivalCurvePrefix
H_sorted_leq: sorted_leq_steps ac_prefix
H_no_inf_arrivals: no_inf_arrivals ac_prefix
monotone leq (value_at ac_prefix)
    intros t1 t2 LE; clear H_no_inf_arrivals.
ac_prefix: ArrivalCurvePrefix
H_sorted_leq: sorted_leq_steps ac_prefix
t1, t2: nat
LE: t1 <= t2
value_at ac_prefix t1 <= value_at ac_prefix t2
    unfold sorted_leq_steps, value_at, step_at, steps_of in *.
ac_prefix: ArrivalCurvePrefix
H_sorted_leq: sorted leq_steps ac_prefix.2
t1, t2: nat
LE: t1 <= t2
(last (0, 0) [seq step <- ac_prefix.2 | step.1 <= t1]).2 <=
(last (0, 0) [seq step <- ac_prefix.2 | step.1 <= t2]).2
    destruct ac_prefix as [h steps]; simpl.
ac_prefix: ArrivalCurvePrefix
h: duration
steps: seq (duration * nat)
H_sorted_leq: sorted leq_steps (h, steps).2
t1, t2: nat
LE: t1 <= t2
(last (0, 0) [seq step <- steps | step.1 <= t1]).2 <=
(last (0, 0) [seq step <- steps | step.1 <= t2]).2
    have GenLem:
      forall t__d1 v__d1 t__d2 v__d2,
        v__d1 <= v__d2 ->
        all (leq_steps (t__d1, v__d1)) steps ->
        all (leq_steps (t__d2, v__d2)) steps ->
        snd (last (t__d1, v__d1) [seq step <- steps | fst step <= t1]) <= snd (last (t__d2, v__d2) [seq step <- steps | fst step <= t2]).
ac_prefix: ArrivalCurvePrefix
h: duration
steps: seq (duration * nat)
H_sorted_leq: sorted leq_steps (h, steps).2
t1, t2: nat
LE: t1 <= t2
forall t__d1 v__d1 t__d2 v__d2 : nat,
v__d1 <= v__d2 ->
all (leq_steps (t__d1, v__d1)) steps ->
all (leq_steps (t__d2, v__d2)) steps ->
(last (t__d1, v__d1)
   [seq step <- steps | step.1 <= t1]).2 <=
(last (t__d2, v__d2)
   [seq step <- steps | step.1 <= t2]).2
ac_prefix: ArrivalCurvePrefix
h: duration
steps: seq (duration * nat)
H_sorted_leq: sorted leq_steps (h, steps).2
t1, t2: nat
LE: t1 <= t2
GenLem: forall t__d1 v__d1 t__d2 v__d2 : nat,
v__d1 <= v__d2 ->
all (leq_steps (t__d1, v__d1)) steps ->
all (leq_steps (t__d2, v__d2)) steps ->
(last (t__d1, v__d1)
   [seq step <- steps | step.1 <= t1]).2 <=
(last (t__d2, v__d2)
   [seq step <- steps | step.1 <= t2]).2
(last (0, 0) [seq step <- steps | step.1 <= t1]).2 <=
(last (0, 0) [seq step <- steps | step.1 <= t2]).2
    {
ac_prefix: ArrivalCurvePrefix
h: duration
steps: seq (duration * nat)
H_sorted_leq: sorted leq_steps (h, steps).2
t1, t2: nat
LE: t1 <= t2
forall t__d1 v__d1 t__d2 v__d2 : nat,
v__d1 <= v__d2 ->
all (leq_steps (t__d1, v__d1)) steps ->
all (leq_steps (t__d2, v__d2)) steps ->
(last (t__d1, v__d1)
   [seq step <- steps | step.1 <= t1]).2 <=
(last (t__d2, v__d2)
   [seq step <- steps | step.1 <= t2]).2 have steps_sorted := H_sorted_leq; clear H_sorted_leq.
ac_prefix: ArrivalCurvePrefix
h: duration
steps: seq (duration * nat)
t1, t2: nat
LE: t1 <= t2
steps_sorted: sorted leq_steps (h, steps).2
forall t__d1 v__d1 t__d2 v__d2 : nat,
v__d1 <= v__d2 ->
all (leq_steps (t__d1, v__d1)) steps ->
all (leq_steps (t__d2, v__d2)) steps ->
(last (t__d1, v__d1)
   [seq step <- steps | step.1 <= t1]).2 <=
(last (t__d2, v__d2)
   [seq step <- steps | step.1 <= t2]).2
      elim: steps steps_sorted => [//|[t__c v__c] steps IHsteps] steps_sorted.
ac_prefix: ArrivalCurvePrefix
h: duration
t1, t2: nat
LE: t1 <= t2
t__c: duration
v__c: nat
steps: seq (duration * nat)
IHsteps: sorted leq_steps (h, steps).2 ->
forall t__d1 v__d1 t__d2 v__d2 : nat,
v__d1 <= v__d2 ->
all (leq_steps (t__d1, v__d1)) steps ->
all (leq_steps (t__d2, v__d2)) steps ->
(last (t__d1, v__d1)
   [seq step <- steps | step.1 <= t1]).2 <=
(last (t__d2, v__d2)
   [seq step <- steps | step.1 <= t2]).2
steps_sorted: sorted leq_steps
  (h, (t__c, v__c) :: steps).2
forall t__d1 v__d1 t__d2 v__d2 : nat,
v__d1 <= v__d2 ->
all (leq_steps (t__d1, v__d1)) ((t__c, v__c) :: steps) ->
all (leq_steps (t__d2, v__d2)) ((t__c, v__c) :: steps) ->
(last (t__d1, v__d1)
   [seq step <- (t__c, v__c) :: steps | step.1 <= t1]).2 <=
(last (t__d2, v__d2)
   [seq step <- (t__c, v__c) :: steps | step.1 <= t2]).2
      simpl; intros *; move => LEv /andP [LTN1 /allP ALL1] /andP [LTN2 /allP ALL2].
ac_prefix: ArrivalCurvePrefix
h: duration
t1, t2: nat
LE: t1 <= t2
t__c: duration
v__c: nat
steps: seq (duration * nat)
IHsteps: sorted leq_steps (h, steps).2 ->
forall t__d1 v__d1 t__d2 v__d2 : nat,
v__d1 <= v__d2 ->
all (leq_steps (t__d1, v__d1)) steps ->
all (leq_steps (t__d2, v__d2)) steps ->
(last (t__d1, v__d1)
   [seq step <- steps | step.1 <= t1]).2 <=
(last (t__d2, v__d2)
   [seq step <- steps | step.1 <= t2]).2
steps_sorted: sorted leq_steps
  (h, (t__c, v__c) :: steps).2
t__d1, v__d1, t__d2, v__d2: nat
LEv: v__d1 <= v__d2
LTN1: leq_steps (t__d1, v__d1) (t__c, v__c)
ALL1: {in steps,
  forall
    x : Datatypes_prod__canonical__eqtype_Equality
          Datatypes_nat__canonical__eqtype_Equality
          Datatypes_nat__canonical__eqtype_Equality,
  leq_steps (t__d1, v__d1) x}
LTN2: leq_steps (t__d2, v__d2) (t__c, v__c)
ALL2: {in steps,
  forall
    x : Datatypes_prod__canonical__eqtype_Equality
          Datatypes_nat__canonical__eqtype_Equality
          Datatypes_nat__canonical__eqtype_Equality,
  leq_steps (t__d2, v__d2) x}
(last (t__d1, v__d1)
   (if t__c <= t1
    then
     (t__c, v__c)
     :: [seq step <- steps | step.1 <= t1]
    else [seq step <- steps | step.1 <= t1])).2 <=
(last (t__d2, v__d2)
   (if t__c <= t2
    then
     (t__c, v__c)
     :: [seq step <- steps | step.1 <= t2]
    else [seq step <- steps | step.1 <= t2])).2
      move: (steps_sorted); rewrite //= (@path_sorted_inE _ predT leq_steps); first last.
ac_prefix: ArrivalCurvePrefix
h: duration
t1, t2: nat
LE: t1 <= t2
t__c: duration
v__c: nat
steps: seq (duration * nat)
IHsteps: sorted leq_steps (h, steps).2 ->
forall t__d1 v__d1 t__d2 v__d2 : nat,
v__d1 <= v__d2 ->
all (leq_steps (t__d1, v__d1)) steps ->
all (leq_steps (t__d2, v__d2)) steps ->
(last (t__d1, v__d1)
   [seq step <- steps | step.1 <= t1]).2 <=
(last (t__d2, v__d2)
   [seq step <- steps | step.1 <= t2]).2
steps_sorted: sorted leq_steps
  (h, (t__c, v__c) :: steps).2
t__d1, v__d1, t__d2, v__d2: nat
LEv: v__d1 <= v__d2
LTN1: leq_steps (t__d1, v__d1) (t__c, v__c)
ALL1: {in steps,
  forall
    x : Datatypes_prod__canonical__eqtype_Equality
          Datatypes_nat__canonical__eqtype_Equality
          Datatypes_nat__canonical__eqtype_Equality,
  leq_steps (t__d1, v__d1) x}
LTN2: leq_steps (t__d2, v__d2) (t__c, v__c)
ALL2: {in steps,
  forall
    x : Datatypes_prod__canonical__eqtype_Equality
          Datatypes_nat__canonical__eqtype_Equality
          Datatypes_nat__canonical__eqtype_Equality,
  leq_steps (t__d2, v__d2) x}
all predT ((t__c, v__c) :: steps)
ac_prefix: ArrivalCurvePrefix
h: duration
t1, t2: nat
LE: t1 <= t2
t__c: duration
v__c: nat
steps: seq (duration * nat)
IHsteps: sorted leq_steps (h, steps).2 ->
forall t__d1 v__d1 t__d2 v__d2 : nat,
v__d1 <= v__d2 ->
all (leq_steps (t__d1, v__d1)) steps ->
all (leq_steps (t__d2, v__d2)) steps ->
(last (t__d1, v__d1)
   [seq step <- steps | step.1 <= t1]).2 <=
(last (t__d2, v__d2)
   [seq step <- steps | step.1 <= t2]).2
steps_sorted: sorted leq_steps
  (h, (t__c, v__c) :: steps).2
t__d1, v__d1, t__d2, v__d2: nat
LEv: v__d1 <= v__d2
LTN1: leq_steps (t__d1, v__d1) (t__c, v__c)
ALL1: {in steps,
  forall
    x : Datatypes_prod__canonical__eqtype_Equality
          Datatypes_nat__canonical__eqtype_Equality
          Datatypes_nat__canonical__eqtype_Equality,
  leq_steps (t__d1, v__d1) x}
LTN2: leq_steps (t__d2, v__d2) (t__c, v__c)
ALL2: {in steps,
  forall
    x : Datatypes_prod__canonical__eqtype_Equality
          Datatypes_nat__canonical__eqtype_Equality
          Datatypes_nat__canonical__eqtype_Equality,
  leq_steps (t__d2, v__d2) x}
{in predT & &, transitive (T:=nat * nat) leq_steps}
ac_prefix: ArrivalCurvePrefix
h: duration
t1, t2: nat
LE: t1 <= t2
t__c: duration
v__c: nat
steps: seq (duration * nat)
IHsteps: sorted leq_steps (h, steps).2 ->
forall t__d1 v__d1 t__d2 v__d2 : nat,
v__d1 <= v__d2 ->
all (leq_steps (t__d1, v__d1)) steps ->
all (leq_steps (t__d2, v__d2)) steps ->
(last (t__d1, v__d1)
   [seq step <- steps | step.1 <= t1]).2 <=
(last (t__d2, v__d2)
   [seq step <- steps | step.1 <= t2]).2
steps_sorted: sorted leq_steps
  (h, (t__c, v__c) :: steps).2
t__d1, v__d1, t__d2, v__d2: nat
LEv: v__d1 <= v__d2
LTN1: leq_steps (t__d1, v__d1) (t__c, v__c)
ALL1: {in steps,
  forall
    x : Datatypes_prod__canonical__eqtype_Equality
          Datatypes_nat__canonical__eqtype_Equality
          Datatypes_nat__canonical__eqtype_Equality,
  leq_steps (t__d1, v__d1) x}
LTN2: leq_steps (t__d2, v__d2) (t__c, v__c)
ALL2: {in steps,
  forall
    x : Datatypes_prod__canonical__eqtype_Equality
          Datatypes_nat__canonical__eqtype_Equality
          Datatypes_nat__canonical__eqtype_Equality,
  leq_steps (t__d2, v__d2) x}
all (leq_steps (t__c, v__c)) steps &&
sorted leq_steps steps ->
(last (t__d1, v__d1)
   (if t__c <= t1
    then
     (t__c, v__c)
     :: [seq step <- steps | step.1 <= t1]
    else [seq step <- steps | step.1 <= t1])).2 <=
(last (t__d2, v__d2)
   (if t__c <= t2
    then
     (t__c, v__c)
     :: [seq step <- steps | step.1 <= t2]
    else [seq step <- steps | step.1 <= t2])).2
      {
ac_prefix: ArrivalCurvePrefix
h: duration
t1, t2: nat
LE: t1 <= t2
t__c: duration
v__c: nat
steps: seq (duration * nat)
IHsteps: sorted leq_steps (h, steps).2 ->
forall t__d1 v__d1 t__d2 v__d2 : nat,
v__d1 <= v__d2 ->
all (leq_steps (t__d1, v__d1)) steps ->
all (leq_steps (t__d2, v__d2)) steps ->
(last (t__d1, v__d1)
   [seq step <- steps | step.1 <= t1]).2 <=
(last (t__d2, v__d2)
   [seq step <- steps | step.1 <= t2]).2
steps_sorted: sorted leq_steps
  (h, (t__c, v__c) :: steps).2
t__d1, v__d1, t__d2, v__d2: nat
LEv: v__d1 <= v__d2
LTN1: leq_steps (t__d1, v__d1) (t__c, v__c)
ALL1: {in steps,
  forall
    x : Datatypes_prod__canonical__eqtype_Equality
          Datatypes_nat__canonical__eqtype_Equality
          Datatypes_nat__canonical__eqtype_Equality,
  leq_steps (t__d1, v__d1) x}
LTN2: leq_steps (t__d2, v__d2) (t__c, v__c)
ALL2: {in steps,
  forall
    x : Datatypes_prod__canonical__eqtype_Equality
          Datatypes_nat__canonical__eqtype_Equality
          Datatypes_nat__canonical__eqtype_Equality,
  leq_steps (t__d2, v__d2) x}
all predT ((t__c, v__c) :: steps) by apply/allP. }
ac_prefix: ArrivalCurvePrefix
h: duration
t1, t2: nat
LE: t1 <= t2
t__c: duration
v__c: nat
steps: seq (duration * nat)
IHsteps: sorted leq_steps (h, steps).2 ->
forall t__d1 v__d1 t__d2 v__d2 : nat,
v__d1 <= v__d2 ->
all (leq_steps (t__d1, v__d1)) steps ->
all (leq_steps (t__d2, v__d2)) steps ->
(last (t__d1, v__d1)
   [seq step <- steps | step.1 <= t1]).2 <=
(last (t__d2, v__d2)
   [seq step <- steps | step.1 <= t2]).2
steps_sorted: sorted leq_steps
  (h, (t__c, v__c) :: steps).2
t__d1, v__d1, t__d2, v__d2: nat
LEv: v__d1 <= v__d2
LTN1: leq_steps (t__d1, v__d1) (t__c, v__c)
ALL1: {in steps,
  forall
    x : Datatypes_prod__canonical__eqtype_Equality
          Datatypes_nat__canonical__eqtype_Equality
          Datatypes_nat__canonical__eqtype_Equality,
  leq_steps (t__d1, v__d1) x}
LTN2: leq_steps (t__d2, v__d2) (t__c, v__c)
ALL2: {in steps,
  forall
    x : Datatypes_prod__canonical__eqtype_Equality
          Datatypes_nat__canonical__eqtype_Equality
          Datatypes_nat__canonical__eqtype_Equality,
  leq_steps (t__d2, v__d2) x}
{in predT & &, transitive (T:=nat * nat) leq_steps}
ac_prefix: ArrivalCurvePrefix
h: duration
t1, t2: nat
LE: t1 <= t2
t__c: duration
v__c: nat
steps: seq (duration * nat)
IHsteps: sorted leq_steps (h, steps).2 ->
forall t__d1 v__d1 t__d2 v__d2 : nat,
v__d1 <= v__d2 ->
all (leq_steps (t__d1, v__d1)) steps ->
all (leq_steps (t__d2, v__d2)) steps ->
(last (t__d1, v__d1)
   [seq step <- steps | step.1 <= t1]).2 <=
(last (t__d2, v__d2)
   [seq step <- steps | step.1 <= t2]).2
steps_sorted: sorted leq_steps
  (h, (t__c, v__c) :: steps).2
t__d1, v__d1, t__d2, v__d2: nat
LEv: v__d1 <= v__d2
LTN1: leq_steps (t__d1, v__d1) (t__c, v__c)
ALL1: {in steps,
  forall
    x : Datatypes_prod__canonical__eqtype_Equality
          Datatypes_nat__canonical__eqtype_Equality
          Datatypes_nat__canonical__eqtype_Equality,
  leq_steps (t__d1, v__d1) x}
LTN2: leq_steps (t__d2, v__d2) (t__c, v__c)
ALL2: {in steps,
  forall
    x : Datatypes_prod__canonical__eqtype_Equality
          Datatypes_nat__canonical__eqtype_Equality
          Datatypes_nat__canonical__eqtype_Equality,
  leq_steps (t__d2, v__d2) x}
all (leq_steps (t__c, v__c)) steps &&
sorted leq_steps steps ->
(last (t__d1, v__d1)
   (if t__c <= t1
    then
     (t__c, v__c)
     :: [seq step <- steps | step.1 <= t1]
    else [seq step <- steps | step.1 <= t1])).2 <=
(last (t__d2, v__d2)
   (if t__c <= t2
    then
     (t__c, v__c)
     :: [seq step <- steps | step.1 <= t2]
    else [seq step <- steps | step.1 <= t2])).2
      {
ac_prefix: ArrivalCurvePrefix
h: duration
t1, t2: nat
LE: t1 <= t2
t__c: duration
v__c: nat
steps: seq (duration * nat)
IHsteps: sorted leq_steps (h, steps).2 ->
forall t__d1 v__d1 t__d2 v__d2 : nat,
v__d1 <= v__d2 ->
all (leq_steps (t__d1, v__d1)) steps ->
all (leq_steps (t__d2, v__d2)) steps ->
(last (t__d1, v__d1)
   [seq step <- steps | step.1 <= t1]).2 <=
(last (t__d2, v__d2)
   [seq step <- steps | step.1 <= t2]).2
steps_sorted: sorted leq_steps
  (h, (t__c, v__c) :: steps).2
t__d1, v__d1, t__d2, v__d2: nat
LEv: v__d1 <= v__d2
LTN1: leq_steps (t__d1, v__d1) (t__c, v__c)
ALL1: {in steps,
  forall
    x : Datatypes_prod__canonical__eqtype_Equality
          Datatypes_nat__canonical__eqtype_Equality
          Datatypes_nat__canonical__eqtype_Equality,
  leq_steps (t__d1, v__d1) x}
LTN2: leq_steps (t__d2, v__d2) (t__c, v__c)
ALL2: {in steps,
  forall
    x : Datatypes_prod__canonical__eqtype_Equality
          Datatypes_nat__canonical__eqtype_Equality
          Datatypes_nat__canonical__eqtype_Equality,
  leq_steps (t__d2, v__d2) x}
{in predT & &, transitive (T:=nat * nat) leq_steps} by intros ? ? ? _ _ _; apply leq_steps_is_transitive. }
ac_prefix: ArrivalCurvePrefix
h: duration
t1, t2: nat
LE: t1 <= t2
t__c: duration
v__c: nat
steps: seq (duration * nat)
IHsteps: sorted leq_steps (h, steps).2 ->
forall t__d1 v__d1 t__d2 v__d2 : nat,
v__d1 <= v__d2 ->
all (leq_steps (t__d1, v__d1)) steps ->
all (leq_steps (t__d2, v__d2)) steps ->
(last (t__d1, v__d1)
   [seq step <- steps | step.1 <= t1]).2 <=
(last (t__d2, v__d2)
   [seq step <- steps | step.1 <= t2]).2
steps_sorted: sorted leq_steps
  (h, (t__c, v__c) :: steps).2
t__d1, v__d1, t__d2, v__d2: nat
LEv: v__d1 <= v__d2
LTN1: leq_steps (t__d1, v__d1) (t__c, v__c)
ALL1: {in steps,
  forall
    x : Datatypes_prod__canonical__eqtype_Equality
          Datatypes_nat__canonical__eqtype_Equality
          Datatypes_nat__canonical__eqtype_Equality,
  leq_steps (t__d1, v__d1) x}
LTN2: leq_steps (t__d2, v__d2) (t__c, v__c)
ALL2: {in steps,
  forall
    x : Datatypes_prod__canonical__eqtype_Equality
          Datatypes_nat__canonical__eqtype_Equality
          Datatypes_nat__canonical__eqtype_Equality,
  leq_steps (t__d2, v__d2) x}
all (leq_steps (t__c, v__c)) steps &&
sorted leq_steps steps ->
(last (t__d1, v__d1)
   (if t__c <= t1
    then
     (t__c, v__c)
     :: [seq step <- steps | step.1 <= t1]
    else [seq step <- steps | step.1 <= t1])).2 <=
(last (t__d2, v__d2)
   (if t__c <= t2
    then
     (t__c, v__c)
     :: [seq step <- steps | step.1 <= t2]
    else [seq step <- steps | step.1 <= t2])).2
      move => /andP [ALL SORT].
ac_prefix: ArrivalCurvePrefix
h: duration
t1, t2: nat
LE: t1 <= t2
t__c: duration
v__c: nat
steps: seq (duration * nat)
IHsteps: sorted leq_steps (h, steps).2 ->
forall t__d1 v__d1 t__d2 v__d2 : nat,
v__d1 <= v__d2 ->
all (leq_steps (t__d1, v__d1)) steps ->
all (leq_steps (t__d2, v__d2)) steps ->
(last (t__d1, v__d1)
   [seq step <- steps | step.1 <= t1]).2 <=
(last (t__d2, v__d2)
   [seq step <- steps | step.1 <= t2]).2
steps_sorted: sorted leq_steps
  (h, (t__c, v__c) :: steps).2
t__d1, v__d1, t__d2, v__d2: nat
LEv: v__d1 <= v__d2
LTN1: leq_steps (t__d1, v__d1) (t__c, v__c)
ALL1: {in steps,
  forall
    x : Datatypes_prod__canonical__eqtype_Equality
          Datatypes_nat__canonical__eqtype_Equality
          Datatypes_nat__canonical__eqtype_Equality,
  leq_steps (t__d1, v__d1) x}
LTN2: leq_steps (t__d2, v__d2) (t__c, v__c)
ALL2: {in steps,
  forall
    x : Datatypes_prod__canonical__eqtype_Equality
          Datatypes_nat__canonical__eqtype_Equality
          Datatypes_nat__canonical__eqtype_Equality,
  leq_steps (t__d2, v__d2) x}
ALL: all (leq_steps (t__c, v__c)) steps
SORT: sorted leq_steps steps
(last (t__d1, v__d1)
   (if t__c <= t1
    then
     (t__c, v__c)
     :: [seq step <- steps | step.1 <= t1]
    else [seq step <- steps | step.1 <= t1])).2 <=
(last (t__d2, v__d2)
   (if t__c <= t2
    then
     (t__c, v__c)
     :: [seq step <- steps | step.1 <= t2]
    else [seq step <- steps | step.1 <= t2])).2
      destruct (leqP (fst (t__c, v__c)) t1) as [R1 | R1], (leqP (fst (t__c, v__c)) t2) as [R2 | R2]; simpl in *.
ac_prefix: ArrivalCurvePrefix
h: duration
t1, t2: nat
LE: t1 <= t2
t__c: duration
v__c: nat
steps: seq (duration * nat)
IHsteps: sorted leq_steps steps ->
forall t__d1 v__d1 t__d2 v__d2 : nat,
v__d1 <= v__d2 ->
all (leq_steps (t__d1, v__d1)) steps ->
all (leq_steps (t__d2, v__d2)) steps ->
(last (t__d1, v__d1)
   [seq step <- steps | step.1 <= t1]).2 <=
(last (t__d2, v__d2)
   [seq step <- steps | step.1 <= t2]).2
steps_sorted: path leq_steps (t__c, v__c) steps
t__d1, v__d1, t__d2, v__d2: nat
LEv: v__d1 <= v__d2
LTN1: leq_steps (t__d1, v__d1) (t__c, v__c)
ALL1: {in steps,
  forall x : nat * nat,
  leq_steps (t__d1, v__d1) x}
LTN2: leq_steps (t__d2, v__d2) (t__c, v__c)
ALL2: {in steps,
  forall x : nat * nat,
  leq_steps (t__d2, v__d2) x}
ALL: all (leq_steps (t__c, v__c)) steps
SORT: sorted leq_steps steps
R1: t__c <= t1
R2: t__c <= t2
(last (t__d1, v__d1)
   (if t__c <= t1
    then
     (t__c, v__c)
     :: [seq step <- steps | step.1 <= t1]
    else [seq step <- steps | step.1 <= t1])).2 <=
(last (t__d2, v__d2)
   (if t__c <= t2
    then
     (t__c, v__c)
     :: [seq step <- steps | step.1 <= t2]
    else [seq step <- steps | step.1 <= t2])).2
ac_prefix: ArrivalCurvePrefix
h: duration
t1, t2: nat
LE: t1 <= t2
t__c: duration
v__c: nat
steps: seq (duration * nat)
IHsteps: sorted leq_steps steps ->
forall t__d1 v__d1 t__d2 v__d2 : nat,
v__d1 <= v__d2 ->
all (leq_steps (t__d1, v__d1)) steps ->
all (leq_steps (t__d2, v__d2)) steps ->
(last (t__d1, v__d1)
   [seq step <- steps | step.1 <= t1]).2 <=
(last (t__d2, v__d2)
   [seq step <- steps | step.1 <= t2]).2
steps_sorted: path leq_steps (t__c, v__c) steps
t__d1, v__d1, t__d2, v__d2: nat
LEv: v__d1 <= v__d2
LTN1: leq_steps (t__d1, v__d1) (t__c, v__c)
ALL1: {in steps,
  forall x : nat * nat,
  leq_steps (t__d1, v__d1) x}
LTN2: leq_steps (t__d2, v__d2) (t__c, v__c)
ALL2: {in steps,
  forall x : nat * nat,
  leq_steps (t__d2, v__d2) x}
ALL: all (leq_steps (t__c, v__c)) steps
SORT: sorted leq_steps steps
R1: t__c <= t1
R2: t2 < t__c
(last (t__d1, v__d1)
   (if t__c <= t1
    then
     (t__c, v__c)
     :: [seq step <- steps | step.1 <= t1]
    else [seq step <- steps | step.1 <= t1])).2 <=
(last (t__d2, v__d2)
   (if t__c <= t2
    then
     (t__c, v__c)
     :: [seq step <- steps | step.1 <= t2]
    else [seq step <- steps | step.1 <= t2])).2
ac_prefix: ArrivalCurvePrefix
h: duration
t1, t2: nat
LE: t1 <= t2
t__c: duration
v__c: nat
steps: seq (duration * nat)
IHsteps: sorted leq_steps steps ->
forall t__d1 v__d1 t__d2 v__d2 : nat,
v__d1 <= v__d2 ->
all (leq_steps (t__d1, v__d1)) steps ->
all (leq_steps (t__d2, v__d2)) steps ->
(last (t__d1, v__d1)
   [seq step <- steps | step.1 <= t1]).2 <=
(last (t__d2, v__d2)
   [seq step <- steps | step.1 <= t2]).2
steps_sorted: path leq_steps (t__c, v__c) steps
t__d1, v__d1, t__d2, v__d2: nat
LEv: v__d1 <= v__d2
LTN1: leq_steps (t__d1, v__d1) (t__c, v__c)
ALL1: {in steps,
  forall x : nat * nat,
  leq_steps (t__d1, v__d1) x}
LTN2: leq_steps (t__d2, v__d2) (t__c, v__c)
ALL2: {in steps,
  forall x : nat * nat,
  leq_steps (t__d2, v__d2) x}
ALL: all (leq_steps (t__c, v__c)) steps
SORT: sorted leq_steps steps
R1: t1 < t__c
R2: t__c <= t2
(last (t__d1, v__d1)
   (if t__c <= t1
    then
     (t__c, v__c)
     :: [seq step <- steps | step.1 <= t1]
    else [seq step <- steps | step.1 <= t1])).2 <=
(last (t__d2, v__d2)
   (if t__c <= t2
    then
     (t__c, v__c)
     :: [seq step <- steps | step.1 <= t2]
    else [seq step <- steps | step.1 <= t2])).2
ac_prefix: ArrivalCurvePrefix
h: duration
t1, t2: nat
LE: t1 <= t2
t__c: duration
v__c: nat
steps: seq (duration * nat)
IHsteps: sorted leq_steps steps ->
forall t__d1 v__d1 t__d2 v__d2 : nat,
v__d1 <= v__d2 ->
all (leq_steps (t__d1, v__d1)) steps ->
all (leq_steps (t__d2, v__d2)) steps ->
(last (t__d1, v__d1)
   [seq step <- steps | step.1 <= t1]).2 <=
(last (t__d2, v__d2)
   [seq step <- steps | step.1 <= t2]).2
steps_sorted: path leq_steps (t__c, v__c) steps
t__d1, v__d1, t__d2, v__d2: nat
LEv: v__d1 <= v__d2
LTN1: leq_steps (t__d1, v__d1) (t__c, v__c)
ALL1: {in steps,
  forall x : nat * nat,
  leq_steps (t__d1, v__d1) x}
LTN2: leq_steps (t__d2, v__d2) (t__c, v__c)
ALL2: {in steps,
  forall x : nat * nat,
  leq_steps (t__d2, v__d2) x}
ALL: all (leq_steps (t__c, v__c)) steps
SORT: sorted leq_steps steps
R1: t1 < t__c
R2: t2 < t__c
(last (t__d1, v__d1)
   (if t__c <= t1
    then
     (t__c, v__c)
     :: [seq step <- steps | step.1 <= t1]
    else [seq step <- steps | step.1 <= t1])).2 <=
(last (t__d2, v__d2)
   (if t__c <= t2
    then
     (t__c, v__c)
     :: [seq step <- steps | step.1 <= t2]
    else [seq step <- steps | step.1 <= t2])).2
      {
ac_prefix: ArrivalCurvePrefix
h: duration
t1, t2: nat
LE: t1 <= t2
t__c: duration
v__c: nat
steps: seq (duration * nat)
IHsteps: sorted leq_steps steps ->
forall t__d1 v__d1 t__d2 v__d2 : nat,
v__d1 <= v__d2 ->
all (leq_steps (t__d1, v__d1)) steps ->
all (leq_steps (t__d2, v__d2)) steps ->
(last (t__d1, v__d1)
   [seq step <- steps | step.1 <= t1]).2 <=
(last (t__d2, v__d2)
   [seq step <- steps | step.1 <= t2]).2
steps_sorted: path leq_steps (t__c, v__c) steps
t__d1, v__d1, t__d2, v__d2: nat
LEv: v__d1 <= v__d2
LTN1: leq_steps (t__d1, v__d1) (t__c, v__c)
ALL1: {in steps,
  forall x : nat * nat,
  leq_steps (t__d1, v__d1) x}
LTN2: leq_steps (t__d2, v__d2) (t__c, v__c)
ALL2: {in steps,
  forall x : nat * nat,
  leq_steps (t__d2, v__d2) x}
ALL: all (leq_steps (t__c, v__c)) steps
SORT: sorted leq_steps steps
R1: t__c <= t1
R2: t__c <= t2
(last (t__d1, v__d1)
   (if t__c <= t1
    then
     (t__c, v__c)
     :: [seq step <- steps | step.1 <= t1]
    else [seq step <- steps | step.1 <= t1])).2 <=
(last (t__d2, v__d2)
   (if t__c <= t2
    then
     (t__c, v__c)
     :: [seq step <- steps | step.1 <= t2]
    else [seq step <- steps | step.1 <= t2])).2 by rewrite R1 R2 //=; apply: IHsteps. }
ac_prefix: ArrivalCurvePrefix
h: duration
t1, t2: nat
LE: t1 <= t2
t__c: duration
v__c: nat
steps: seq (duration * nat)
IHsteps: sorted leq_steps steps ->
forall t__d1 v__d1 t__d2 v__d2 : nat,
v__d1 <= v__d2 ->
all (leq_steps (t__d1, v__d1)) steps ->
all (leq_steps (t__d2, v__d2)) steps ->
(last (t__d1, v__d1)
   [seq step <- steps | step.1 <= t1]).2 <=
(last (t__d2, v__d2)
   [seq step <- steps | step.1 <= t2]).2
steps_sorted: path leq_steps (t__c, v__c) steps
t__d1, v__d1, t__d2, v__d2: nat
LEv: v__d1 <= v__d2
LTN1: leq_steps (t__d1, v__d1) (t__c, v__c)
ALL1: {in steps,
  forall x : nat * nat,
  leq_steps (t__d1, v__d1) x}
LTN2: leq_steps (t__d2, v__d2) (t__c, v__c)
ALL2: {in steps,
  forall x : nat * nat,
  leq_steps (t__d2, v__d2) x}
ALL: all (leq_steps (t__c, v__c)) steps
SORT: sorted leq_steps steps
R1: t__c <= t1
R2: t2 < t__c
(last (t__d1, v__d1)
   (if t__c <= t1
    then
     (t__c, v__c)
     :: [seq step <- steps | step.1 <= t1]
    else [seq step <- steps | step.1 <= t1])).2 <=
(last (t__d2, v__d2)
   (if t__c <= t2
    then
     (t__c, v__c)
     :: [seq step <- steps | step.1 <= t2]
    else [seq step <- steps | step.1 <= t2])).2
ac_prefix: ArrivalCurvePrefix
h: duration
t1, t2: nat
LE: t1 <= t2
t__c: duration
v__c: nat
steps: seq (duration * nat)
IHsteps: sorted leq_steps steps ->
forall t__d1 v__d1 t__d2 v__d2 : nat,
v__d1 <= v__d2 ->
all (leq_steps (t__d1, v__d1)) steps ->
all (leq_steps (t__d2, v__d2)) steps ->
(last (t__d1, v__d1)
   [seq step <- steps | step.1 <= t1]).2 <=
(last (t__d2, v__d2)
   [seq step <- steps | step.1 <= t2]).2
steps_sorted: path leq_steps (t__c, v__c) steps
t__d1, v__d1, t__d2, v__d2: nat
LEv: v__d1 <= v__d2
LTN1: leq_steps (t__d1, v__d1) (t__c, v__c)
ALL1: {in steps,
  forall x : nat * nat,
  leq_steps (t__d1, v__d1) x}
LTN2: leq_steps (t__d2, v__d2) (t__c, v__c)
ALL2: {in steps,
  forall x : nat * nat,
  leq_steps (t__d2, v__d2) x}
ALL: all (leq_steps (t__c, v__c)) steps
SORT: sorted leq_steps steps
R1: t1 < t__c
R2: t__c <= t2
(last (t__d1, v__d1)
   (if t__c <= t1
    then
     (t__c, v__c)
     :: [seq step <- steps | step.1 <= t1]
    else [seq step <- steps | step.1 <= t1])).2 <=
(last (t__d2, v__d2)
   (if t__c <= t2
    then
     (t__c, v__c)
     :: [seq step <- steps | step.1 <= t2]
    else [seq step <- steps | step.1 <= t2])).2
ac_prefix: ArrivalCurvePrefix
h: duration
t1, t2: nat
LE: t1 <= t2
t__c: duration
v__c: nat
steps: seq (duration * nat)
IHsteps: sorted leq_steps steps ->
forall t__d1 v__d1 t__d2 v__d2 : nat,
v__d1 <= v__d2 ->
all (leq_steps (t__d1, v__d1)) steps ->
all (leq_steps (t__d2, v__d2)) steps ->
(last (t__d1, v__d1)
   [seq step <- steps | step.1 <= t1]).2 <=
(last (t__d2, v__d2)
   [seq step <- steps | step.1 <= t2]).2
steps_sorted: path leq_steps (t__c, v__c) steps
t__d1, v__d1, t__d2, v__d2: nat
LEv: v__d1 <= v__d2
LTN1: leq_steps (t__d1, v__d1) (t__c, v__c)
ALL1: {in steps,
  forall x : nat * nat,
  leq_steps (t__d1, v__d1) x}
LTN2: leq_steps (t__d2, v__d2) (t__c, v__c)
ALL2: {in steps,
  forall x : nat * nat,
  leq_steps (t__d2, v__d2) x}
ALL: all (leq_steps (t__c, v__c)) steps
SORT: sorted leq_steps steps
R1: t1 < t__c
R2: t2 < t__c
(last (t__d1, v__d1)
   (if t__c <= t1
    then
     (t__c, v__c)
     :: [seq step <- steps | step.1 <= t1]
    else [seq step <- steps | step.1 <= t1])).2 <=
(last (t__d2, v__d2)
   (if t__c <= t2
    then
     (t__c, v__c)
     :: [seq step <- steps | step.1 <= t2]
    else [seq step <- steps | step.1 <= t2])).2
      {
ac_prefix: ArrivalCurvePrefix
h: duration
t1, t2: nat
LE: t1 <= t2
t__c: duration
v__c: nat
steps: seq (duration * nat)
IHsteps: sorted leq_steps steps ->
forall t__d1 v__d1 t__d2 v__d2 : nat,
v__d1 <= v__d2 ->
all (leq_steps (t__d1, v__d1)) steps ->
all (leq_steps (t__d2, v__d2)) steps ->
(last (t__d1, v__d1)
   [seq step <- steps | step.1 <= t1]).2 <=
(last (t__d2, v__d2)
   [seq step <- steps | step.1 <= t2]).2
steps_sorted: path leq_steps (t__c, v__c) steps
t__d1, v__d1, t__d2, v__d2: nat
LEv: v__d1 <= v__d2
LTN1: leq_steps (t__d1, v__d1) (t__c, v__c)
ALL1: {in steps,
  forall x : nat * nat,
  leq_steps (t__d1, v__d1) x}
LTN2: leq_steps (t__d2, v__d2) (t__c, v__c)
ALL2: {in steps,
  forall x : nat * nat,
  leq_steps (t__d2, v__d2) x}
ALL: all (leq_steps (t__c, v__c)) steps
SORT: sorted leq_steps steps
R1: t__c <= t1
R2: t2 < t__c
(last (t__d1, v__d1)
   (if t__c <= t1
    then
     (t__c, v__c)
     :: [seq step <- steps | step.1 <= t1]
    else [seq step <- steps | step.1 <= t1])).2 <=
(last (t__d2, v__d2)
   (if t__c <= t2
    then
     (t__c, v__c)
     :: [seq step <- steps | step.1 <= t2]
    else [seq step <- steps | step.1 <= t2])).2 lia. }
ac_prefix: ArrivalCurvePrefix
h: duration
t1, t2: nat
LE: t1 <= t2
t__c: duration
v__c: nat
steps: seq (duration * nat)
IHsteps: sorted leq_steps steps ->
forall t__d1 v__d1 t__d2 v__d2 : nat,
v__d1 <= v__d2 ->
all (leq_steps (t__d1, v__d1)) steps ->
all (leq_steps (t__d2, v__d2)) steps ->
(last (t__d1, v__d1)
   [seq step <- steps | step.1 <= t1]).2 <=
(last (t__d2, v__d2)
   [seq step <- steps | step.1 <= t2]).2
steps_sorted: path leq_steps (t__c, v__c) steps
t__d1, v__d1, t__d2, v__d2: nat
LEv: v__d1 <= v__d2
LTN1: leq_steps (t__d1, v__d1) (t__c, v__c)
ALL1: {in steps,
  forall x : nat * nat,
  leq_steps (t__d1, v__d1) x}
LTN2: leq_steps (t__d2, v__d2) (t__c, v__c)
ALL2: {in steps,
  forall x : nat * nat,
  leq_steps (t__d2, v__d2) x}
ALL: all (leq_steps (t__c, v__c)) steps
SORT: sorted leq_steps steps
R1: t1 < t__c
R2: t__c <= t2
(last (t__d1, v__d1)
   (if t__c <= t1
    then
     (t__c, v__c)
     :: [seq step <- steps | step.1 <= t1]
    else [seq step <- steps | step.1 <= t1])).2 <=
(last (t__d2, v__d2)
   (if t__c <= t2
    then
     (t__c, v__c)
     :: [seq step <- steps | step.1 <= t2]
    else [seq step <- steps | step.1 <= t2])).2
ac_prefix: ArrivalCurvePrefix
h: duration
t1, t2: nat
LE: t1 <= t2
t__c: duration
v__c: nat
steps: seq (duration * nat)
IHsteps: sorted leq_steps steps ->
forall t__d1 v__d1 t__d2 v__d2 : nat,
v__d1 <= v__d2 ->
all (leq_steps (t__d1, v__d1)) steps ->
all (leq_steps (t__d2, v__d2)) steps ->
(last (t__d1, v__d1)
   [seq step <- steps | step.1 <= t1]).2 <=
(last (t__d2, v__d2)
   [seq step <- steps | step.1 <= t2]).2
steps_sorted: path leq_steps (t__c, v__c) steps
t__d1, v__d1, t__d2, v__d2: nat
LEv: v__d1 <= v__d2
LTN1: leq_steps (t__d1, v__d1) (t__c, v__c)
ALL1: {in steps,
  forall x : nat * nat,
  leq_steps (t__d1, v__d1) x}
LTN2: leq_steps (t__d2, v__d2) (t__c, v__c)
ALL2: {in steps,
  forall x : nat * nat,
  leq_steps (t__d2, v__d2) x}
ALL: all (leq_steps (t__c, v__c)) steps
SORT: sorted leq_steps steps
R1: t1 < t__c
R2: t2 < t__c
(last (t__d1, v__d1)
   (if t__c <= t1
    then
     (t__c, v__c)
     :: [seq step <- steps | step.1 <= t1]
    else [seq step <- steps | step.1 <= t1])).2 <=
(last (t__d2, v__d2)
   (if t__c <= t2
    then
     (t__c, v__c)
     :: [seq step <- steps | step.1 <= t2]
    else [seq step <- steps | step.1 <= t2])).2
      {
ac_prefix: ArrivalCurvePrefix
h: duration
t1, t2: nat
LE: t1 <= t2
t__c: duration
v__c: nat
steps: seq (duration * nat)
IHsteps: sorted leq_steps steps ->
forall t__d1 v__d1 t__d2 v__d2 : nat,
v__d1 <= v__d2 ->
all (leq_steps (t__d1, v__d1)) steps ->
all (leq_steps (t__d2, v__d2)) steps ->
(last (t__d1, v__d1)
   [seq step <- steps | step.1 <= t1]).2 <=
(last (t__d2, v__d2)
   [seq step <- steps | step.1 <= t2]).2
steps_sorted: path leq_steps (t__c, v__c) steps
t__d1, v__d1, t__d2, v__d2: nat
LEv: v__d1 <= v__d2
LTN1: leq_steps (t__d1, v__d1) (t__c, v__c)
ALL1: {in steps,
  forall x : nat * nat,
  leq_steps (t__d1, v__d1) x}
LTN2: leq_steps (t__d2, v__d2) (t__c, v__c)
ALL2: {in steps,
  forall x : nat * nat,
  leq_steps (t__d2, v__d2) x}
ALL: all (leq_steps (t__c, v__c)) steps
SORT: sorted leq_steps steps
R1: t1 < t__c
R2: t__c <= t2
(last (t__d1, v__d1)
   (if t__c <= t1
    then
     (t__c, v__c)
     :: [seq step <- steps | step.1 <= t1]
    else [seq step <- steps | step.1 <= t1])).2 <=
(last (t__d2, v__d2)
   (if t__c <= t2
    then
     (t__c, v__c)
     :: [seq step <- steps | step.1 <= t2]
    else [seq step <- steps | step.1 <= t2])).2 rewrite ltnNge -eqbF_neg in R1; move: R1 => /eqP ->; rewrite R2 //=; apply IHsteps => //.
ac_prefix: ArrivalCurvePrefix
h: duration
t1, t2: nat
LE: t1 <= t2
t__c: duration
v__c: nat
steps: seq (duration * nat)
IHsteps: sorted leq_steps steps ->
forall t__d1 v__d1 t__d2 v__d2 : nat,
v__d1 <= v__d2 ->
all (leq_steps (t__d1, v__d1)) steps ->
all (leq_steps (t__d2, v__d2)) steps ->
(last (t__d1, v__d1)
   [seq step <- steps | step.1 <= t1]).2 <=
(last (t__d2, v__d2)
   [seq step <- steps | step.1 <= t2]).2
steps_sorted: path leq_steps (t__c, v__c) steps
t__d1, v__d1, t__d2, v__d2: nat
LEv: v__d1 <= v__d2
LTN1: leq_steps (t__d1, v__d1) (t__c, v__c)
ALL1: {in steps,
  forall x : nat * nat,
  leq_steps (t__d1, v__d1) x}
LTN2: leq_steps (t__d2, v__d2) (t__c, v__c)
ALL2: {in steps,
  forall x : nat * nat,
  leq_steps (t__d2, v__d2) x}
ALL: all (leq_steps (t__c, v__c)) steps
SORT: sorted leq_steps steps
R2: t__c <= t2
v__d1 <= v__c
ac_prefix: ArrivalCurvePrefix
h: duration
t1, t2: nat
LE: t1 <= t2
t__c: duration
v__c: nat
steps: seq (duration * nat)
IHsteps: sorted leq_steps steps ->
forall t__d1 v__d1 t__d2 v__d2 : nat,
v__d1 <= v__d2 ->
all (leq_steps (t__d1, v__d1)) steps ->
all (leq_steps (t__d2, v__d2)) steps ->
(last (t__d1, v__d1)
   [seq step <- steps | step.1 <= t1]).2 <=
(last (t__d2, v__d2)
   [seq step <- steps | step.1 <= t2]).2
steps_sorted: path leq_steps (t__c, v__c) steps
t__d1, v__d1, t__d2, v__d2: nat
LEv: v__d1 <= v__d2
LTN1: leq_steps (t__d1, v__d1) (t__c, v__c)
ALL1: {in steps,
  forall x : nat * nat,
  leq_steps (t__d1, v__d1) x}
LTN2: leq_steps (t__d2, v__d2) (t__c, v__c)
ALL2: {in steps,
  forall x : nat * nat,
  leq_steps (t__d2, v__d2) x}
ALL: all (leq_steps (t__c, v__c)) steps
SORT: sorted leq_steps steps
R2: t__c <= t2
all (leq_steps (t__d1, v__d1)) steps
        -
ac_prefix: ArrivalCurvePrefix
h: duration
t1, t2: nat
LE: t1 <= t2
t__c: duration
v__c: nat
steps: seq (duration * nat)
IHsteps: sorted leq_steps steps ->
forall t__d1 v__d1 t__d2 v__d2 : nat,
v__d1 <= v__d2 ->
all (leq_steps (t__d1, v__d1)) steps ->
all (leq_steps (t__d2, v__d2)) steps ->
(last (t__d1, v__d1)
   [seq step <- steps | step.1 <= t1]).2 <=
(last (t__d2, v__d2)
   [seq step <- steps | step.1 <= t2]).2
steps_sorted: path leq_steps (t__c, v__c) steps
t__d1, v__d1, t__d2, v__d2: nat
LEv: v__d1 <= v__d2
LTN1: leq_steps (t__d1, v__d1) (t__c, v__c)
ALL1: {in steps,
  forall x : nat * nat,
  leq_steps (t__d1, v__d1) x}
LTN2: leq_steps (t__d2, v__d2) (t__c, v__c)
ALL2: {in steps,
  forall x : nat * nat,
  leq_steps (t__d2, v__d2) x}
ALL: all (leq_steps (t__c, v__c)) steps
SORT: sorted leq_steps steps
R2: t__c <= t2
v__d1 <= v__c by move: LTN1; rewrite /leq_steps => /andP //= [_ LEc].
        -
ac_prefix: ArrivalCurvePrefix
h: duration
t1, t2: nat
LE: t1 <= t2
t__c: duration
v__c: nat
steps: seq (duration * nat)
IHsteps: sorted leq_steps steps ->
forall t__d1 v__d1 t__d2 v__d2 : nat,
v__d1 <= v__d2 ->
all (leq_steps (t__d1, v__d1)) steps ->
all (leq_steps (t__d2, v__d2)) steps ->
(last (t__d1, v__d1)
   [seq step <- steps | step.1 <= t1]).2 <=
(last (t__d2, v__d2)
   [seq step <- steps | step.1 <= t2]).2
steps_sorted: path leq_steps (t__c, v__c) steps
t__d1, v__d1, t__d2, v__d2: nat
LEv: v__d1 <= v__d2
LTN1: leq_steps (t__d1, v__d1) (t__c, v__c)
ALL1: {in steps,
  forall x : nat * nat,
  leq_steps (t__d1, v__d1) x}
LTN2: leq_steps (t__d2, v__d2) (t__c, v__c)
ALL2: {in steps,
  forall x : nat * nat,
  leq_steps (t__d2, v__d2) x}
ALL: all (leq_steps (t__c, v__c)) steps
SORT: sorted leq_steps steps
R2: t__c <= t2
all (leq_steps (t__d1, v__d1)) steps by apply/allP.
      }
ac_prefix: ArrivalCurvePrefix
h: duration
t1, t2: nat
LE: t1 <= t2
t__c: duration
v__c: nat
steps: seq (duration * nat)
IHsteps: sorted leq_steps steps ->
forall t__d1 v__d1 t__d2 v__d2 : nat,
v__d1 <= v__d2 ->
all (leq_steps (t__d1, v__d1)) steps ->
all (leq_steps (t__d2, v__d2)) steps ->
(last (t__d1, v__d1)
   [seq step <- steps | step.1 <= t1]).2 <=
(last (t__d2, v__d2)
   [seq step <- steps | step.1 <= t2]).2
steps_sorted: path leq_steps (t__c, v__c) steps
t__d1, v__d1, t__d2, v__d2: nat
LEv: v__d1 <= v__d2
LTN1: leq_steps (t__d1, v__d1) (t__c, v__c)
ALL1: {in steps,
  forall x : nat * nat,
  leq_steps (t__d1, v__d1) x}
LTN2: leq_steps (t__d2, v__d2) (t__c, v__c)
ALL2: {in steps,
  forall x : nat * nat,
  leq_steps (t__d2, v__d2) x}
ALL: all (leq_steps (t__c, v__c)) steps
SORT: sorted leq_steps steps
R1: t1 < t__c
R2: t2 < t__c
(last (t__d1, v__d1)
   (if t__c <= t1
    then
     (t__c, v__c)
     :: [seq step <- steps | step.1 <= t1]
    else [seq step <- steps | step.1 <= t1])).2 <=
(last (t__d2, v__d2)
   (if t__c <= t2
    then
     (t__c, v__c)
     :: [seq step <- steps | step.1 <= t2]
    else [seq step <- steps | step.1 <= t2])).2
      {
ac_prefix: ArrivalCurvePrefix
h: duration
t1, t2: nat
LE: t1 <= t2
t__c: duration
v__c: nat
steps: seq (duration * nat)
IHsteps: sorted leq_steps steps ->
forall t__d1 v__d1 t__d2 v__d2 : nat,
v__d1 <= v__d2 ->
all (leq_steps (t__d1, v__d1)) steps ->
all (leq_steps (t__d2, v__d2)) steps ->
(last (t__d1, v__d1)
   [seq step <- steps | step.1 <= t1]).2 <=
(last (t__d2, v__d2)
   [seq step <- steps | step.1 <= t2]).2
steps_sorted: path leq_steps (t__c, v__c) steps
t__d1, v__d1, t__d2, v__d2: nat
LEv: v__d1 <= v__d2
LTN1: leq_steps (t__d1, v__d1) (t__c, v__c)
ALL1: {in steps,
  forall x : nat * nat,
  leq_steps (t__d1, v__d1) x}
LTN2: leq_steps (t__d2, v__d2) (t__c, v__c)
ALL2: {in steps,
  forall x : nat * nat,
  leq_steps (t__d2, v__d2) x}
ALL: all (leq_steps (t__c, v__c)) steps
SORT: sorted leq_steps steps
R1: t1 < t__c
R2: t2 < t__c
(last (t__d1, v__d1)
   (if t__c <= t1
    then
     (t__c, v__c)
     :: [seq step <- steps | step.1 <= t1]
    else [seq step <- steps | step.1 <= t1])).2 <=
(last (t__d2, v__d2)
   (if t__c <= t2
    then
     (t__c, v__c)
     :: [seq step <- steps | step.1 <= t2]
    else [seq step <- steps | step.1 <= t2])).2 rewrite ltnNge -eqbF_neg in R1; move: R1 => /eqP ->.
ac_prefix: ArrivalCurvePrefix
h: duration
t1, t2: nat
LE: t1 <= t2
t__c: duration
v__c: nat
steps: seq (duration * nat)
IHsteps: sorted leq_steps steps ->
forall t__d1 v__d1 t__d2 v__d2 : nat,
v__d1 <= v__d2 ->
all (leq_steps (t__d1, v__d1)) steps ->
all (leq_steps (t__d2, v__d2)) steps ->
(last (t__d1, v__d1)
   [seq step <- steps | step.1 <= t1]).2 <=
(last (t__d2, v__d2)
   [seq step <- steps | step.1 <= t2]).2
steps_sorted: path leq_steps (t__c, v__c) steps
t__d1, v__d1, t__d2, v__d2: nat
LEv: v__d1 <= v__d2
LTN1: leq_steps (t__d1, v__d1) (t__c, v__c)
ALL1: {in steps,
  forall x : nat * nat,
  leq_steps (t__d1, v__d1) x}
LTN2: leq_steps (t__d2, v__d2) (t__c, v__c)
ALL2: {in steps,
  forall x : nat * nat,
  leq_steps (t__d2, v__d2) x}
ALL: all (leq_steps (t__c, v__c)) steps
SORT: sorted leq_steps steps
R2: t2 < t__c
(last (t__d1, v__d1)
   [seq step <- steps | step.1 <= t1]).2 <=
(last (t__d2, v__d2)
   (if t__c <= t2
    then
     (t__c, v__c)
     :: [seq step <- steps | step.1 <= t2]
    else [seq step <- steps | step.1 <= t2])).2
        rewrite ltnNge -eqbF_neg in R2; move: R2 => /eqP ->.
ac_prefix: ArrivalCurvePrefix
h: duration
t1, t2: nat
LE: t1 <= t2
t__c: duration
v__c: nat
steps: seq (duration * nat)
IHsteps: sorted leq_steps steps ->
forall t__d1 v__d1 t__d2 v__d2 : nat,
v__d1 <= v__d2 ->
all (leq_steps (t__d1, v__d1)) steps ->
all (leq_steps (t__d2, v__d2)) steps ->
(last (t__d1, v__d1)
   [seq step <- steps | step.1 <= t1]).2 <=
(last (t__d2, v__d2)
   [seq step <- steps | step.1 <= t2]).2
steps_sorted: path leq_steps (t__c, v__c) steps
t__d1, v__d1, t__d2, v__d2: nat
LEv: v__d1 <= v__d2
LTN1: leq_steps (t__d1, v__d1) (t__c, v__c)
ALL1: {in steps,
  forall x : nat * nat,
  leq_steps (t__d1, v__d1) x}
LTN2: leq_steps (t__d2, v__d2) (t__c, v__c)
ALL2: {in steps,
  forall x : nat * nat,
  leq_steps (t__d2, v__d2) x}
ALL: all (leq_steps (t__c, v__c)) steps
SORT: sorted leq_steps steps
(last (t__d1, v__d1)
   [seq step <- steps | step.1 <= t1]).2 <=
(last (t__d2, v__d2)
   [seq step <- steps | step.1 <= t2]).2
        by apply IHsteps => //; apply/allP.
      }
    }
ac_prefix: ArrivalCurvePrefix
h: duration
steps: seq (duration * nat)
H_sorted_leq: sorted leq_steps (h, steps).2
t1, t2: nat
LE: t1 <= t2
GenLem: forall t__d1 v__d1 t__d2 v__d2 : nat,
v__d1 <= v__d2 ->
all (leq_steps (t__d1, v__d1)) steps ->
all (leq_steps (t__d2, v__d2)) steps ->
(last (t__d1, v__d1)
   [seq step <- steps | step.1 <= t1]).2 <=
(last (t__d2, v__d2)
   [seq step <- steps | step.1 <= t2]).2
(last (0, 0) [seq step <- steps | step.1 <= t1]).2 <=
(last (0, 0) [seq step <- steps | step.1 <= t2]).2
    by apply: GenLem => [//||];  apply/allP; intros x _; rewrite /leq_steps //=.
  Qed.

  (** Next, we prove a correctness claim stating that if [value_at]
      makes a step at time instant [t + ε] (that is, [value_at t <
      value_at (t + ε)]), then [steps_of ac_prefix] contains a step
      [(t + ε, v)] for some [v]. *)
  Lemma value_at_change_is_in_steps_of :
    forall t,
      value_at ac_prefix t < value_at ac_prefix (t + ε) ->
      exists v, (t + ε, v) \in steps_of ac_prefix.
ac_prefix: ArrivalCurvePrefix
H_sorted_leq: sorted_leq_steps ac_prefix
H_no_inf_arrivals: no_inf_arrivals ac_prefix
forall t : duration,
value_at ac_prefix t < value_at ac_prefix (t + 1) ->
exists v : Datatypes_nat__canonical__eqtype_Equality,
  (t + 1, v) \in steps_of ac_prefix
  Proof.
ac_prefix: ArrivalCurvePrefix
H_sorted_leq: sorted_leq_steps ac_prefix
H_no_inf_arrivals: no_inf_arrivals ac_prefix
forall t : duration,
value_at ac_prefix t < value_at ac_prefix (t + 1) ->
exists v : Datatypes_nat__canonical__eqtype_Equality,
  (t + 1, v) \in steps_of ac_prefix
    move=> t LT /=.
ac_prefix: ArrivalCurvePrefix
H_sorted_leq: sorted_leq_steps ac_prefix
H_no_inf_arrivals: no_inf_arrivals ac_prefix
t: duration
LT: value_at ac_prefix t < value_at ac_prefix (t + 1)
exists v : nat, (t + 1, v) \in steps_of ac_prefix
    unfold value_at, step_at in LT.
ac_prefix: ArrivalCurvePrefix
H_sorted_leq: sorted_leq_steps ac_prefix
H_no_inf_arrivals: no_inf_arrivals ac_prefix
t: duration
LT: (last (0, 0)
   [seq step <- steps_of ac_prefix | step.1 <= t]).2 <
(last (0, 0)
   [seq step <- steps_of ac_prefix
      | step.1 <= t + 1]).2
exists v : nat, (t + 1, v) \in steps_of ac_prefix
    destruct ac_prefix as [h2 steps]; simpl in LT.
ac_prefix: ArrivalCurvePrefix
h2: duration
steps: seq (duration * nat)
H_sorted_leq: sorted_leq_steps (h2, steps)
H_no_inf_arrivals: no_inf_arrivals (h2, steps)
t: duration
LT: (last (0, 0) [seq step <- steps | step.1 <= t]).2 <
(last (0, 0)
   [seq step <- steps | step.1 <= t + 1]).2
exists v : nat, (t + 1, v) \in steps_of (h2, steps)
    rewrite [in X in _ < X](sorted_split _ _ fst t) /= in LT.
ac_prefix: ArrivalCurvePrefix
h2: duration
steps: seq (duration * nat)
H_sorted_leq: sorted_leq_steps (h2, steps)
H_no_inf_arrivals: no_inf_arrivals (h2, steps)
t: duration
LT: (last (0, 0) [seq step <- steps | step.1 <= t]).2 <
(last (0, 0)
   ([seq x <- steps | x.1 <= t + 1 & x.1 <= t] ++
    [seq x <- steps | x.1 <= t + 1 & t < x.1])).2
exists v : nat, (t + 1, v) \in steps_of (h2, steps)
ac_prefix: ArrivalCurvePrefix
h2: duration
steps: seq (duration * nat)
H_sorted_leq: sorted_leq_steps (h2, steps)
H_no_inf_arrivals: no_inf_arrivals (h2, steps)
t: duration
sorted (fun x y : nat * nat => x.1 <= y.1) steps
    {
ac_prefix: ArrivalCurvePrefix
h2: duration
steps: seq (duration * nat)
H_sorted_leq: sorted_leq_steps (h2, steps)
H_no_inf_arrivals: no_inf_arrivals (h2, steps)
t: duration
LT: (last (0, 0) [seq step <- steps | step.1 <= t]).2 <
(last (0, 0)
   ([seq x <- steps | x.1 <= t + 1 & x.1 <= t] ++
    [seq x <- steps | x.1 <= t + 1 & t < x.1])).2
exists v : nat, (t + 1, v) \in steps_of (h2, steps) rewrite [in X in _ ++ X](eq_filter (a2 := fun x => fst x == t + ε)) in LT; last first.
ac_prefix: ArrivalCurvePrefix
h2: duration
steps: seq (duration * nat)
H_sorted_leq: sorted_leq_steps (h2, steps)
H_no_inf_arrivals: no_inf_arrivals (h2, steps)
t: duration
(fun x : nat * nat => (x.1 <= t + 1) && (t < x.1)) =1
(fun
   x : Datatypes_nat__canonical__eqtype_Equality * nat
 => x.1 == t + 1)
ac_prefix: ArrivalCurvePrefix
h2: duration
steps: seq (duration * nat)
H_sorted_leq: sorted_leq_steps (h2, steps)
H_no_inf_arrivals: no_inf_arrivals (h2, steps)
t: duration
LT: (last (0, 0) [seq step <- steps | step.1 <= t]).2 <
(last (0, 0)
   ([seq x <- steps | x.1 <= t + 1 & x.1 <= t] ++
    [seq x <- steps | x.1 == t + 1])).2
exists v : nat, (t + 1, v) \in steps_of (h2, steps)
      {
ac_prefix: ArrivalCurvePrefix
h2: duration
steps: seq (duration * nat)
H_sorted_leq: sorted_leq_steps (h2, steps)
H_no_inf_arrivals: no_inf_arrivals (h2, steps)
t: duration
(fun x : nat * nat => (x.1 <= t + 1) && (t < x.1)) =1
(fun
   x : Datatypes_nat__canonical__eqtype_Equality * nat
 => x.1 == t + 1) by move=> [a b] /=; lia. }
ac_prefix: ArrivalCurvePrefix
h2: duration
steps: seq (duration * nat)
H_sorted_leq: sorted_leq_steps (h2, steps)
H_no_inf_arrivals: no_inf_arrivals (h2, steps)
t: duration
LT: (last (0, 0) [seq step <- steps | step.1 <= t]).2 <
(last (0, 0)
   ([seq x <- steps | x.1 <= t + 1 & x.1 <= t] ++
    [seq x <- steps | x.1 == t + 1])).2
exists v : nat, (t + 1, v) \in steps_of (h2, steps)
      {
ac_prefix: ArrivalCurvePrefix
h2: duration
steps: seq (duration * nat)
H_sorted_leq: sorted_leq_steps (h2, steps)
H_no_inf_arrivals: no_inf_arrivals (h2, steps)
t: duration
LT: (last (0, 0) [seq step <- steps | step.1 <= t]).2 <
(last (0, 0)
   ([seq x <- steps | x.1 <= t + 1 & x.1 <= t] ++
    [seq x <- steps | x.1 == t + 1])).2
exists v : nat, (t + 1, v) \in steps_of (h2, steps) destruct ([seq x <- steps | fst x == t + ε]) as [|p l] eqn:LST => //=.
ac_prefix: ArrivalCurvePrefix
h2: duration
steps: seq (duration * nat)
H_sorted_leq: sorted_leq_steps (h2, steps)
H_no_inf_arrivals: no_inf_arrivals (h2, steps)
t: duration
LST: [seq x <- steps | x.1 == t + 1] = [::]
LT: (last (0, 0) [seq step <- steps | step.1 <= t]).2 <
(last (0, 0)
   ([seq x <- steps | x.1 <= t + 1 & x.1 <= t] ++
    [::])).2
exists v : nat, (t + 1, v) \in steps
ac_prefix: ArrivalCurvePrefix
h2: duration
steps: seq (duration * nat)
H_sorted_leq: sorted_leq_steps (h2, steps)
H_no_inf_arrivals: no_inf_arrivals (h2, steps)
t: duration
p: (Datatypes_nat__canonical__eqtype_Equality * nat)%type
l: seq
  (Datatypes_nat__canonical__eqtype_Equality * nat)
LST: [seq x <- steps | x.1 == t + 1] = p :: l
LT: (last (0, 0) [seq step <- steps | step.1 <= t]).2 <
(last (0, 0)
   ([seq x <- steps | x.1 <= t + 1 & x.1 <= t] ++
    p :: l)).2
exists v : nat, (t + 1, v) \in steps
        {
ac_prefix: ArrivalCurvePrefix
h2: duration
steps: seq (duration * nat)
H_sorted_leq: sorted_leq_steps (h2, steps)
H_no_inf_arrivals: no_inf_arrivals (h2, steps)
t: duration
LST: [seq x <- steps | x.1 == t + 1] = [::]
LT: (last (0, 0) [seq step <- steps | step.1 <= t]).2 <
(last (0, 0)
   ([seq x <- steps | x.1 <= t + 1 & x.1 <= t] ++
    [::])).2
exists v : nat, (t + 1, v) \in steps rewrite [in X in X ++ _](eq_filter (a2 := fun x => fst x <= t)) in LT; last first.
ac_prefix: ArrivalCurvePrefix
h2: duration
steps: seq (duration * nat)
H_sorted_leq: sorted_leq_steps (h2, steps)
H_no_inf_arrivals: no_inf_arrivals (h2, steps)
t: duration
LST: [seq x <- steps | x.1 == t + 1] = [::]
(fun x : nat * nat => (x.1 <= t + 1) && (x.1 <= t)) =1
(fun x : nat * nat => x.1 <= t)
ac_prefix: ArrivalCurvePrefix
h2: duration
steps: seq (duration * nat)
H_sorted_leq: sorted_leq_steps (h2, steps)
H_no_inf_arrivals: no_inf_arrivals (h2, steps)
t: duration
LST: [seq x <- steps | x.1 == t + 1] = [::]
LT: (last (0, 0) [seq step <- steps | step.1 <= t]).2 <
(last (0, 0)
   ([seq x <- steps | x.1 <= t] ++ [::])).2
exists v : nat, (t + 1, v) \in steps
          {
ac_prefix: ArrivalCurvePrefix
h2: duration
steps: seq (duration * nat)
H_sorted_leq: sorted_leq_steps (h2, steps)
H_no_inf_arrivals: no_inf_arrivals (h2, steps)
t: duration
LST: [seq x <- steps | x.1 == t + 1] = [::]
(fun x : nat * nat => (x.1 <= t + 1) && (x.1 <= t)) =1
(fun x : nat * nat => x.1 <= t) clear; intros [a b]; simpl.
t: duration
a, b: nat
(a <= t + 1) && (a <= t) = (a <= t)
            destruct (leqP a t).
t: duration
a, b: nat
i: a <= t
(a <= t + 1) && true = true
t: duration
a, b: nat
i: t < a
(a <= t + 1) && false = false
            -
t: duration
a, b: nat
i: a <= t
(a <= t + 1) && true = true by rewrite Bool.andb_true_r; apply/eqP; lia.
            -
t: duration
a, b: nat
i: t < a
(a <= t + 1) && false = false by rewrite Bool.andb_false_r.
          }
ac_prefix: ArrivalCurvePrefix
h2: duration
steps: seq (duration * nat)
H_sorted_leq: sorted_leq_steps (h2, steps)
H_no_inf_arrivals: no_inf_arrivals (h2, steps)
t: duration
LST: [seq x <- steps | x.1 == t + 1] = [::]
LT: (last (0, 0) [seq step <- steps | step.1 <= t]).2 <
(last (0, 0)
   ([seq x <- steps | x.1 <= t] ++ [::])).2
exists v : nat, (t + 1, v) \in steps
          {
ac_prefix: ArrivalCurvePrefix
h2: duration
steps: seq (duration * nat)
H_sorted_leq: sorted_leq_steps (h2, steps)
H_no_inf_arrivals: no_inf_arrivals (h2, steps)
t: duration
LST: [seq x <- steps | x.1 == t + 1] = [::]
LT: (last (0, 0) [seq step <- steps | step.1 <= t]).2 <
(last (0, 0)
   ([seq x <- steps | x.1 <= t] ++ [::])).2
exists v : nat, (t + 1, v) \in steps by rewrite cats0 ltnn in LT. }
        }
ac_prefix: ArrivalCurvePrefix
h2: duration
steps: seq (duration * nat)
H_sorted_leq: sorted_leq_steps (h2, steps)
H_no_inf_arrivals: no_inf_arrivals (h2, steps)
t: duration
p: (Datatypes_nat__canonical__eqtype_Equality * nat)%type
l: seq
  (Datatypes_nat__canonical__eqtype_Equality * nat)
LST: [seq x <- steps | x.1 == t + 1] = p :: l
LT: (last (0, 0) [seq step <- steps | step.1 <= t]).2 <
(last (0, 0)
   ([seq x <- steps | x.1 <= t + 1 & x.1 <= t] ++
    p :: l)).2
exists v : nat, (t + 1, v) \in steps
        {
ac_prefix: ArrivalCurvePrefix
h2: duration
steps: seq (duration * nat)
H_sorted_leq: sorted_leq_steps (h2, steps)
H_no_inf_arrivals: no_inf_arrivals (h2, steps)
t: duration
p: (Datatypes_nat__canonical__eqtype_Equality * nat)%type
l: seq
  (Datatypes_nat__canonical__eqtype_Equality * nat)
LST: [seq x <- steps | x.1 == t + 1] = p :: l
LT: (last (0, 0) [seq step <- steps | step.1 <= t]).2 <
(last (0, 0)
   ([seq x <- steps | x.1 <= t + 1 & x.1 <= t] ++
    p :: l)).2
exists v : nat, (t + 1, v) \in steps have: p \in [seq x <- steps | x.1 == t + 1]
            by rewrite LST; apply: mem_head.
ac_prefix: ArrivalCurvePrefix
h2: duration
steps: seq (duration * nat)
H_sorted_leq: sorted_leq_steps (h2, steps)
H_no_inf_arrivals: no_inf_arrivals (h2, steps)
t: duration
p: (Datatypes_nat__canonical__eqtype_Equality * nat)%type
l: seq
  (Datatypes_nat__canonical__eqtype_Equality * nat)
LST: [seq x <- steps | x.1 == t + 1] = p :: l
LT: (last (0, 0) [seq step <- steps | step.1 <= t]).2 <
(last (0, 0)
   ([seq x <- steps | x.1 <= t + 1 & x.1 <= t] ++
    p :: l)).2
p \in [seq x <- steps | x.1 == t + 1] ->
exists v : nat, (t + 1, v) \in steps
          move=> {LT} {LST}; move: p => //= [t_c v_c].
ac_prefix: ArrivalCurvePrefix
h2: duration
steps: seq (duration * nat)
H_sorted_leq: sorted_leq_steps (h2, steps)
H_no_inf_arrivals: no_inf_arrivals (h2, steps)
t: duration
l: seq
  (Datatypes_nat__canonical__eqtype_Equality * nat)
t_c, v_c: nat
(t_c, v_c) \in [seq x <- steps | x.1 == t + 1] ->
exists v : nat, (t + 1, v) \in steps
          by rewrite mem_filter => //= /andP [/eqP ->].
        }
      }
    }
ac_prefix: ArrivalCurvePrefix
h2: duration
steps: seq (duration * nat)
H_sorted_leq: sorted_leq_steps (h2, steps)
H_no_inf_arrivals: no_inf_arrivals (h2, steps)
t: duration
sorted (fun x y : nat * nat => x.1 <= y.1) steps
    {
ac_prefix: ArrivalCurvePrefix
h2: duration
steps: seq (duration * nat)
H_sorted_leq: sorted_leq_steps (h2, steps)
H_no_inf_arrivals: no_inf_arrivals (h2, steps)
t: duration
sorted (fun x y : nat * nat => x.1 <= y.1) steps move: (H_sorted_leq); clear H_sorted_leq; rewrite /sorted_leq_steps //= => SORT; clear H_no_inf_arrivals.
ac_prefix: ArrivalCurvePrefix
h2: duration
steps: seq (duration * nat)
t: duration
SORT: sorted leq_steps steps
sorted (fun x y : nat * nat => x.1 <= y.1) steps
      elim: steps SORT => [//|a steps IHsteps] /= SORT.
ac_prefix: ArrivalCurvePrefix
h2, t: duration
a: (duration * nat)%type
steps: seq (duration * nat)
IHsteps: sorted leq_steps steps ->
sorted (fun x y : nat * nat => x.1 <= y.1)
  steps
SORT: path leq_steps a steps
path (fun x y : nat * nat => x.1 <= y.1) a steps
      move: SORT; rewrite path_sortedE; auto using leq_steps_is_transitive; move => /andP [LE SORT].
ac_prefix: ArrivalCurvePrefix
h2, t: duration
a: (duration * nat)%type
steps: seq (duration * nat)
IHsteps: sorted leq_steps steps ->
sorted (fun x y : nat * nat => x.1 <= y.1)
  steps
LE: all (leq_steps a) steps
SORT: sorted leq_steps steps
path (fun x y : nat * nat => x.1 <= y.1) a steps
      apply IHsteps in SORT.
ac_prefix: ArrivalCurvePrefix
h2, t: duration
a: (duration * nat)%type
steps: seq (duration * nat)
IHsteps: sorted leq_steps steps ->
sorted (fun x y : nat * nat => x.1 <= y.1)
  steps
LE: all (leq_steps a) steps
SORT: sorted (fun x y : nat * nat => x.1 <= y.1)
  steps
path (fun x y : nat * nat => x.1 <= y.1) a steps
      rewrite path_sortedE; last by intros ? ? ? LE1 LE2; lia.
ac_prefix: ArrivalCurvePrefix
h2, t: duration
a: (duration * nat)%type
steps: seq (duration * nat)
IHsteps: sorted leq_steps steps ->
sorted (fun x y : nat * nat => x.1 <= y.1)
  steps
LE: all (leq_steps a) steps
SORT: sorted (fun x y : nat * nat => x.1 <= y.1)
  steps
all (fun y : nat * nat => a.1 <= y.1) steps &&
sorted (fun x y : nat * nat => x.1 <= y.1) steps
      apply/andP; split=> [|//].
ac_prefix: ArrivalCurvePrefix
h2, t: duration
a: (duration * nat)%type
steps: seq (duration * nat)
IHsteps: sorted leq_steps steps ->
sorted (fun x y : nat * nat => x.1 <= y.1)
  steps
LE: all (leq_steps a) steps
SORT: sorted (fun x y : nat * nat => x.1 <= y.1)
  steps
all (fun y : nat * nat => a.1 <= y.1) steps
      apply/allP; intros [x y] IN.
ac_prefix: ArrivalCurvePrefix
h2, t: duration
a: (duration * nat)%type
steps: seq (duration * nat)
IHsteps: sorted leq_steps steps ->
sorted (fun x y : nat * nat => x.1 <= y.1)
  steps
LE: all (leq_steps a) steps
SORT: sorted (fun x y : nat * nat => x.1 <= y.1)
  steps
x, y: Datatypes_nat__canonical__eqtype_Equality
IN: (x, y) \in steps
a.1 <= (x, y).1
      by move: LE => /allP LE; specialize (LE _ IN); move: LE => /andP [LT _].
    }
  Qed.

End ArrivalCurvePrefixSortedLeq.

(* In the next section, we make the stronger assumption that
   arrival-curve prefixes are sorted according to the [ltn_steps]
   relation. *)
Section ArrivalCurvePrefixSortedLtn.

  (** Consider an arbitrary [ltn]-sorted arrival-curve prefix without
      infinite arrivals. *)
  Variable ac_prefix : ArrivalCurvePrefix.
  Hypothesis H_sorted_ltn : sorted_ltn_steps ac_prefix. (* Stronger assumption. *)
  Hypothesis H_no_inf_arrivals : no_inf_arrivals ac_prefix.

  (** First, we show that an [ltn]-sorted arrival-curve prefix is an
      [leq]-sorted arrival-curve prefix. *)
  Lemma sorted_ltn_steps_imply_sorted_leq_steps_steps :
    sorted_leq_steps ac_prefix.
ac_prefix: ArrivalCurvePrefix
H_sorted_ltn: sorted_ltn_steps ac_prefix
H_no_inf_arrivals: no_inf_arrivals ac_prefix
sorted_leq_steps ac_prefix
  Proof.
ac_prefix: ArrivalCurvePrefix
H_sorted_ltn: sorted_ltn_steps ac_prefix
H_no_inf_arrivals: no_inf_arrivals ac_prefix
sorted_leq_steps ac_prefix
    destruct ac_prefix as [d l]; unfold sorted_leq_steps, sorted_ltn_steps in *; simpl in *.
ac_prefix: ArrivalCurvePrefix
d: duration
l: seq (duration * nat)
H_sorted_ltn: sorted ltn_steps l
H_no_inf_arrivals: no_inf_arrivals (d, l)
sorted leq_steps l
    clear H_no_inf_arrivals d.
ac_prefix: ArrivalCurvePrefix
l: seq (duration * nat)
H_sorted_ltn: sorted ltn_steps l
sorted leq_steps l
    destruct l => [//|]; simpl in *.
ac_prefix: ArrivalCurvePrefix
p: (duration * nat)%type
l: seq (duration * nat)
H_sorted_ltn: path ltn_steps p l
path leq_steps p l
    eapply sub_path; last by apply H_sorted_ltn.
ac_prefix: ArrivalCurvePrefix
p: (duration * nat)%type
l: seq (duration * nat)
H_sorted_ltn: path ltn_steps p l
subrel (T:=nat * nat) ltn_steps leq_steps
    intros [a1 b1] [a2 b2] LT.
ac_prefix: ArrivalCurvePrefix
p: (duration * nat)%type
l: seq (duration * nat)
H_sorted_ltn: path ltn_steps p l
a1, b1, a2, b2: nat
LT: ltn_steps (a1, b1) (a2, b2)
leq_steps (a1, b1) (a2, b2)
    by unfold ltn_steps, leq_steps in *; simpl in *; lia.
  Qed.

  (** Next, we show that [step_at 0] is equal to [(0, 0)]. *)
  Lemma step_at_0_is_00 :
    step_at ac_prefix 0 = (0, 0).
ac_prefix: ArrivalCurvePrefix
H_sorted_ltn: sorted_ltn_steps ac_prefix
H_no_inf_arrivals: no_inf_arrivals ac_prefix
step_at ac_prefix 0 = (0, 0)
  Proof.
ac_prefix: ArrivalCurvePrefix
H_sorted_ltn: sorted_ltn_steps ac_prefix
H_no_inf_arrivals: no_inf_arrivals ac_prefix
step_at ac_prefix 0 = (0, 0)
    unfold step_at; destruct ac_prefix as [h [ | [t v] steps]] => [//|].
ac_prefix: ArrivalCurvePrefix
h, t: duration
v: nat
steps: seq (duration * nat)
H_sorted_ltn: sorted_ltn_steps (h, (t, v) :: steps)
H_no_inf_arrivals: no_inf_arrivals
  (h, (t, v) :: steps)
last (0, 0)
  [seq step <- steps_of (h, (t, v) :: steps)
     | step.1 <= 0] = (0, 0)
    have TR := ltn_steps_is_transitive.
ac_prefix: ArrivalCurvePrefix
h, t: duration
v: nat
steps: seq (duration * nat)
H_sorted_ltn: sorted_ltn_steps (h, (t, v) :: steps)
H_no_inf_arrivals: no_inf_arrivals
  (h, (t, v) :: steps)
TR: transitive (T:=nat * nat) ltn_steps
last (0, 0)
  [seq step <- steps_of (h, (t, v) :: steps)
     | step.1 <= 0] = (0, 0)
    move: (H_sorted_ltn); clear H_sorted_ltn; rewrite /sorted_ltn_steps //= path_sortedE // => /andP [ALL LT].
ac_prefix: ArrivalCurvePrefix
h, t: duration
v: nat
steps: seq (duration * nat)
H_no_inf_arrivals: no_inf_arrivals
  (h, (t, v) :: steps)
TR: transitive (T:=nat * nat) ltn_steps
ALL: all (ltn_steps (t, v)) steps
LT: sorted ltn_steps steps
last (0, 0)
  (if t <= 0
   then (t, v) :: [seq step <- steps | step.1 <= 0]
   else [seq step <- steps | step.1 <= 0]) = (0, 0)
    have EM : [seq step <- steps | fst step <= 0] = [::].
ac_prefix: ArrivalCurvePrefix
h, t: duration
v: nat
steps: seq (duration * nat)
H_no_inf_arrivals: no_inf_arrivals
  (h, (t, v) :: steps)
TR: transitive (T:=nat * nat) ltn_steps
ALL: all (ltn_steps (t, v)) steps
LT: sorted ltn_steps steps
[seq step <- steps | step.1 <= 0] = [::]
ac_prefix: ArrivalCurvePrefix
h, t: duration
v: nat
steps: seq (duration * nat)
H_no_inf_arrivals: no_inf_arrivals
  (h, (t, v) :: steps)
TR: transitive (T:=nat * nat) ltn_steps
ALL: all (ltn_steps (t, v)) steps
LT: sorted ltn_steps steps
EM: [seq step <- steps | step.1 <= 0] = [::]
last (0, 0)
  (if t <= 0
   then (t, v) :: [seq step <- steps | step.1 <= 0]
   else [seq step <- steps | step.1 <= 0]) = (
0, 0)
    {
ac_prefix: ArrivalCurvePrefix
h, t: duration
v: nat
steps: seq (duration * nat)
H_no_inf_arrivals: no_inf_arrivals
  (h, (t, v) :: steps)
TR: transitive (T:=nat * nat) ltn_steps
ALL: all (ltn_steps (t, v)) steps
LT: sorted ltn_steps steps
[seq step <- steps | step.1 <= 0] = [::] apply filter_in_pred0; intros [t' v'] IN.
ac_prefix: ArrivalCurvePrefix
h, t: duration
v: nat
steps: seq (duration * nat)
H_no_inf_arrivals: no_inf_arrivals
  (h, (t, v) :: steps)
TR: transitive (T:=nat * nat) ltn_steps
ALL: all (ltn_steps (t, v)) steps
LT: sorted ltn_steps steps
t', v': Datatypes_nat__canonical__eqtype_Equality
IN: (t', v') \in steps
~~ ((t', v').1 <= 0)
      move: ALL => /allP ALL; specialize (ALL _ IN); simpl in ALL.
ac_prefix: ArrivalCurvePrefix
h, t: duration
v: nat
steps: seq (duration * nat)
H_no_inf_arrivals: no_inf_arrivals
  (h, (t, v) :: steps)
TR: transitive (T:=nat * nat) ltn_steps
LT: sorted ltn_steps steps
t', v': Datatypes_nat__canonical__eqtype_Equality
IN: (t', v') \in steps
ALL: ltn_steps (t, v) (t', v')
~~ ((t', v').1 <= 0)
      by rewrite -ltnNge //=; move: ALL; rewrite /ltn_steps //= => /andP [T _ ]; lia. }
ac_prefix: ArrivalCurvePrefix
h, t: duration
v: nat
steps: seq (duration * nat)
H_no_inf_arrivals: no_inf_arrivals
  (h, (t, v) :: steps)
TR: transitive (T:=nat * nat) ltn_steps
ALL: all (ltn_steps (t, v)) steps
LT: sorted ltn_steps steps
EM: [seq step <- steps | step.1 <= 0] = [::]
last (0, 0)
  (if t <= 0
   then (t, v) :: [seq step <- steps | step.1 <= 0]
   else [seq step <- steps | step.1 <= 0]) = (0, 0)
    rewrite EM; destruct (posnP t) as [Z | POS].
ac_prefix: ArrivalCurvePrefix
h, t: duration
v: nat
steps: seq (duration * nat)
H_no_inf_arrivals: no_inf_arrivals
  (h, (t, v) :: steps)
TR: transitive (T:=nat * nat) ltn_steps
ALL: all (ltn_steps (t, v)) steps
LT: sorted ltn_steps steps
EM: [seq step <- steps | step.1 <= 0] = [::]
Z: t = 0
last (0, 0) (if t <= 0 then [:: (t, v)] else [::]) =
(0, 0)
ac_prefix: ArrivalCurvePrefix
h, t: duration
v: nat
steps: seq (duration * nat)
H_no_inf_arrivals: no_inf_arrivals
  (h, (t, v) :: steps)
TR: transitive (T:=nat * nat) ltn_steps
ALL: all (ltn_steps (t, v)) steps
LT: sorted ltn_steps steps
EM: [seq step <- steps | step.1 <= 0] = [::]
POS: 0 < t
last (0, 0) (if t <= 0 then [:: (t, v)] else [::]) =
(0, 0)
    {
ac_prefix: ArrivalCurvePrefix
h, t: duration
v: nat
steps: seq (duration * nat)
H_no_inf_arrivals: no_inf_arrivals
  (h, (t, v) :: steps)
TR: transitive (T:=nat * nat) ltn_steps
ALL: all (ltn_steps (t, v)) steps
LT: sorted ltn_steps steps
EM: [seq step <- steps | step.1 <= 0] = [::]
Z: t = 0
last (0, 0) (if t <= 0 then [:: (t, v)] else [::]) =
(0, 0) subst t; simpl.
ac_prefix: ArrivalCurvePrefix
h: duration
v: nat
steps: seq (duration * nat)
H_no_inf_arrivals: no_inf_arrivals
  (h, (0, v) :: steps)
TR: transitive (T:=nat * nat) ltn_steps
ALL: all (ltn_steps (0, v)) steps
LT: sorted ltn_steps steps
EM: [seq step <- steps | step.1 <= 0] = [::]
(0, v) = (0, 0)
      move: H_no_inf_arrivals; rewrite /no_inf_arrivals /value_at /step_at //= EM //=.
ac_prefix: ArrivalCurvePrefix
h: duration
v: nat
steps: seq (duration * nat)
H_no_inf_arrivals: no_inf_arrivals
  (h, (0, v) :: steps)
TR: transitive (T:=nat * nat) ltn_steps
ALL: all (ltn_steps (0, v)) steps
LT: sorted ltn_steps steps
EM: [seq step <- steps | step.1 <= 0] = [::]
v == 0 -> (0, v) = (0, 0)
      by move => /eqP EQ; subst v. }
ac_prefix: ArrivalCurvePrefix
h, t: duration
v: nat
steps: seq (duration * nat)
H_no_inf_arrivals: no_inf_arrivals
  (h, (t, v) :: steps)
TR: transitive (T:=nat * nat) ltn_steps
ALL: all (ltn_steps (t, v)) steps
LT: sorted ltn_steps steps
EM: [seq step <- steps | step.1 <= 0] = [::]
POS: 0 < t
last (0, 0) (if t <= 0 then [:: (t, v)] else [::]) =
(0, 0)
    {
ac_prefix: ArrivalCurvePrefix
h, t: duration
v: nat
steps: seq (duration * nat)
H_no_inf_arrivals: no_inf_arrivals
  (h, (t, v) :: steps)
TR: transitive (T:=nat * nat) ltn_steps
ALL: all (ltn_steps (t, v)) steps
LT: sorted ltn_steps steps
EM: [seq step <- steps | step.1 <= 0] = [::]
POS: 0 < t
last (0, 0) (if t <= 0 then [:: (t, v)] else [::]) =
(0, 0) by rewrite leqNgt POS //=. }
  Qed.

  (** We show that functions [steps_of] and [step_at] are consistent.
      That is, if a pair [(t, v)] is in steps of [ac_prefix], then
      [step_at t] is equal to [(t, v)]. *)
  Lemma step_at_agrees_with_steps_of :
    forall t v, (t, v) \in steps_of ac_prefix -> step_at ac_prefix t = (t, v).
ac_prefix: ArrivalCurvePrefix
H_sorted_ltn: sorted_ltn_steps ac_prefix
H_no_inf_arrivals: no_inf_arrivals ac_prefix
forall t v : Datatypes_nat__canonical__eqtype_Equality,
(t, v) \in steps_of ac_prefix ->
step_at ac_prefix t = (t, v)
  Proof.
ac_prefix: ArrivalCurvePrefix
H_sorted_ltn: sorted_ltn_steps ac_prefix
H_no_inf_arrivals: no_inf_arrivals ac_prefix
forall t v : Datatypes_nat__canonical__eqtype_Equality,
(t, v) \in steps_of ac_prefix ->
step_at ac_prefix t = (t, v)
    case: ac_prefix H_sorted_ltn => [h steps] + //= ? ? IN.
ac_prefix: ArrivalCurvePrefix
H_sorted_ltn: sorted_ltn_steps ac_prefix
H_no_inf_arrivals: no_inf_arrivals ac_prefix
h: duration
steps: seq (duration * nat)
_t_, _v_: nat
IN: (_t_, _v_) \in steps
sorted_ltn_steps (h, steps) ->
step_at (h, steps) _t_ = (_t_, _v_)
    move: IN => /in_cat //= [steps__l [steps__r ->]] /sorted_cat //=; case => //= [|_ +]; first by apply ltn_steps_is_transitive.
ac_prefix: ArrivalCurvePrefix
H_sorted_ltn: sorted_ltn_steps ac_prefix
H_no_inf_arrivals: no_inf_arrivals ac_prefix
h: duration
steps: seq (duration * nat)
_t_, _v_: nat
steps__l, steps__r: seq (nat * nat)
path ltn_steps (_t_, _v_) steps__r ->
step_at (h, steps__l ++ (_t_, _v_) :: steps__r) _t_ =
(_t_, _v_)
    rewrite /step_at filter_cat last_cat (nonnil_last _ _ (0,0)); last by rewrite //= leqnn.
ac_prefix: ArrivalCurvePrefix
H_sorted_ltn: sorted_ltn_steps ac_prefix
H_no_inf_arrivals: no_inf_arrivals ac_prefix
h: duration
steps: seq (duration * nat)
_t_, _v_: nat
steps__l, steps__r: seq (nat * nat)
path ltn_steps (_t_, _v_) steps__r ->
last (0, 0)
  [seq step <- (_t_, _v_) :: steps__r | step.1 <= _t_] =
(_t_, _v_)
    rewrite //= path_sortedE; auto using ltn_steps_is_transitive; rewrite //= leqnn => /andP [ALL SORT].
ac_prefix: ArrivalCurvePrefix
H_sorted_ltn: sorted_ltn_steps ac_prefix
H_no_inf_arrivals: no_inf_arrivals ac_prefix
h: duration
steps: seq (duration * nat)
_t_, _v_: nat
steps__l, steps__r: seq (nat * nat)
ALL: all (ltn_steps (_t_, _v_)) steps__r
SORT: sorted ltn_steps steps__r
last (0, 0)
  ((_t_, _v_)
   :: [seq step <- steps__r | step.1 <= _t_]) =
(_t_, _v_)
    replace (filter _ _ ) with (@nil (nat * nat)) => [//|].
ac_prefix: ArrivalCurvePrefix
H_sorted_ltn: sorted_ltn_steps ac_prefix
H_no_inf_arrivals: no_inf_arrivals ac_prefix
h: duration
steps: seq (duration * nat)
_t_, _v_: nat
steps__l, steps__r: seq (nat * nat)
ALL: all (ltn_steps (_t_, _v_)) steps__r
SORT: sorted ltn_steps steps__r
[::] = [seq step <- steps__r | step.1 <= _t_]
    rewrite filter_in_pred0 // => x IN; rewrite -ltnNge.
ac_prefix: ArrivalCurvePrefix
H_sorted_ltn: sorted_ltn_steps ac_prefix
H_no_inf_arrivals: no_inf_arrivals ac_prefix
h: duration
steps: seq (duration * nat)
_t_, _v_: nat
steps__l, steps__r: seq (nat * nat)
ALL: all (ltn_steps (_t_, _v_)) steps__r
SORT: sorted ltn_steps steps__r
x: Datatypes_prod__canonical__eqtype_Equality
  Datatypes_nat__canonical__eqtype_Equality
  Datatypes_nat__canonical__eqtype_Equality
IN: x \in steps__r
_t_ < x.1
    by move: ALL => /allP ALL; move: (ALL _ IN); rewrite /ltn_steps //= => /andP [LT _ ].
  Qed.

End ArrivalCurvePrefixSortedLtn.

(** In this section, we prove a few basic properties of
    [extrapolated_arrival_curve] function, such as (1) monotonicity of
    [extrapolated_arrival_curve] or (2) implications of the fact that
    [extrapolated_arrival_curve] makes a step at time [t + ε]. *)
Section ExtrapolatedArrivalCurve.

  (** Consider an arbitrary [leq]-sorted arrival-curve prefix without infinite arrivals. *)
  Variable ac_prefix : ArrivalCurvePrefix.
  Hypothesis H_positive : positive_horizon ac_prefix.
  Hypothesis H_sorted_leq : sorted_leq_steps ac_prefix.

  (** Let [h] denote the horizon of [ac_prefix] ... *)
  Let h := horizon_of ac_prefix.

  (** ... and [prefix] be shorthand for [value_at ac_prefix]. *)
  Let prefix := value_at ac_prefix.

  (** We show that [extrapolated_arrival_curve] is monotone. *)
  Lemma extrapolated_arrival_curve_is_monotone :
    monotone leq (extrapolated_arrival_curve ac_prefix).
ac_prefix: ArrivalCurvePrefix
H_positive: positive_horizon ac_prefix
H_sorted_leq: sorted_leq_steps ac_prefix
h:= horizon_of ac_prefix: duration
prefix:= value_at ac_prefix: duration -> nat
monotone leq (extrapolated_arrival_curve ac_prefix)
  Proof.
ac_prefix: ArrivalCurvePrefix
H_positive: positive_horizon ac_prefix
H_sorted_leq: sorted_leq_steps ac_prefix
h:= horizon_of ac_prefix: duration
prefix:= value_at ac_prefix: duration -> nat
monotone leq (extrapolated_arrival_curve ac_prefix)
    intros t1 t2 LE; unfold extrapolated_arrival_curve.
ac_prefix: ArrivalCurvePrefix
H_positive: positive_horizon ac_prefix
H_sorted_leq: sorted_leq_steps ac_prefix
h:= horizon_of ac_prefix: duration
prefix:= value_at ac_prefix: duration -> nat
t1, t2: nat
LE: t1 <= t2
t1 %/ horizon_of ac_prefix *
value_at ac_prefix (horizon_of ac_prefix) +
value_at ac_prefix (t1 %% horizon_of ac_prefix) <=
t2 %/ horizon_of ac_prefix *
value_at ac_prefix (horizon_of ac_prefix) +
value_at ac_prefix (t2 %% horizon_of ac_prefix)
    replace (horizon_of _) with h => [|//].
ac_prefix: ArrivalCurvePrefix
H_positive: positive_horizon ac_prefix
H_sorted_leq: sorted_leq_steps ac_prefix
h:= horizon_of ac_prefix: duration
prefix:= value_at ac_prefix: duration -> nat
t1, t2: nat
LE: t1 <= t2
t1 %/ h * value_at ac_prefix h +
value_at ac_prefix (t1 %% h) <=
t2 %/ h * value_at ac_prefix h +
value_at ac_prefix (t2 %% h)
    move: LE; rewrite leq_eqVlt => /orP [/eqP EQ | LTs].
ac_prefix: ArrivalCurvePrefix
H_positive: positive_horizon ac_prefix
H_sorted_leq: sorted_leq_steps ac_prefix
h:= horizon_of ac_prefix: duration
prefix:= value_at ac_prefix: duration -> nat
t1, t2: nat
EQ: t1 = t2
t1 %/ h * value_at ac_prefix h +
value_at ac_prefix (t1 %% h) <=
t2 %/ h * value_at ac_prefix h +
value_at ac_prefix (t2 %% h)
ac_prefix: ArrivalCurvePrefix
H_positive: positive_horizon ac_prefix
H_sorted_leq: sorted_leq_steps ac_prefix
h:= horizon_of ac_prefix: duration
prefix:= value_at ac_prefix: duration -> nat
t1, t2: nat
LTs: t1 < t2
t1 %/ h * value_at ac_prefix h +
value_at ac_prefix (t1 %% h) <=
t2 %/ h * value_at ac_prefix h +
value_at ac_prefix (t2 %% h)
    {
ac_prefix: ArrivalCurvePrefix
H_positive: positive_horizon ac_prefix
H_sorted_leq: sorted_leq_steps ac_prefix
h:= horizon_of ac_prefix: duration
prefix:= value_at ac_prefix: duration -> nat
t1, t2: nat
EQ: t1 = t2
t1 %/ h * value_at ac_prefix h +
value_at ac_prefix (t1 %% h) <=
t2 %/ h * value_at ac_prefix h +
value_at ac_prefix (t2 %% h) by subst t2. }
ac_prefix: ArrivalCurvePrefix
H_positive: positive_horizon ac_prefix
H_sorted_leq: sorted_leq_steps ac_prefix
h:= horizon_of ac_prefix: duration
prefix:= value_at ac_prefix: duration -> nat
t1, t2: nat
LTs: t1 < t2
t1 %/ h * value_at ac_prefix h +
value_at ac_prefix (t1 %% h) <=
t2 %/ h * value_at ac_prefix h +
value_at ac_prefix (t2 %% h)
    {
ac_prefix: ArrivalCurvePrefix
H_positive: positive_horizon ac_prefix
H_sorted_leq: sorted_leq_steps ac_prefix
h:= horizon_of ac_prefix: duration
prefix:= value_at ac_prefix: duration -> nat
t1, t2: nat
LTs: t1 < t2
t1 %/ h * value_at ac_prefix h +
value_at ac_prefix (t1 %% h) <=
t2 %/ h * value_at ac_prefix h +
value_at ac_prefix (t2 %% h) have ALT : (t1 %/ h == t2 %/ h) \/ (t1 %/ h < t2 %/ h).
ac_prefix: ArrivalCurvePrefix
H_positive: positive_horizon ac_prefix
H_sorted_leq: sorted_leq_steps ac_prefix
h:= horizon_of ac_prefix: duration
prefix:= value_at ac_prefix: duration -> nat
t1, t2: nat
LTs: t1 < t2
t1 %/ h == t2 %/ h \/ t1 %/ h < t2 %/ h
ac_prefix: ArrivalCurvePrefix
H_positive: positive_horizon ac_prefix
H_sorted_leq: sorted_leq_steps ac_prefix
h:= horizon_of ac_prefix: duration
prefix:= value_at ac_prefix: duration -> nat
t1, t2: nat
LTs: t1 < t2
ALT: t1 %/ h == t2 %/ h \/ t1 %/ h < t2 %/ h
t1 %/ h * value_at ac_prefix h +
value_at ac_prefix (t1 %% h) <=
t2 %/ h * value_at ac_prefix h +
value_at ac_prefix (t2 %% h)
      {
ac_prefix: ArrivalCurvePrefix
H_positive: positive_horizon ac_prefix
H_sorted_leq: sorted_leq_steps ac_prefix
h:= horizon_of ac_prefix: duration
prefix:= value_at ac_prefix: duration -> nat
t1, t2: nat
LTs: t1 < t2
t1 %/ h == t2 %/ h \/ t1 %/ h < t2 %/ h by apply/orP; rewrite -leq_eqVlt; apply leq_div2r, ltnW. }
ac_prefix: ArrivalCurvePrefix
H_positive: positive_horizon ac_prefix
H_sorted_leq: sorted_leq_steps ac_prefix
h:= horizon_of ac_prefix: duration
prefix:= value_at ac_prefix: duration -> nat
t1, t2: nat
LTs: t1 < t2
ALT: t1 %/ h == t2 %/ h \/ t1 %/ h < t2 %/ h
t1 %/ h * value_at ac_prefix h +
value_at ac_prefix (t1 %% h) <=
t2 %/ h * value_at ac_prefix h +
value_at ac_prefix (t2 %% h)
      move: ALT => [/eqP EQ | LT].
ac_prefix: ArrivalCurvePrefix
H_positive: positive_horizon ac_prefix
H_sorted_leq: sorted_leq_steps ac_prefix
h:= horizon_of ac_prefix: duration
prefix:= value_at ac_prefix: duration -> nat
t1, t2: nat
LTs: t1 < t2
EQ: t1 %/ h = t2 %/ h
t1 %/ h * value_at ac_prefix h +
value_at ac_prefix (t1 %% h) <=
t2 %/ h * value_at ac_prefix h +
value_at ac_prefix (t2 %% h)
ac_prefix: ArrivalCurvePrefix
H_positive: positive_horizon ac_prefix
H_sorted_leq: sorted_leq_steps ac_prefix
h:= horizon_of ac_prefix: duration
prefix:= value_at ac_prefix: duration -> nat
t1, t2: nat
LTs: t1 < t2
LT: t1 %/ h < t2 %/ h
t1 %/ h * value_at ac_prefix h +
value_at ac_prefix (t1 %% h) <=
t2 %/ h * value_at ac_prefix h +
value_at ac_prefix (t2 %% h)
      {
ac_prefix: ArrivalCurvePrefix
H_positive: positive_horizon ac_prefix
H_sorted_leq: sorted_leq_steps ac_prefix
h:= horizon_of ac_prefix: duration
prefix:= value_at ac_prefix: duration -> nat
t1, t2: nat
LTs: t1 < t2
EQ: t1 %/ h = t2 %/ h
t1 %/ h * value_at ac_prefix h +
value_at ac_prefix (t1 %% h) <=
t2 %/ h * value_at ac_prefix h +
value_at ac_prefix (t2 %% h) rewrite EQ leq_add2l; apply value_at_monotone => //.
ac_prefix: ArrivalCurvePrefix
H_positive: positive_horizon ac_prefix
H_sorted_leq: sorted_leq_steps ac_prefix
h:= horizon_of ac_prefix: duration
prefix:= value_at ac_prefix: duration -> nat
t1, t2: nat
LTs: t1 < t2
EQ: t1 %/ h = t2 %/ h
t1 %% h <= t2 %% h
        by apply eqdivn_leqmodn; lia.
      }
ac_prefix: ArrivalCurvePrefix
H_positive: positive_horizon ac_prefix
H_sorted_leq: sorted_leq_steps ac_prefix
h:= horizon_of ac_prefix: duration
prefix:= value_at ac_prefix: duration -> nat
t1, t2: nat
LTs: t1 < t2
LT: t1 %/ h < t2 %/ h
t1 %/ h * value_at ac_prefix h +
value_at ac_prefix (t1 %% h) <=
t2 %/ h * value_at ac_prefix h +
value_at ac_prefix (t2 %% h)
      {
ac_prefix: ArrivalCurvePrefix
H_positive: positive_horizon ac_prefix
H_sorted_leq: sorted_leq_steps ac_prefix
h:= horizon_of ac_prefix: duration
prefix:= value_at ac_prefix: duration -> nat
t1, t2: nat
LTs: t1 < t2
LT: t1 %/ h < t2 %/ h
t1 %/ h * value_at ac_prefix h +
value_at ac_prefix (t1 %% h) <=
t2 %/ h * value_at ac_prefix h +
value_at ac_prefix (t2 %% h) have EQ: exists k, t1 + k = t2 /\ k > 0.
ac_prefix: ArrivalCurvePrefix
H_positive: positive_horizon ac_prefix
H_sorted_leq: sorted_leq_steps ac_prefix
h:= horizon_of ac_prefix: duration
prefix:= value_at ac_prefix: duration -> nat
t1, t2: nat
LTs: t1 < t2
LT: t1 %/ h < t2 %/ h
exists k : nat, t1 + k = t2 /\ 0 < k
ac_prefix: ArrivalCurvePrefix
H_positive: positive_horizon ac_prefix
H_sorted_leq: sorted_leq_steps ac_prefix
h:= horizon_of ac_prefix: duration
prefix:= value_at ac_prefix: duration -> nat
t1, t2: nat
LTs: t1 < t2
LT: t1 %/ h < t2 %/ h
EQ: exists k : nat, t1 + k = t2 /\ 0 < k
t1 %/ h * value_at ac_prefix h +
value_at ac_prefix (t1 %% h) <=
t2 %/ h * value_at ac_prefix h +
value_at ac_prefix (t2 %% h)
        {
ac_prefix: ArrivalCurvePrefix
H_positive: positive_horizon ac_prefix
H_sorted_leq: sorted_leq_steps ac_prefix
h:= horizon_of ac_prefix: duration
prefix:= value_at ac_prefix: duration -> nat
t1, t2: nat
LTs: t1 < t2
LT: t1 %/ h < t2 %/ h
exists k : nat, t1 + k = t2 /\ 0 < k exists (t2 - t1); split; lia. }
ac_prefix: ArrivalCurvePrefix
H_positive: positive_horizon ac_prefix
H_sorted_leq: sorted_leq_steps ac_prefix
h:= horizon_of ac_prefix: duration
prefix:= value_at ac_prefix: duration -> nat
t1, t2: nat
LTs: t1 < t2
LT: t1 %/ h < t2 %/ h
EQ: exists k : nat, t1 + k = t2 /\ 0 < k
t1 %/ h * value_at ac_prefix h +
value_at ac_prefix (t1 %% h) <=
t2 %/ h * value_at ac_prefix h +
value_at ac_prefix (t2 %% h)
        destruct EQ as [k [EQ POS]]; subst t2; clear LTs.
ac_prefix: ArrivalCurvePrefix
H_positive: positive_horizon ac_prefix
H_sorted_leq: sorted_leq_steps ac_prefix
h:= horizon_of ac_prefix: duration
prefix:= value_at ac_prefix: duration -> nat
t1, k: nat
LT: t1 %/ h < (t1 + k) %/ h
POS: 0 < k
t1 %/ h * value_at ac_prefix h +
value_at ac_prefix (t1 %% h) <=
(t1 + k) %/ h * value_at ac_prefix h +
value_at ac_prefix ((t1 + k) %% h)
        rewrite divnD//.
ac_prefix: ArrivalCurvePrefix
H_positive: positive_horizon ac_prefix
H_sorted_leq: sorted_leq_steps ac_prefix
h:= horizon_of ac_prefix: duration
prefix:= value_at ac_prefix: duration -> nat
t1, k: nat
LT: t1 %/ h < (t1 + k) %/ h
POS: 0 < k
t1 %/ h * value_at ac_prefix h +
value_at ac_prefix (t1 %% h) <=
(t1 %/ h + k %/ h + (h <= t1 %% h + k %% h)) *
value_at ac_prefix h +
value_at ac_prefix ((t1 + k) %% h)
        rewrite !mulnDl -!addnA leq_add2l.
ac_prefix: ArrivalCurvePrefix
H_positive: positive_horizon ac_prefix
H_sorted_leq: sorted_leq_steps ac_prefix
h:= horizon_of ac_prefix: duration
prefix:= value_at ac_prefix: duration -> nat
t1, k: nat
LT: t1 %/ h < (t1 + k) %/ h
POS: 0 < k
value_at ac_prefix (t1 %% h) <=
k %/ h * value_at ac_prefix h +
((h <= t1 %% h + k %% h) * value_at ac_prefix h +
 value_at ac_prefix ((t1 + k) %% h))
        destruct (leqP h k) as [LEk|LTk].
ac_prefix: ArrivalCurvePrefix
H_positive: positive_horizon ac_prefix
H_sorted_leq: sorted_leq_steps ac_prefix
h:= horizon_of ac_prefix: duration
prefix:= value_at ac_prefix: duration -> nat
t1, k: nat
LT: t1 %/ h < (t1 + k) %/ h
POS: 0 < k
LEk: h <= k
value_at ac_prefix (t1 %% h) <=
k %/ h * value_at ac_prefix h +
((h <= t1 %% h + k %% h) * value_at ac_prefix h +
 value_at ac_prefix ((t1 + k) %% h))
ac_prefix: ArrivalCurvePrefix
H_positive: positive_horizon ac_prefix
H_sorted_leq: sorted_leq_steps ac_prefix
h:= horizon_of ac_prefix: duration
prefix:= value_at ac_prefix: duration -> nat
t1, k: nat
LT: t1 %/ h < (t1 + k) %/ h
POS: 0 < k
LTk: k < h
value_at ac_prefix (t1 %% h) <=
k %/ h * value_at ac_prefix h +
((h <= t1 %% h + k %% h) * value_at ac_prefix h +
 value_at ac_prefix ((t1 + k) %% h))
        {
ac_prefix: ArrivalCurvePrefix
H_positive: positive_horizon ac_prefix
H_sorted_leq: sorted_leq_steps ac_prefix
h:= horizon_of ac_prefix: duration
prefix:= value_at ac_prefix: duration -> nat
t1, k: nat
LT: t1 %/ h < (t1 + k) %/ h
POS: 0 < k
LEk: h <= k
value_at ac_prefix (t1 %% h) <=
k %/ h * value_at ac_prefix h +
((h <= t1 %% h + k %% h) * value_at ac_prefix h +
 value_at ac_prefix ((t1 + k) %% h)) eapply leq_trans; last by apply leq_addr.
ac_prefix: ArrivalCurvePrefix
H_positive: positive_horizon ac_prefix
H_sorted_leq: sorted_leq_steps ac_prefix
h:= horizon_of ac_prefix: duration
prefix:= value_at ac_prefix: duration -> nat
t1, k: nat
LT: t1 %/ h < (t1 + k) %/ h
POS: 0 < k
LEk: h <= k
value_at ac_prefix (t1 %% h) <=
k %/ h * value_at ac_prefix h
          move: LEk; rewrite leq_eqVlt => /orP [/eqP EQk | LTk].
ac_prefix: ArrivalCurvePrefix
H_positive: positive_horizon ac_prefix
H_sorted_leq: sorted_leq_steps ac_prefix
h:= horizon_of ac_prefix: duration
prefix:= value_at ac_prefix: duration -> nat
t1, k: nat
LT: t1 %/ h < (t1 + k) %/ h
POS: 0 < k
EQk: h = k
value_at ac_prefix (t1 %% h) <=
k %/ h * value_at ac_prefix h
ac_prefix: ArrivalCurvePrefix
H_positive: positive_horizon ac_prefix
H_sorted_leq: sorted_leq_steps ac_prefix
h:= horizon_of ac_prefix: duration
prefix:= value_at ac_prefix: duration -> nat
t1, k: nat
LT: t1 %/ h < (t1 + k) %/ h
POS: 0 < k
LTk: h < k
value_at ac_prefix (t1 %% h) <=
k %/ h * value_at ac_prefix h
          {
ac_prefix: ArrivalCurvePrefix
H_positive: positive_horizon ac_prefix
H_sorted_leq: sorted_leq_steps ac_prefix
h:= horizon_of ac_prefix: duration
prefix:= value_at ac_prefix: duration -> nat
t1, k: nat
LT: t1 %/ h < (t1 + k) %/ h
POS: 0 < k
EQk: h = k
value_at ac_prefix (t1 %% h) <=
k %/ h * value_at ac_prefix h by subst; rewrite divnn POS mul1n; apply value_at_monotone, ltnW, ltn_pmod. }
ac_prefix: ArrivalCurvePrefix
H_positive: positive_horizon ac_prefix
H_sorted_leq: sorted_leq_steps ac_prefix
h:= horizon_of ac_prefix: duration
prefix:= value_at ac_prefix: duration -> nat
t1, k: nat
LT: t1 %/ h < (t1 + k) %/ h
POS: 0 < k
LTk: h < k
value_at ac_prefix (t1 %% h) <=
k %/ h * value_at ac_prefix h
          {
ac_prefix: ArrivalCurvePrefix
H_positive: positive_horizon ac_prefix
H_sorted_leq: sorted_leq_steps ac_prefix
h:= horizon_of ac_prefix: duration
prefix:= value_at ac_prefix: duration -> nat
t1, k: nat
LT: t1 %/ h < (t1 + k) %/ h
POS: 0 < k
LTk: h < k
value_at ac_prefix (t1 %% h) <=
k %/ h * value_at ac_prefix h rewrite -[value_at _ (t1 %% h)]mul1n; apply leq_mul.
ac_prefix: ArrivalCurvePrefix
H_positive: positive_horizon ac_prefix
H_sorted_leq: sorted_leq_steps ac_prefix
h:= horizon_of ac_prefix: duration
prefix:= value_at ac_prefix: duration -> nat
t1, k: nat
LT: t1 %/ h < (t1 + k) %/ h
POS: 0 < k
LTk: h < k
0 < k %/ h
ac_prefix: ArrivalCurvePrefix
H_positive: positive_horizon ac_prefix
H_sorted_leq: sorted_leq_steps ac_prefix
h:= horizon_of ac_prefix: duration
prefix:= value_at ac_prefix: duration -> nat
t1, k: nat
LT: t1 %/ h < (t1 + k) %/ h
POS: 0 < k
LTk: h < k
value_at ac_prefix (t1 %% h) <= value_at ac_prefix h
            -
ac_prefix: ArrivalCurvePrefix
H_positive: positive_horizon ac_prefix
H_sorted_leq: sorted_leq_steps ac_prefix
h:= horizon_of ac_prefix: duration
prefix:= value_at ac_prefix: duration -> nat
t1, k: nat
LT: t1 %/ h < (t1 + k) %/ h
POS: 0 < k
LTk: h < k
0 < k %/ h by rewrite divn_gt0; [apply: ltnW|].
            -
ac_prefix: ArrivalCurvePrefix
H_positive: positive_horizon ac_prefix
H_sorted_leq: sorted_leq_steps ac_prefix
h:= horizon_of ac_prefix: duration
prefix:= value_at ac_prefix: duration -> nat
t1, k: nat
LT: t1 %/ h < (t1 + k) %/ h
POS: 0 < k
LTk: h < k
value_at ac_prefix (t1 %% h) <= value_at ac_prefix h by apply value_at_monotone, ltnW, ltn_pmod.
          }
        }
ac_prefix: ArrivalCurvePrefix
H_positive: positive_horizon ac_prefix
H_sorted_leq: sorted_leq_steps ac_prefix
h:= horizon_of ac_prefix: duration
prefix:= value_at ac_prefix: duration -> nat
t1, k: nat
LT: t1 %/ h < (t1 + k) %/ h
POS: 0 < k
LTk: k < h
value_at ac_prefix (t1 %% h) <=
k %/ h * value_at ac_prefix h +
((h <= t1 %% h + k %% h) * value_at ac_prefix h +
 value_at ac_prefix ((t1 + k) %% h))
        {
ac_prefix: ArrivalCurvePrefix
H_positive: positive_horizon ac_prefix
H_sorted_leq: sorted_leq_steps ac_prefix
h:= horizon_of ac_prefix: duration
prefix:= value_at ac_prefix: duration -> nat
t1, k: nat
LT: t1 %/ h < (t1 + k) %/ h
POS: 0 < k
LTk: k < h
value_at ac_prefix (t1 %% h) <=
k %/ h * value_at ac_prefix h +
((h <= t1 %% h + k %% h) * value_at ac_prefix h +
 value_at ac_prefix ((t1 + k) %% h)) rewrite divn_small // mul0n add0n.
ac_prefix: ArrivalCurvePrefix
H_positive: positive_horizon ac_prefix
H_sorted_leq: sorted_leq_steps ac_prefix
h:= horizon_of ac_prefix: duration
prefix:= value_at ac_prefix: duration -> nat
t1, k: nat
LT: t1 %/ h < (t1 + k) %/ h
POS: 0 < k
LTk: k < h
value_at ac_prefix (t1 %% h) <=
(h <= t1 %% h + k %% h) * value_at ac_prefix h +
value_at ac_prefix ((t1 + k) %% h)
          rewrite divnD // in LT; move: LT; rewrite -addnA -addn1 leq_add2l divn_small // add0n.
ac_prefix: ArrivalCurvePrefix
H_positive: positive_horizon ac_prefix
H_sorted_leq: sorted_leq_steps ac_prefix
h:= horizon_of ac_prefix: duration
prefix:= value_at ac_prefix: duration -> nat
t1, k: nat
POS: 0 < k
LTk: k < h
0 < (h <= t1 %% h + k %% h) ->
value_at ac_prefix (t1 %% h) <=
(h <= t1 %% h + k %% h) * value_at ac_prefix h +
value_at ac_prefix ((t1 + k) %% h)
          rewrite lt0b => F; rewrite F; clear F.
ac_prefix: ArrivalCurvePrefix
H_positive: positive_horizon ac_prefix
H_sorted_leq: sorted_leq_steps ac_prefix
h:= horizon_of ac_prefix: duration
prefix:= value_at ac_prefix: duration -> nat
t1, k: nat
POS: 0 < k
LTk: k < h
value_at ac_prefix (t1 %% h) <=
true * value_at ac_prefix h +
value_at ac_prefix ((t1 + k) %% h)
          rewrite mul1n; eapply leq_trans; last by apply leq_addr.
ac_prefix: ArrivalCurvePrefix
H_positive: positive_horizon ac_prefix
H_sorted_leq: sorted_leq_steps ac_prefix
h:= horizon_of ac_prefix: duration
prefix:= value_at ac_prefix: duration -> nat
t1, k: nat
POS: 0 < k
LTk: k < h
value_at ac_prefix (t1 %% h) <= value_at ac_prefix h
          by apply value_at_monotone, ltnW, ltn_pmod.
        }
      }
    }
  Qed.

  (** Finally, we show that if
      [extrapolated_arrival_curve t <> extrapolated_arrival_curve (t + ε)],
      then either (1) [t + ε] divides [h] or (2) [prefix (t mod h) < prefix ((t + ε) mod h)]. *)
  Lemma extrapolated_arrival_curve_change :
    forall t,
      extrapolated_arrival_curve ac_prefix t != extrapolated_arrival_curve ac_prefix (t + ε) ->
      (* 1 *) t %/ h < (t + ε) %/ h
      \/ (* 2 *) t %/ h = (t + ε) %/ h /\ prefix (t %% h) < prefix ((t + ε) %% h).
ac_prefix: ArrivalCurvePrefix
H_positive: positive_horizon ac_prefix
H_sorted_leq: sorted_leq_steps ac_prefix
h:= horizon_of ac_prefix: duration
prefix:= value_at ac_prefix: duration -> nat
forall t : duration,
extrapolated_arrival_curve ac_prefix t
!= extrapolated_arrival_curve ac_prefix (t + 1) ->
t %/ h < (t + 1) %/ h \/
t %/ h = (t + 1) %/ h /\
prefix (t %% h) < prefix ((t + 1) %% h)
  Proof.
ac_prefix: ArrivalCurvePrefix
H_positive: positive_horizon ac_prefix
H_sorted_leq: sorted_leq_steps ac_prefix
h:= horizon_of ac_prefix: duration
prefix:= value_at ac_prefix: duration -> nat
forall t : duration,
extrapolated_arrival_curve ac_prefix t
!= extrapolated_arrival_curve ac_prefix (t + 1) ->
t %/ h < (t + 1) %/ h \/
t %/ h = (t + 1) %/ h /\
prefix (t %% h) < prefix ((t + 1) %% h)
    intros t NEQ.
ac_prefix: ArrivalCurvePrefix
H_positive: positive_horizon ac_prefix
H_sorted_leq: sorted_leq_steps ac_prefix
h:= horizon_of ac_prefix: duration
prefix:= value_at ac_prefix: duration -> nat
t: duration
NEQ: extrapolated_arrival_curve ac_prefix t
!= extrapolated_arrival_curve ac_prefix (t + 1)
t %/ h < (t + 1) %/ h \/
t %/ h = (t + 1) %/ h /\
prefix (t %% h) < prefix ((t + 1) %% h)
    have LT := ltn_neqAle (extrapolated_arrival_curve ac_prefix t) (extrapolated_arrival_curve ac_prefix (t + ε)).
ac_prefix: ArrivalCurvePrefix
H_positive: positive_horizon ac_prefix
H_sorted_leq: sorted_leq_steps ac_prefix
h:= horizon_of ac_prefix: duration
prefix:= value_at ac_prefix: duration -> nat
t: duration
NEQ: extrapolated_arrival_curve ac_prefix t
!= extrapolated_arrival_curve ac_prefix (t + 1)
LT: (extrapolated_arrival_curve ac_prefix t <
 extrapolated_arrival_curve ac_prefix (t + 1)) =
(extrapolated_arrival_curve ac_prefix t
 != extrapolated_arrival_curve ac_prefix (t + 1)) &&
(extrapolated_arrival_curve ac_prefix t <=
 extrapolated_arrival_curve ac_prefix (t + 1))
t %/ h < (t + 1) %/ h \/
t %/ h = (t + 1) %/ h /\
prefix (t %% h) < prefix ((t + 1) %% h)
    rewrite NEQ in LT; rewrite extrapolated_arrival_curve_is_monotone in LT; last by apply leq_addr.
ac_prefix: ArrivalCurvePrefix
H_positive: positive_horizon ac_prefix
H_sorted_leq: sorted_leq_steps ac_prefix
h:= horizon_of ac_prefix: duration
prefix:= value_at ac_prefix: duration -> nat
t: duration
NEQ: extrapolated_arrival_curve ac_prefix t
!= extrapolated_arrival_curve ac_prefix (t + 1)
LT: (extrapolated_arrival_curve ac_prefix t <
 extrapolated_arrival_curve ac_prefix (t + 1)) =
true && true
t %/ h < (t + 1) %/ h \/
t %/ h = (t + 1) %/ h /\
prefix (t %% h) < prefix ((t + 1) %% h)
    clear NEQ; simpl in LT.
ac_prefix: ArrivalCurvePrefix
H_positive: positive_horizon ac_prefix
H_sorted_leq: sorted_leq_steps ac_prefix
h:= horizon_of ac_prefix: duration
prefix:= value_at ac_prefix: duration -> nat
t: duration
LT: (extrapolated_arrival_curve ac_prefix t <
 extrapolated_arrival_curve ac_prefix (t + 1)) =
true
t %/ h < (t + 1) %/ h \/
t %/ h = (t + 1) %/ h /\
prefix (t %% h) < prefix ((t + 1) %% h)
    unfold extrapolated_arrival_curve in LT.
ac_prefix: ArrivalCurvePrefix
H_positive: positive_horizon ac_prefix
H_sorted_leq: sorted_leq_steps ac_prefix
h:= horizon_of ac_prefix: duration
prefix:= value_at ac_prefix: duration -> nat
t: duration
LT: (t %/ horizon_of ac_prefix *
 value_at ac_prefix (horizon_of ac_prefix) +
 value_at ac_prefix (t %% horizon_of ac_prefix) <
 (t + 1) %/ horizon_of ac_prefix *
 value_at ac_prefix (horizon_of ac_prefix) +
 value_at ac_prefix
   ((t + 1) %% horizon_of ac_prefix)) = true
t %/ h < (t + 1) %/ h \/
t %/ h = (t + 1) %/ h /\
prefix (t %% h) < prefix ((t + 1) %% h)
    replace (horizon_of _) with h in LT => [|//].
ac_prefix: ArrivalCurvePrefix
H_positive: positive_horizon ac_prefix
H_sorted_leq: sorted_leq_steps ac_prefix
h:= horizon_of ac_prefix: duration
prefix:= value_at ac_prefix: duration -> nat
t: duration
LT: (t %/ h * value_at ac_prefix h +
 value_at ac_prefix (t %% h) <
 (t + 1) %/ h * value_at ac_prefix h +
 value_at ac_prefix ((t + 1) %% h)) = true
t %/ h < (t + 1) %/ h \/
t %/ h = (t + 1) %/ h /\
prefix (t %% h) < prefix ((t + 1) %% h)
    have AF : forall s1 s2 m x y,
        s1 <= s2 ->
        m * s1 + x < m * s2 + y ->
        s1 < s2 \/ s1 = s2 /\ x < y.
ac_prefix: ArrivalCurvePrefix
H_positive: positive_horizon ac_prefix
H_sorted_leq: sorted_leq_steps ac_prefix
h:= horizon_of ac_prefix: duration
prefix:= value_at ac_prefix: duration -> nat
t: duration
LT: (t %/ h * value_at ac_prefix h +
 value_at ac_prefix (t %% h) <
 (t + 1) %/ h * value_at ac_prefix h +
 value_at ac_prefix ((t + 1) %% h)) = true
forall s1 s2 m x y : nat,
s1 <= s2 ->
m * s1 + x < m * s2 + y -> s1 < s2 \/ s1 = s2 /\ x < y
ac_prefix: ArrivalCurvePrefix
H_positive: positive_horizon ac_prefix
H_sorted_leq: sorted_leq_steps ac_prefix
h:= horizon_of ac_prefix: duration
prefix:= value_at ac_prefix: duration -> nat
t: duration
LT: (t %/ h * value_at ac_prefix h +
 value_at ac_prefix (t %% h) <
 (t + 1) %/ h * value_at ac_prefix h +
 value_at ac_prefix ((t + 1) %% h)) = true
AF: forall s1 s2 m x y : nat,
s1 <= s2 ->
m * s1 + x < m * s2 + y ->
s1 < s2 \/ s1 = s2 /\ x < y
t %/ h < (t + 1) %/ h \/
t %/ h = (t + 1) %/ h /\
prefix (t %% h) < prefix ((t + 1) %% h)
    {
ac_prefix: ArrivalCurvePrefix
H_positive: positive_horizon ac_prefix
H_sorted_leq: sorted_leq_steps ac_prefix
h:= horizon_of ac_prefix: duration
prefix:= value_at ac_prefix: duration -> nat
t: duration
LT: (t %/ h * value_at ac_prefix h +
 value_at ac_prefix (t %% h) <
 (t + 1) %/ h * value_at ac_prefix h +
 value_at ac_prefix ((t + 1) %% h)) = true
forall s1 s2 m x y : nat,
s1 <= s2 ->
m * s1 + x < m * s2 + y -> s1 < s2 \/ s1 = s2 /\ x < y  clear; intros s1 s2 m x y LEs LT.
s1, s2, m, x, y: nat
LEs: s1 <= s2
LT: m * s1 + x < m * s2 + y
s1 < s2 \/ s1 = s2 /\ x < y
       move: LEs; rewrite leq_eqVlt => /orP [/eqP EQ | LTs].
s1, s2, m, x, y: nat
LT: m * s1 + x < m * s2 + y
EQ: s1 = s2
s1 < s2 \/ s1 = s2 /\ x < y
s1, s2, m, x, y: nat
LT: m * s1 + x < m * s2 + y
LTs: s1 < s2
s1 < s2 \/ s1 = s2 /\ x < y
       {
s1, s2, m, x, y: nat
LT: m * s1 + x < m * s2 + y
EQ: s1 = s2
s1 < s2 \/ s1 = s2 /\ x < y by subst s2; rename s1 into s; right; split; [|lia]. }
s1, s2, m, x, y: nat
LT: m * s1 + x < m * s2 + y
LTs: s1 < s2
s1 < s2 \/ s1 = s2 /\ x < y
       {
s1, s2, m, x, y: nat
LT: m * s1 + x < m * s2 + y
LTs: s1 < s2
s1 < s2 \/ s1 = s2 /\ x < y by left. }
    }
ac_prefix: ArrivalCurvePrefix
H_positive: positive_horizon ac_prefix
H_sorted_leq: sorted_leq_steps ac_prefix
h:= horizon_of ac_prefix: duration
prefix:= value_at ac_prefix: duration -> nat
t: duration
LT: (t %/ h * value_at ac_prefix h +
 value_at ac_prefix (t %% h) <
 (t + 1) %/ h * value_at ac_prefix h +
 value_at ac_prefix ((t + 1) %% h)) = true
AF: forall s1 s2 m x y : nat,
s1 <= s2 ->
m * s1 + x < m * s2 + y ->
s1 < s2 \/ s1 = s2 /\ x < y
t %/ h < (t + 1) %/ h \/
t %/ h = (t + 1) %/ h /\
prefix (t %% h) < prefix ((t + 1) %% h)
    apply AF with (m := prefix h).
ac_prefix: ArrivalCurvePrefix
H_positive: positive_horizon ac_prefix
H_sorted_leq: sorted_leq_steps ac_prefix
h:= horizon_of ac_prefix: duration
prefix:= value_at ac_prefix: duration -> nat
t: duration
LT: (t %/ h * value_at ac_prefix h +
 value_at ac_prefix (t %% h) <
 (t + 1) %/ h * value_at ac_prefix h +
 value_at ac_prefix ((t + 1) %% h)) = true
AF: forall s1 s2 m x y : nat,
s1 <= s2 ->
m * s1 + x < m * s2 + y ->
s1 < s2 \/ s1 = s2 /\ x < y
t %/ h <= (t + 1) %/ h
ac_prefix: ArrivalCurvePrefix
H_positive: positive_horizon ac_prefix
H_sorted_leq: sorted_leq_steps ac_prefix
h:= horizon_of ac_prefix: duration
prefix:= value_at ac_prefix: duration -> nat
t: duration
LT: (t %/ h * value_at ac_prefix h +
 value_at ac_prefix (t %% h) <
 (t + 1) %/ h * value_at ac_prefix h +
 value_at ac_prefix ((t + 1) %% h)) = true
AF: forall s1 s2 m x y : nat,
s1 <= s2 ->
m * s1 + x < m * s2 + y ->
s1 < s2 \/ s1 = s2 /\ x < y
prefix h * (t %/ h) + prefix (t %% h) <
prefix h * ((t + 1) %/ h) + prefix ((t + 1) %% h)
    {
ac_prefix: ArrivalCurvePrefix
H_positive: positive_horizon ac_prefix
H_sorted_leq: sorted_leq_steps ac_prefix
h:= horizon_of ac_prefix: duration
prefix:= value_at ac_prefix: duration -> nat
t: duration
LT: (t %/ h * value_at ac_prefix h +
 value_at ac_prefix (t %% h) <
 (t + 1) %/ h * value_at ac_prefix h +
 value_at ac_prefix ((t + 1) %% h)) = true
AF: forall s1 s2 m x y : nat,
s1 <= s2 ->
m * s1 + x < m * s2 + y ->
s1 < s2 \/ s1 = s2 /\ x < y
t %/ h <= (t + 1) %/ h by apply leq_div2r, leq_addr. }
ac_prefix: ArrivalCurvePrefix
H_positive: positive_horizon ac_prefix
H_sorted_leq: sorted_leq_steps ac_prefix
h:= horizon_of ac_prefix: duration
prefix:= value_at ac_prefix: duration -> nat
t: duration
LT: (t %/ h * value_at ac_prefix h +
 value_at ac_prefix (t %% h) <
 (t + 1) %/ h * value_at ac_prefix h +
 value_at ac_prefix ((t + 1) %% h)) = true
AF: forall s1 s2 m x y : nat,
s1 <= s2 ->
m * s1 + x < m * s2 + y ->
s1 < s2 \/ s1 = s2 /\ x < y
prefix h * (t %/ h) + prefix (t %% h) <
prefix h * ((t + 1) %/ h) + prefix ((t + 1) %% h)
    {
ac_prefix: ArrivalCurvePrefix
H_positive: positive_horizon ac_prefix
H_sorted_leq: sorted_leq_steps ac_prefix
h:= horizon_of ac_prefix: duration
prefix:= value_at ac_prefix: duration -> nat
t: duration
LT: (t %/ h * value_at ac_prefix h +
 value_at ac_prefix (t %% h) <
 (t + 1) %/ h * value_at ac_prefix h +
 value_at ac_prefix ((t + 1) %% h)) = true
AF: forall s1 s2 m x y : nat,
s1 <= s2 ->
m * s1 + x < m * s2 + y ->
s1 < s2 \/ s1 = s2 /\ x < y
prefix h * (t %/ h) + prefix (t %% h) <
prefix h * ((t + 1) %/ h) + prefix ((t + 1) %% h) by rewrite ![prefix _ * _]mulnC; apply LT. }
  Qed.

End ExtrapolatedArrivalCurve.