Built with Alectryon, running Coq+SerAPI v8.15.0+0.15.0. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use instead of Ctrl.
Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "_ + _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ - _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ <= _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ < _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ >= _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ > _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ <= _ <= _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ < _ <= _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ <= _ < _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ < _ < _" was already used in scope nat_scope. [notation-overridden,parsing]
Notation "_ * _" was already used in scope nat_scope. [notation-overridden,parsing]
Require Export prosa.behavior.time.
Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ : _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ & _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ | _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
Notation "[ rel _ _ in _ ]" was already used in scope fun_scope. [notation-overridden,parsing]
(** 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. *)

transitive (T:=nat * nat) ltn_steps

transitive (T:=nat * nat) ltn_steps
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... *)

reflexive (T:=nat * nat) leq_steps

reflexive (T:=nat * nat) leq_steps
l, r: nat

leq_steps (l, r) (l, r)
l, r: nat

((l, r).1 <= (l, r).1) && ((l, r).2 <= (l, r).2)
by apply /andP; split. Qed. (** ... and transitive. *)

transitive (T:=nat * nat) leq_steps

transitive (T:=nat * nat) leq_steps
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 [<=]. *)
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)
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)
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
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
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
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
ac_prefix: ArrivalCurvePrefix
h, t__c: duration
v__c: nat
steps: seq (duration * nat)
H_sorted_leq: sorted leq_steps (h, (t__c, v__c) :: steps).2
t1, t2: nat
LE: t1 <= t2
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

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
ac_prefix: ArrivalCurvePrefix
h, t__c: duration
v__c: nat
steps: seq (duration * nat)
H_sorted_leq: sorted leq_steps (h, (t__c, v__c) :: steps).2
t1, t2: nat
LE: t1 <= t2
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
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 : prod_eqType nat_eqType nat_eqType, leq_steps (t__d1, v__d1) x}
LTN2: leq_steps (t__d2, v__d2) (t__c, v__c)
ALL2: {in steps, forall x : prod_eqType nat_eqType nat_eqType, 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
ac_prefix: ArrivalCurvePrefix
h, t__c: duration
v__c: nat
steps: seq (duration * nat)
H_sorted_leq: sorted leq_steps (h, (t__c, v__c) :: steps).2
t1, t2: nat
LE: t1 <= t2
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
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 : prod_eqType nat_eqType nat_eqType, leq_steps (t__d1, v__d1) x}
LTN2: leq_steps (t__d2, v__d2) (t__c, v__c)
ALL2: {in steps, forall x : prod_eqType nat_eqType nat_eqType, leq_steps (t__d2, v__d2) x}

all predT ((t__c, v__c) :: steps)
ac_prefix: ArrivalCurvePrefix
h, t__c: duration
v__c: nat
steps: seq (duration * nat)
H_sorted_leq: sorted leq_steps (h, (t__c, v__c) :: steps).2
t1, t2: nat
LE: t1 <= t2
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
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 : prod_eqType nat_eqType nat_eqType, leq_steps (t__d1, v__d1) x}
LTN2: leq_steps (t__d2, v__d2) (t__c, v__c)
ALL2: {in steps, forall x : prod_eqType nat_eqType nat_eqType, leq_steps (t__d2, v__d2) x}
{in predT & &, transitive (T:=nat * nat) leq_steps}
ac_prefix: ArrivalCurvePrefix
h, t__c: duration
v__c: nat
steps: seq (duration * nat)
H_sorted_leq: sorted leq_steps (h, (t__c, v__c) :: steps).2
t1, t2: nat
LE: t1 <= t2
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
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 : prod_eqType nat_eqType nat_eqType, leq_steps (t__d1, v__d1) x}
LTN2: leq_steps (t__d2, v__d2) (t__c, v__c)
ALL2: {in steps, forall x : prod_eqType nat_eqType nat_eqType, 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, t__c: duration
v__c: nat
steps: seq (duration * nat)
H_sorted_leq: sorted leq_steps (h, (t__c, v__c) :: steps).2
t1, t2: nat
LE: t1 <= t2
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
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 : prod_eqType nat_eqType nat_eqType, leq_steps (t__d1, v__d1) x}
LTN2: leq_steps (t__d2, v__d2) (t__c, v__c)
ALL2: {in steps, forall x : prod_eqType nat_eqType nat_eqType, leq_steps (t__d2, v__d2) x}

all predT ((t__c, v__c) :: steps)
by apply/allP.
ac_prefix: ArrivalCurvePrefix
h, t__c: duration
v__c: nat
steps: seq (duration * nat)
H_sorted_leq: sorted leq_steps (h, (t__c, v__c) :: steps).2
t1, t2: nat
LE: t1 <= t2
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
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 : prod_eqType nat_eqType nat_eqType, leq_steps (t__d1, v__d1) x}
LTN2: leq_steps (t__d2, v__d2) (t__c, v__c)
ALL2: {in steps, forall x : prod_eqType nat_eqType nat_eqType, leq_steps (t__d2, v__d2) x}

{in predT & &, transitive (T:=nat * nat) leq_steps}
ac_prefix: ArrivalCurvePrefix
h, t__c: duration
v__c: nat
steps: seq (duration * nat)
H_sorted_leq: sorted leq_steps (h, (t__c, v__c) :: steps).2
t1, t2: nat
LE: t1 <= t2
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
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 : prod_eqType nat_eqType nat_eqType, leq_steps (t__d1, v__d1) x}
LTN2: leq_steps (t__d2, v__d2) (t__c, v__c)
ALL2: {in steps, forall x : prod_eqType nat_eqType nat_eqType, 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, t__c: duration
v__c: nat
steps: seq (duration * nat)
H_sorted_leq: sorted leq_steps (h, (t__c, v__c) :: steps).2
t1, t2: nat
LE: t1 <= t2
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
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 : prod_eqType nat_eqType nat_eqType, leq_steps (t__d1, v__d1) x}
LTN2: leq_steps (t__d2, v__d2) (t__c, v__c)
ALL2: {in steps, forall x : prod_eqType nat_eqType nat_eqType, 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, t__c: duration
v__c: nat
steps: seq (duration * nat)
H_sorted_leq: sorted leq_steps (h, (t__c, v__c) :: steps).2
t1, t2: nat
LE: t1 <= t2
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
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 : prod_eqType nat_eqType nat_eqType, leq_steps (t__d1, v__d1) x}
LTN2: leq_steps (t__d2, v__d2) (t__c, v__c)
ALL2: {in steps, forall x : prod_eqType nat_eqType nat_eqType, 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, t__c: duration
v__c: nat
steps: seq (duration * nat)
H_sorted_leq: sorted leq_steps (h, (t__c, v__c) :: steps).2
t1, t2: nat
LE: t1 <= t2
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
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 : prod_eqType nat_eqType nat_eqType, leq_steps (t__d1, v__d1) x}
LTN2: leq_steps (t__d2, v__d2) (t__c, v__c)
ALL2: {in steps, forall x : prod_eqType nat_eqType nat_eqType, 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
ac_prefix: ArrivalCurvePrefix
h, t__c: duration
v__c: nat
steps: seq (duration * nat)
H_sorted_leq: path leq_steps (t__c, v__c) steps
t1, t2: nat
LE: t1 <= t2
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
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, t__c: duration
v__c: nat
steps: seq (duration * nat)
H_sorted_leq: path leq_steps (t__c, v__c) steps
t1, t2: nat
LE: t1 <= t2
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
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, t__c: duration
v__c: nat
steps: seq (duration * nat)
H_sorted_leq: path leq_steps (t__c, v__c) steps
t1, t2: nat
LE: t1 <= t2
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
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, t__c: duration
v__c: nat
steps: seq (duration * nat)
H_sorted_leq: path leq_steps (t__c, v__c) steps
t1, t2: nat
LE: t1 <= t2
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
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, t__c: duration
v__c: nat
steps: seq (duration * nat)
H_sorted_leq: path leq_steps (t__c, v__c) steps
t1, t2: nat
LE: t1 <= t2
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
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
rewrite R1 R2 //=; apply IHsteps; try done.
ac_prefix: ArrivalCurvePrefix
h, t__c: duration
v__c: nat
steps: seq (duration * nat)
H_sorted_leq: path leq_steps (t__c, v__c) steps
t1, t2: nat
LE: t1 <= t2
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
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, t__c: duration
v__c: nat
steps: seq (duration * nat)
H_sorted_leq: path leq_steps (t__c, v__c) steps
t1, t2: nat
LE: t1 <= t2
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
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, t__c: duration
v__c: nat
steps: seq (duration * nat)
H_sorted_leq: path leq_steps (t__c, v__c) steps
t1, t2: nat
LE: t1 <= t2
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
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, t__c: duration
v__c: nat
steps: seq (duration * nat)
H_sorted_leq: path leq_steps (t__c, v__c) steps
t1, t2: nat
LE: t1 <= t2
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
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
by lia.
ac_prefix: ArrivalCurvePrefix
h, t__c: duration
v__c: nat
steps: seq (duration * nat)
H_sorted_leq: path leq_steps (t__c, v__c) steps
t1, t2: nat
LE: t1 <= t2
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
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, t__c: duration
v__c: nat
steps: seq (duration * nat)
H_sorted_leq: path leq_steps (t__c, v__c) steps
t1, t2: nat
LE: t1 <= t2
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
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, t__c: duration
v__c: nat
steps: seq (duration * nat)
H_sorted_leq: path leq_steps (t__c, v__c) steps
t1, t2: nat
LE: t1 <= t2
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
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, t__c: duration
v__c: nat
steps: seq (duration * nat)
H_sorted_leq: path leq_steps (t__c, v__c) steps
t1, t2: nat
LE: t1 <= t2
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
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, t__c: duration
v__c: nat
steps: seq (duration * nat)
H_sorted_leq: path leq_steps (t__c, v__c) steps
t1, t2: nat
LE: t1 <= t2
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
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, t__c: duration
v__c: nat
steps: seq (duration * nat)
H_sorted_leq: path leq_steps (t__c, v__c) steps
t1, t2: nat
LE: t1 <= t2
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
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, t__c: duration
v__c: nat
steps: seq (duration * nat)
H_sorted_leq: path leq_steps (t__c, v__c) steps
t1, t2: nat
LE: t1 <= t2
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
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, t__c: duration
v__c: nat
steps: seq (duration * nat)
H_sorted_leq: path leq_steps (t__c, v__c) steps
t1, t2: nat
LE: t1 <= t2
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
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, t__c: duration
v__c: nat
steps: seq (duration * nat)
H_sorted_leq: path leq_steps (t__c, v__c) steps
t1, t2: nat
LE: t1 <= t2
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
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, t__c: duration
v__c: nat
steps: seq (duration * nat)
H_sorted_leq: path leq_steps (t__c, v__c) steps
t1, t2: nat
LE: t1 <= t2
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
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, t__c: duration
v__c: nat
steps: seq (duration * nat)
H_sorted_leq: path leq_steps (t__c, v__c) steps
t1, t2: nat
LE: t1 <= t2
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
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, t__c: duration
v__c: nat
steps: seq (duration * nat)
H_sorted_leq: path leq_steps (t__c, v__c) steps
t1, t2: nat
LE: t1 <= t2
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
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
ac_prefix: ArrivalCurvePrefix
h, t__c: duration
v__c: nat
steps: seq (duration * nat)
H_sorted_leq: path leq_steps (t__c, v__c) steps
t1, t2: nat
LE: t1 <= t2
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
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
ac_prefix: ArrivalCurvePrefix
h, t__c: duration
v__c: nat
steps: seq (duration * nat)
H_sorted_leq: path leq_steps (t__c, v__c) steps
t1, t2: nat
LE: t1 <= t2
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
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

all (leq_steps (t__d1, v__d1)) steps
ac_prefix: ArrivalCurvePrefix
h, t__c: duration
v__c: nat
steps: seq (duration * nat)
H_sorted_leq: path leq_steps (t__c, v__c) steps
t1, t2: nat
LE: t1 <= t2
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
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
all (leq_steps (t__d2, v__d2)) steps
ac_prefix: ArrivalCurvePrefix
h, t__c: duration
v__c: nat
steps: seq (duration * nat)
H_sorted_leq: path leq_steps (t__c, v__c) steps
t1, t2: nat
LE: t1 <= t2
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
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

all (leq_steps (t__d1, v__d1)) steps
ac_prefix: ArrivalCurvePrefix
h, t__c: duration
v__c: nat
steps: seq (duration * nat)
H_sorted_leq: path leq_steps (t__c, v__c) steps
t1, t2: nat
LE: t1 <= t2
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
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
all (leq_steps (t__d2, v__d2)) steps
ac_prefix: ArrivalCurvePrefix
h, t__c: duration
v__c: nat
steps: seq (duration * nat)
H_sorted_leq: path leq_steps (t__c, v__c) steps
t1, t2: nat
LE: t1 <= t2
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
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

all (leq_steps (t__d2, v__d2)) steps
ac_prefix: ArrivalCurvePrefix
h, t__c: duration
v__c: nat
steps: seq (duration * nat)
H_sorted_leq: path leq_steps (t__c, v__c) steps
t1, t2: nat
LE: t1 <= t2
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
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

all (leq_steps (t__d2, v__d2)) steps
by 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
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

all (leq_steps (0, 0)) steps
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
all (leq_steps (0, 0)) steps
all: by 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]. *)
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 + ε) -> exists v : nat_eqType, (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 + ε) -> exists v : nat_eqType, (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
t: duration
LT: value_at ac_prefix t < value_at ac_prefix (t + ε)

exists v : nat_eqType, (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
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 + ε]).2

exists v : nat_eqType, (t + ε, v) \in steps_of ac_prefix
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 + ε]).2

exists v : nat_eqType, (t + ε, 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 + ε & x.1 <= t] ++ [seq x <- steps | x.1 <= t + ε & t < x.1])).2

exists v : nat_eqType, (t + ε, 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 : prod_eqType nat_eqType nat_eqType => 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 + ε & x.1 <= t] ++ [seq x <- steps | x.1 <= t + ε & t < x.1])).2

exists v : nat_eqType, (t + ε, 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 : prod_eqType nat_eqType nat_eqType => (x.1 <= t + ε) && (t < x.1)) =1 (fun x : nat_eqType * nat_eqType => 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
LT: (last (0, 0) [seq step <- steps | step.1 <= t]).2 < (last (0, 0) ([seq x <- steps | x.1 <= t + ε & x.1 <= t] ++ [seq x <- steps | x.1 == t + ε])).2
exists v : nat_eqType, (t + ε, 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 : prod_eqType nat_eqType nat_eqType => (x.1 <= t + ε) && (t < x.1)) =1 (fun x : nat_eqType * nat_eqType => x.1 == t + ε)
by intros [a b]; simpl; rewrite -addn1 /ε eqn_leq.
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 + ε & x.1 <= t] ++ [seq x <- steps | x.1 == t + ε])).2

exists v : nat_eqType, (t + ε, 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 + ε & x.1 <= t] ++ [seq x <- steps | x.1 == t + ε])).2

exists v : nat_eqType, (t + ε, 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 + ε & x.1 <= t] ++ [seq x <- steps | x.1 == t + ε])).2
LST: [seq x <- steps | x.1 == t + ε] = [::]

exists v : nat_eqType, (t + ε, 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 + ε & x.1 <= t] ++ [seq x <- steps | x.1 == t + ε])).2
p: (nat_eqType * nat)%type
l: seq (nat_eqType * nat)
LST: [seq x <- steps | x.1 == t + ε] = p :: l
exists v : nat_eqType, (t + ε, 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 + ε & x.1 <= t] ++ [seq x <- steps | x.1 == t + ε])).2
LST: [seq x <- steps | x.1 == t + ε] = [::]

exists v : nat_eqType, (t + ε, 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
LST: [seq x <- steps | x.1 == t + ε] = [::]
LT: (last (0, 0) [seq step <- steps | step.1 <= t]).2 < (last (0, 0) ([seq x <- steps | x.1 <= t + ε & x.1 <= t] ++ [::])).2

exists v : nat_eqType, (t + ε, 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
LST: [seq x <- steps | x.1 == t + ε] = [::]

(fun x : prod_eqType nat_eqType nat_eqType => (x.1 <= t + ε) && (x.1 <= t)) =1 (fun x : nat * nat_eqType => 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 + ε] = [::]
LT: (last (0, 0) [seq step <- steps | step.1 <= t]).2 < (last (0, 0) ([seq x <- steps | x.1 <= t] ++ [::])).2
exists v : nat_eqType, (t + ε, 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
LST: [seq x <- steps | x.1 == t + ε] = [::]

(fun x : prod_eqType nat_eqType nat_eqType => (x.1 <= t + ε) && (x.1 <= t)) =1 (fun x : nat * nat_eqType => x.1 <= t)
t: duration
a: nat
b: nat_eqType

(a <= t + ε) && (a <= t) = (a <= t)
t: duration
a: nat
b: nat_eqType
i: a <= t

(a <= t + ε) && true = true
t: duration
a: nat
b: nat_eqType
i: t < a
(a <= t + ε) && false = false
t: duration
a: nat
b: nat_eqType
i: a <= t

(a <= t + ε) && true = true
t: duration
a: nat
b: nat_eqType
i: t < a
(a <= t + ε) && false = false
t: duration
a: nat
b: nat_eqType
i: t < a

(a <= t + ε) && false = false
t: duration
a: nat
b: nat_eqType
i: t < a

(a <= t + ε) && 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 + ε] = [::]
LT: (last (0, 0) [seq step <- steps | step.1 <= t]).2 < (last (0, 0) ([seq x <- steps | x.1 <= t] ++ [::])).2

exists v : nat_eqType, (t + ε, 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
LST: [seq x <- steps | x.1 == t + ε] = [::]
LT: (last (0, 0) [seq step <- steps | step.1 <= t]).2 < (last (0, 0) ([seq x <- steps | x.1 <= t] ++ [::])).2

exists v : nat_eqType, (t + ε, v) \in steps_of (h2, 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
LT: (last (0, 0) [seq step <- steps | step.1 <= t]).2 < (last (0, 0) ([seq x <- steps | x.1 <= t + ε & x.1 <= t] ++ [seq x <- steps | x.1 == t + ε])).2
p: (nat_eqType * nat)%type
l: seq (nat_eqType * nat)
LST: [seq x <- steps | x.1 == t + ε] = p :: l

exists v : nat_eqType, (t + ε, 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 + ε & x.1 <= t] ++ [seq x <- steps | x.1 == t + ε])).2
p: (nat_eqType * nat)%type
l: seq (nat_eqType * nat)
LST: [seq x <- steps | x.1 == t + ε] = p :: l

exists v : nat_eqType, (t + ε, 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 + ε & x.1 <= t] ++ [seq x <- steps | x.1 == t + ε])).2
t__c: nat_eqType
v__c: nat
l: seq (nat_eqType * nat)
LST: [seq x <- steps | x.1 == t + ε] = (t__c, v__c) :: l

(t + ε, v__c) \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 + ε & x.1 <= t] ++ [seq x <- steps | x.1 == t + ε])).2
t__c: nat_eqType
v__c: nat
l: seq (nat_eqType * nat)
LST: (t__c, v__c) :: l = [seq x <- steps | x.1 == t + ε]

(t + ε, v__c) \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
LT: (last (0, 0) [seq step <- steps | step.1 <= t]).2 < (last (0, 0) ([seq x <- steps | x.1 <= t + ε & x.1 <= t] ++ [seq x <- steps | x.1 == t + ε])).2
t__c: nat_eqType
v__c: nat
l: seq (nat_eqType * nat)
LST: (t__c, v__c) \in [seq x <- steps | x.1 == t + ε]

(t + ε, v__c) \in steps
by move: LST; rewrite mem_filter //= => /andP [/eqP -> IN]. } }
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 : prod_eqType nat_eqType nat_eqType => 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 : prod_eqType nat_eqType nat_eqType => x.1 <= y.1) steps
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
ac_prefix: ArrivalCurvePrefix
h2: duration
a: (duration * nat)%type
steps: seq (duration * nat)
t: duration
SORT: path leq_steps a steps
IHsteps: sorted leq_steps steps -> sorted (fun x y : nat * nat => x.1 <= y.1) steps

path (fun x y : nat * nat => x.1 <= y.1) a steps
ac_prefix: ArrivalCurvePrefix
h2: duration
a: (duration * nat)%type
steps: seq (duration * nat)
t: duration
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
ac_prefix: ArrivalCurvePrefix
h2: duration
a: (duration * nat)%type
steps: seq (duration * nat)
t: duration
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
ac_prefix: ArrivalCurvePrefix
h2: duration
a: (duration * nat)%type
steps: seq (duration * nat)
t: duration
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
ac_prefix: ArrivalCurvePrefix
h2: duration
a: (duration * nat)%type
steps: seq (duration * nat)
t: duration
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
ac_prefix: ArrivalCurvePrefix
h2: duration
a: (duration * nat)%type
steps: seq (duration * nat)
t: duration
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: nat_eqType
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. *)
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
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
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
ac_prefix: ArrivalCurvePrefix
l: seq (duration * nat)
H_sorted_ltn: sorted ltn_steps l

sorted leq_steps l
ac_prefix: ArrivalCurvePrefix
p: (duration * nat)%type
l: seq (duration * nat)
H_sorted_ltn: path ltn_steps p l

path leq_steps p l
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
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)]. *)
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)
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)
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)
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)
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)
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] = [::]
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': nat_eqType
IN: (t', v') \in steps

~~ ((t', v').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
LT: sorted ltn_steps steps
t', v': nat_eqType
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)
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)
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)
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 => 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)]. *)
ac_prefix: ArrivalCurvePrefix
H_sorted_ltn: sorted_ltn_steps ac_prefix
H_no_inf_arrivals: no_inf_arrivals ac_prefix

forall t v : nat_eqType, (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 : nat_eqType, (t, v) \in steps_of ac_prefix -> step_at ac_prefix t = (t, v)
ac_prefix: ArrivalCurvePrefix
h: duration
steps: seq (duration * nat)
H_sorted_ltn: sorted_ltn_steps (h, steps)
H_no_inf_arrivals: no_inf_arrivals (h, steps)
t, v: nat_eqType
IN: (t, v) \in steps_of (h, steps)

step_at (h, steps) t = (t, v)
ac_prefix: ArrivalCurvePrefix
h: duration
steps: seq (duration * nat)
H_sorted_ltn: sorted_ltn_steps (h, steps)
H_no_inf_arrivals: no_inf_arrivals (h, steps)
t, v: nat
IN: (t, v) \in steps

last (0, 0) [seq step <- steps | step.1 <= t] = (t, v)
ac_prefix: ArrivalCurvePrefix
h: duration
t, v: nat
steps__l, steps__r: seq (prod_eqType nat_eqType nat_eqType)
H_no_inf_arrivals: no_inf_arrivals (h, steps__l ++ [:: (t, v)] ++ steps__r)
H_sorted_ltn: sorted_ltn_steps (h, steps__l ++ [:: (t, v)] ++ steps__r)

last (0, 0) [seq step <- steps__l ++ [:: (t, v)] ++ steps__r | step.1 <= t] = (t, v)
ac_prefix: ArrivalCurvePrefix
h: duration
t, v: nat
steps__l, steps__r: seq (prod_eqType nat_eqType nat_eqType)
H_no_inf_arrivals: no_inf_arrivals (h, steps__l ++ [:: (t, v)] ++ steps__r)
H: sorted ltn_steps steps__l
H0: sorted ltn_steps ([:: (t, v)] ++ steps__r)

last (0, 0) [seq step <- steps__l ++ [:: (t, v)] ++ steps__r | step.1 <= t] = (t, v)
ac_prefix: ArrivalCurvePrefix
h: duration
t, v: nat
steps__l, steps__r: seq (prod_eqType nat_eqType nat_eqType)
H_no_inf_arrivals: no_inf_arrivals (h, steps__l ++ [:: (t, v)] ++ steps__r)
H: sorted ltn_steps steps__l
H0: sorted ltn_steps ([:: (t, v)] ++ steps__r)

last (0, 0) [seq step <- [:: (t, v)] ++ steps__r | step.1 <= t] = (t, v)
ac_prefix: ArrivalCurvePrefix
h: duration
t, v: nat
steps__l, steps__r: seq (prod_eqType nat_eqType nat_eqType)
H_no_inf_arrivals: no_inf_arrivals (h, steps__l ++ [:: (t, v)] ++ steps__r)
H: sorted ltn_steps steps__l
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)
ac_prefix: ArrivalCurvePrefix
h: duration
t, v: nat
steps__l, steps__r: seq (prod_eqType nat_eqType nat_eqType)
H_no_inf_arrivals: no_inf_arrivals (h, steps__l ++ [:: (t, v)] ++ steps__r)
H: sorted ltn_steps steps__l
ALL: all (ltn_steps (t, v)) steps__r
SORT: sorted ltn_steps steps__r

[::] = [seq step <- steps__r | step.1 <= t]
ac_prefix: ArrivalCurvePrefix
h: duration
t, v: nat
steps__l, steps__r: seq (prod_eqType nat_eqType nat_eqType)
H_no_inf_arrivals: no_inf_arrivals (h, steps__l ++ [:: (t, v)] ++ steps__r)
H: sorted ltn_steps steps__l
ALL: all (ltn_steps (t, v)) steps__r
SORT: sorted ltn_steps steps__r
x: prod_eqType nat_eqType nat_eqType
IN: x \in steps__r

t < x.1
by move: ALL => /allP ALL; specialize (ALL _ IN); move: ALL; 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. *)
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)
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)
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)
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)
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)
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)
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)
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)
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)
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)
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)
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))
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))
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
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
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

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))
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)
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)
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)
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)]. *)
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 + ε) -> t %/ h < (t + ε) %/ h \/ 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 + ε) -> t %/ h < (t + ε) %/ h \/ 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
t: duration
NEQ: extrapolated_arrival_curve ac_prefix t != extrapolated_arrival_curve ac_prefix (t + ε)

t %/ h < (t + ε) %/ h \/ 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
t: duration
NEQ: extrapolated_arrival_curve ac_prefix t != extrapolated_arrival_curve ac_prefix (t + ε)
LT: (extrapolated_arrival_curve ac_prefix t < extrapolated_arrival_curve ac_prefix (t + ε)) = (extrapolated_arrival_curve ac_prefix t != extrapolated_arrival_curve ac_prefix (t + ε)) && (extrapolated_arrival_curve ac_prefix t <= extrapolated_arrival_curve ac_prefix (t + ε))

t %/ h < (t + ε) %/ h \/ 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
t: duration
NEQ: extrapolated_arrival_curve ac_prefix t != extrapolated_arrival_curve ac_prefix (t + ε)
LT: (extrapolated_arrival_curve ac_prefix t < extrapolated_arrival_curve ac_prefix (t + ε)) = true && true

t %/ h < (t + ε) %/ h \/ 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
t: duration
LT: (extrapolated_arrival_curve ac_prefix t < extrapolated_arrival_curve ac_prefix (t + ε)) = true

t %/ h < (t + ε) %/ h \/ 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
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 + ε) %/ horizon_of ac_prefix * value_at ac_prefix (horizon_of ac_prefix) + value_at ac_prefix ((t + ε) %% horizon_of ac_prefix)) = true

t %/ h < (t + ε) %/ h \/ 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
t: duration
LT: (t %/ h * value_at ac_prefix h + value_at ac_prefix (t %% h) < (t + ε) %/ h * value_at ac_prefix h + value_at ac_prefix ((t + ε) %% h)) = true

t %/ h < (t + ε) %/ h \/ 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
t: duration
LT: (t %/ h * value_at ac_prefix h + value_at ac_prefix (t %% h) < (t + ε) %/ h * value_at ac_prefix h + value_at ac_prefix ((t + ε) %% 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 + ε) %/ h * value_at ac_prefix h + value_at ac_prefix ((t + ε) %% 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 + ε) %/ h \/ 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
t: duration
LT: (t %/ h * value_at ac_prefix h + value_at ac_prefix (t %% h) < (t + ε) %/ h * value_at ac_prefix h + value_at ac_prefix ((t + ε) %% h)) = true

forall s1 s2 m x y : nat, s1 <= s2 -> m * s1 + x < m * s2 + y -> s1 < s2 \/ s1 = s2 /\ x < y
s1, s2, m, x, y: nat
LEs: s1 <= s2
LT: m * s1 + x < m * s2 + y

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
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; [ done | 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 + ε) %/ h * value_at ac_prefix h + value_at ac_prefix ((t + ε) %% 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 + ε) %/ h \/ 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
t: duration
LT: (t %/ h * value_at ac_prefix h + value_at ac_prefix (t %% h) < (t + ε) %/ h * value_at ac_prefix h + value_at ac_prefix ((t + ε) %% 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 + ε) %/ 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 + ε) %/ h * value_at ac_prefix h + value_at ac_prefix ((t + ε) %% 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 + ε) %/ 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
t: duration
LT: (t %/ h * value_at ac_prefix h + value_at ac_prefix (t %% h) < (t + ε) %/ h * value_at ac_prefix h + value_at ac_prefix ((t + ε) %% 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 + ε) %/ 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 + ε) %/ h * value_at ac_prefix h + value_at ac_prefix ((t + ε) %% 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 + ε) %/ 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
t: duration
LT: (t %/ h * value_at ac_prefix h + value_at ac_prefix (t %% h) < (t + ε) %/ h * value_at ac_prefix h + value_at ac_prefix ((t + ε) %% 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 + ε) %/ h) + prefix ((t + ε) %% h)
by rewrite ![prefix _ * _]mulnC; apply LT. } Qed. End ExtrapolatedArrivalCurve.