Library prosa.analysis.facts.model.ideal_schedule


(* ----------------------------------[ coqtop ]---------------------------------

Welcome to Coq 8.11.2 (June 2020)

----------------------------------------------------------------------------- *)

Require Export prosa.util.all.
Require Export prosa.model.processor.platform_properties.
Require Export prosa.analysis.facts.behavior.service.

Throughout this file, we assume ideal uni-processor schedules.
Require Import prosa.model.processor.ideal.

Note: we do not re-export the basic definitions to avoid littering the global namespace with type class instances.
In this section we establish the classes to which an ideal schedule belongs.
Section ScheduleClass.

  Local Transparent scheduled_in scheduled_on.
Consider any job type and the ideal processor model.
  Context {Job: JobType}.
  Context `{JobArrival Job}.
  Context `{JobCost Job}.

We note that the ideal processor model is indeed a uni-processor model.
  Lemma ideal_proc_model_is_a_uniprocessor_model:
    uniprocessor_model (processor_state Job).

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 630)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  ============================
  uniprocessor_model (processor_state Job)

----------------------------------------------------------------------------- *)

  Proof.
    move⇒ j1 j2 sched t /existsP[[]/eqP E1] /existsP[[]/eqP E2].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 790)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  j1, j2 : Job
  sched : schedule (processor_state Job)
  t : instant
  E1 : sched t = Some j1
  E2 : sched t = Some j2
  ============================
  j1 = j2

----------------------------------------------------------------------------- *)

    by move: E1 E2 =>->[].

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

  Qed.

By definition, [service_in] is the sum of the service on all cores. In the ideal processor model, however, there is only one core, so there is only one term in this sum: the service on the one core.
In the definition of the ideal model, we stated that the type of cores is [unit]. In Coq, this type has only one inhabitant, named [tt].
  Lemma service_in_service_on (j : Job) s :
    service_in j s = service_on j s tt.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 644)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  j : Job
  s : processor_state Job
  ============================
  service_in j s = service_on j s tt

----------------------------------------------------------------------------- *)

  Proof.
    by rewrite /service_in /index_enum Finite.EnumDef.enumDef /= big_seq1.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

  Qed.

  Lemma service_in_def (j : Job) (s : processor_state Job) :
    service_in j s = (s == Some j).

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 655)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  j : Job
  s : processor_state Job
  ============================
  service_in j s = (s == Some j)

----------------------------------------------------------------------------- *)

  Proof.
    by rewrite service_in_service_on.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

  Qed.

We observe that the ideal processor model falls into the category of ideal-progress models, i.e., a scheduled job always receives service.
  Lemma ideal_proc_model_ensures_ideal_progress:
    ideal_progress_proc_model (processor_state Job).

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 658)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  ============================
  ideal_progress_proc_model (processor_state Job)

----------------------------------------------------------------------------- *)

  Proof.
    move⇒ j s /existsP[[]/eqP->] /=.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 743)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  j : Job
  s : processor_state Job
  ============================
  0 < service_in j (Some j)

----------------------------------------------------------------------------- *)

    by rewrite service_in_def /= eqxx /nat_of_bool.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

  Qed.

The ideal processor model is a unit-service model.
  Lemma ideal_proc_model_provides_unit_service:
    unit_service_proc_model (processor_state Job).

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 661)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  ============================
  unit_service_proc_model (processor_state Job)

----------------------------------------------------------------------------- *)

  Proof.
    move⇒ j s.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 664)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  j : Job
  s : processor_state Job
  ============================
  service_in j s <= 1

----------------------------------------------------------------------------- *)

    rewrite service_in_def /= /nat_of_bool.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 670)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  j : Job
  s : processor_state Job
  ============================
  (if s == Some j then 1 else 0) <= 1

----------------------------------------------------------------------------- *)

    by case:ifP.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

  Qed.

  Lemma scheduled_in_def (j : Job) s :
    scheduled_in j s = (s == Some j).

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 675)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  j : Job
  s : option_eqType Job
  ============================
  scheduled_in j s = (s == Some j)

----------------------------------------------------------------------------- *)

  Proof.
    rewrite /scheduled_in/scheduled_on/=.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 690)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  j : Job
  s : option_eqType Job
  ============================
  ~~
  FiniteQuant.quant0b (T:=unit_finType)
    [eta FiniteQuant.ex (T:=unit_finType) (, s == Some j)] = 
  (s == Some j)

----------------------------------------------------------------------------- *)

    case: existsP=>[[_->]//|].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 713)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  j : Job
  s : option_eqType Job
  ============================
  ~ (exists _ : unit_finType, s == Some j) -> false = (s == Some j)

----------------------------------------------------------------------------- *)

    case: (s == Some j)=>//=[[]].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 773)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  j : Job
  s : option_eqType Job
  ============================
  exists _ : unit, true

----------------------------------------------------------------------------- *)

    by ∃.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

  Qed.

  Lemma scheduled_at_def sched (j : Job) t :
    scheduled_at sched j t = (sched t == Some j).

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 691)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  sched : schedule (option_eqType Job)
  j : Job
  t : instant
  ============================
  scheduled_at sched j t = (sched t == Some j)

----------------------------------------------------------------------------- *)

  Proof.
      by rewrite /scheduled_at scheduled_in_def.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

  Qed.

  Lemma service_in_is_scheduled_in (j : Job) s :
    service_in j s = scheduled_in j s.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 705)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  j : Job
  s : processor_state Job
  ============================
  service_in j s = scheduled_in j s

----------------------------------------------------------------------------- *)

  Proof.
    by rewrite service_in_def scheduled_in_def.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

  Qed.

  Lemma service_at_is_scheduled_at sched (j : Job) t :
    service_at sched j t = scheduled_at sched j t.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 721)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  sched : schedule (processor_state Job)
  j : Job
  t : instant
  ============================
  service_at sched j t = scheduled_at sched j t

----------------------------------------------------------------------------- *)

  Proof.
      by rewrite /service_at service_in_is_scheduled_in.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

  Qed.

  Lemma service_on_def (j : Job) (s : processor_state Job) c :
    service_on j s c = (s == Some j).

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 735)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  j : Job
  s : processor_state Job
  c : Core
  ============================
  service_on j s c = (s == Some j)

----------------------------------------------------------------------------- *)

  Proof.
    done.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

  Qed.

  Lemma service_at_def sched (j : Job) t :
    service_at sched j t = (sched t == Some j).

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 751)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  sched : schedule (option_eqType Job)
  j : Job
  t : instant
  ============================
  service_at sched j t = (sched t == Some j)

----------------------------------------------------------------------------- *)

  Proof.
    by rewrite /service_at service_in_def.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

  Qed.

Next we prove a lemma which helps us to do a case analysis on the state of an ideal schedule.
  Lemma ideal_proc_model_sched_case_analysis:
    ∀ (sched : schedule (ideal.processor_state Job)) (t : instant),
      is_idle sched t ∨ ∃ j, scheduled_at sched j t.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 759)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  ============================
  forall (sched : schedule (processor_state Job)) (t : instant),
  is_idle sched t \/ (exists j : Job, scheduled_at sched j t)

----------------------------------------------------------------------------- *)

  Proof.
    intros.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 761)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  sched : schedule (processor_state Job)
  t : instant
  ============================
  is_idle sched t \/ (exists j : Job, scheduled_at sched j t)

----------------------------------------------------------------------------- *)

    unfold is_idle; simpl; destruct (sched t) eqn:EQ.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 778)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  sched : schedule (processor_state Job)
  t : instant
  s : Job
  EQ : sched t = Some s
  ============================
  Some s == None \/ (exists j : Job, scheduled_at sched j t)

subgoal 2 (ID 779) is:
 None == None \/ (exists j : Job, scheduled_at sched j t)

----------------------------------------------------------------------------- *)

    - by right; ∃ s; auto; rewrite scheduled_at_def EQ.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 779)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  sched : schedule (processor_state Job)
  t : instant
  EQ : sched t = None
  ============================
  None == None \/ (exists j : Job, scheduled_at sched j t)

----------------------------------------------------------------------------- *)

    - by left; auto.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

  Qed.

End ScheduleClass.

Incremental Service in Ideal Schedule

In the following section we prove a few facts about service in ideal schedule.
(* Note that these lemmas can be generalized to an arbitrary scheduler. *)
Section IncrementalService.

Consider any job type, ...
  Context {Job : JobType}.
  Context `{JobArrival Job}.
  Context `{JobCost Job}.

... any arrival sequence, ...
  Variable arr_seq : arrival_sequence Job.

... and any ideal uni-processor schedule of this arrival sequence.
  Variable sched : schedule (ideal.processor_state Job).

As a base case, we prove that if a job [j] receives service in some time interval [t1,t2), then there exists a time instant t ∈ [t1,t2) such that [j] is scheduled at time [t] and [t] is the first instant where [j] receives service.
  Lemma positive_service_during:
    ∀ j t1 t2,
      0 < service_during sched j t1 t2 →
      ∃ t : nat, t1 ≤ t < t2 ∧ scheduled_at sched j t ∧ service_during sched j t1 t = 0.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 646)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  ============================
  forall (j : Job) (t1 t2 : instant),
  0 < service_during sched j t1 t2 ->
  exists t : nat,
    t1 <= t < t2 /\ scheduled_at sched j t /\ service_during sched j t1 t = 0

----------------------------------------------------------------------------- *)

  Proof.
    intros j t1 t2 SERV.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 650)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  SERV : 0 < service_during sched j t1 t2
  ============================
  exists t : nat,
    t1 <= t < t2 /\ scheduled_at sched j t /\ service_during sched j t1 t = 0

----------------------------------------------------------------------------- *)

    have LE: t1 ≤ t2.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 651)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  SERV : 0 < service_during sched j t1 t2
  ============================
  t1 <= t2

subgoal 2 (ID 653) is:
 exists t : nat,
   t1 <= t < t2 /\ scheduled_at sched j t /\ service_during sched j t1 t = 0

----------------------------------------------------------------------------- *)

    {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 651)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  SERV : 0 < service_during sched j t1 t2
  ============================
  t1 <= t2

----------------------------------------------------------------------------- *)

rewrite leqNgt; apply/negP; intros CONTR.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 679)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  SERV : 0 < service_during sched j t1 t2
  CONTR : t2 < t1
  ============================
  False

----------------------------------------------------------------------------- *)

        by apply ltnW in CONTR; move: SERV; rewrite /service_during big_geq.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 653)

subgoal 1 (ID 653) is:
 exists t : nat,
   t1 <= t < t2 /\ scheduled_at sched j t /\ service_during sched j t1 t = 0

----------------------------------------------------------------------------- *)

    }

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 653)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  SERV : 0 < service_during sched j t1 t2
  LE : t1 <= t2
  ============================
  exists t : nat,
    t1 <= t < t2 /\ scheduled_at sched j t /\ service_during sched j t1 t = 0

----------------------------------------------------------------------------- *)

    destruct (scheduled_at sched j t1) eqn:SCHED.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 743)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  SERV : 0 < service_during sched j t1 t2
  LE : t1 <= t2
  SCHED : scheduled_at sched j t1 = true
  ============================
  exists t : nat,
    t1 <= t < t2 /\ scheduled_at sched j t /\ service_during sched j t1 t = 0

subgoal 2 (ID 744) is:
 exists t : nat,
   t1 <= t < t2 /\ scheduled_at sched j t /\ service_during sched j t1 t = 0

----------------------------------------------------------------------------- *)

    {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 743)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  SERV : 0 < service_during sched j t1 t2
  LE : t1 <= t2
  SCHED : scheduled_at sched j t1 = true
  ============================
  exists t : nat,
    t1 <= t < t2 /\ scheduled_at sched j t /\ service_during sched j t1 t = 0

----------------------------------------------------------------------------- *)

∃ t1; repeat split; try done.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 748)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  SERV : 0 < service_during sched j t1 t2
  LE : t1 <= t2
  SCHED : scheduled_at sched j t1 = true
  ============================
  t1 <= t1 < t2

subgoal 2 (ID 753) is:
 service_during sched j t1 t1 = 0

----------------------------------------------------------------------------- *)

      - apply/andP; split; first by done.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 826)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  SERV : 0 < service_during sched j t1 t2
  LE : t1 <= t2
  SCHED : scheduled_at sched j t1 = true
  ============================
  t1 < t2

subgoal 2 (ID 753) is:
 service_during sched j t1 t1 = 0

----------------------------------------------------------------------------- *)

        rewrite ltnNge; apply/negP; intros CONTR.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 852)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  SERV : 0 < service_during sched j t1 t2
  LE : t1 <= t2
  SCHED : scheduled_at sched j t1 = true
  CONTR : t2 <= t1
  ============================
  False

subgoal 2 (ID 753) is:
 service_during sched j t1 t1 = 0

----------------------------------------------------------------------------- *)

          by move: SERV; rewrite/service_during big_geq.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 753)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  SERV : 0 < service_during sched j t1 t2
  LE : t1 <= t2
  SCHED : scheduled_at sched j t1 = true
  ============================
  service_during sched j t1 t1 = 0

----------------------------------------------------------------------------- *)

      - by rewrite /service_during big_geq.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 744)

subgoal 1 (ID 744) is:
 exists t : nat,
   t1 <= t < t2 /\ scheduled_at sched j t /\ service_during sched j t1 t = 0

----------------------------------------------------------------------------- *)

    }

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 744)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  SERV : 0 < service_during sched j t1 t2
  LE : t1 <= t2
  SCHED : scheduled_at sched j t1 = false
  ============================
  exists t : nat,
    t1 <= t < t2 /\ scheduled_at sched j t /\ service_during sched j t1 t = 0

----------------------------------------------------------------------------- *)

    {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 744)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  SERV : 0 < service_during sched j t1 t2
  LE : t1 <= t2
  SCHED : scheduled_at sched j t1 = false
  ============================
  exists t : nat,
    t1 <= t < t2 /\ scheduled_at sched j t /\ service_during sched j t1 t = 0

----------------------------------------------------------------------------- *)

apply negbT in SCHED.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 920)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  SERV : 0 < service_during sched j t1 t2
  LE : t1 <= t2
  SCHED : ~~ scheduled_at sched j t1
  ============================
  exists t : nat,
    t1 <= t < t2 /\ scheduled_at sched j t /\ service_during sched j t1 t = 0

----------------------------------------------------------------------------- *)

      move: SERV.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 923)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  LE : t1 <= t2
  SCHED : ~~ scheduled_at sched j t1
  ============================
  0 < service_during sched j t1 t2 ->
  exists t : nat,
    t1 <= t < t2 /\ scheduled_at sched j t /\ service_during sched j t1 t = 0

----------------------------------------------------------------------------- *)

      rewrite /service_during ⇒ /sum_seq_gt0P [t [IN SCHEDt]].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 981)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  LE : t1 <= t2
  SCHED : ~~ scheduled_at sched j t1
  t : nat_eqType
  IN : t \in index_iota t1 t2
  SCHEDt : 0 < service_at sched j t
  ============================
  exists t0 : nat,
    t1 <= t0 < t2 /\
    scheduled_at sched j t0 /\ \sum_(t1 <= t3 < t0) service_at sched j t3 = 0

----------------------------------------------------------------------------- *)

      rewrite service_at_def /= lt0b in SCHEDt.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1012)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  LE : t1 <= t2
  SCHED : ~~ scheduled_at sched j t1
  t : nat_eqType
  IN : t \in index_iota t1 t2
  SCHEDt : sched t == Some j
  ============================
  exists t0 : nat,
    t1 <= t0 < t2 /\
    scheduled_at sched j t0 /\ \sum_(t1 <= t3 < t0) service_at sched j t3 = 0

----------------------------------------------------------------------------- *)

      rewrite mem_iota subnKC in IN; last by done.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1043)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  LE : t1 <= t2
  SCHED : ~~ scheduled_at sched j t1
  t : nat_eqType
  SCHEDt : sched t == Some j
  IN : t1 <= t < t2
  ============================
  exists t0 : nat,
    t1 <= t0 < t2 /\
    scheduled_at sched j t0 /\ \sum_(t1 <= t3 < t0) service_at sched j t3 = 0

----------------------------------------------------------------------------- *)

      move: IN ⇒ /andP [IN1 IN2].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1100)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  LE : t1 <= t2
  SCHED : ~~ scheduled_at sched j t1
  t : nat_eqType
  SCHEDt : sched t == Some j
  IN1 : t1 <= t
  IN2 : t < t2
  ============================
  exists t0 : nat,
    t1 <= t0 < t2 /\
    scheduled_at sched j t0 /\ \sum_(t1 <= t3 < t0) service_at sched j t3 = 0

----------------------------------------------------------------------------- *)

      move: (exists_first_intermediate_point
               ((fun t ⇒ scheduled_at sched j t)) t1 t IN1 SCHED) ⇒ A.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1106)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  LE : t1 <= t2
  SCHED : ~~ scheduled_at sched j t1
  t : nat_eqType
  SCHEDt : sched t == Some j
  IN1 : t1 <= t
  IN2 : t < t2
  A : scheduled_at sched j t ->
      exists t0 : nat,
        t1 < t0 <= t /\
        (forall x : nat, t1 <= x < t0 -> ~~ scheduled_at sched j x) /\
        scheduled_at sched j t0
  ============================
  exists t0 : nat,
    t1 <= t0 < t2 /\
    scheduled_at sched j t0 /\ \sum_(t1 <= t3 < t0) service_at sched j t3 = 0

----------------------------------------------------------------------------- *)

      feed A; first by rewrite scheduled_at_def/=.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1112)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  LE : t1 <= t2
  SCHED : ~~ scheduled_at sched j t1
  t : nat_eqType
  SCHEDt : sched t == Some j
  IN1 : t1 <= t
  IN2 : t < t2
  A : exists t0 : nat,
        t1 < t0 <= t /\
        (forall x : nat, t1 <= x < t0 -> ~~ scheduled_at sched j x) /\
        scheduled_at sched j t0
  ============================
  exists t0 : nat,
    t1 <= t0 < t2 /\
    scheduled_at sched j t0 /\ \sum_(t1 <= t3 < t0) service_at sched j t3 = 0

----------------------------------------------------------------------------- *)

      move: A ⇒ [x [/andP [T1 T4] [T2 T3]]].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1192)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  LE : t1 <= t2
  SCHED : ~~ scheduled_at sched j t1
  t : nat_eqType
  SCHEDt : sched t == Some j
  IN1 : t1 <= t
  IN2 : t < t2
  x : nat
  T1 : t1 < x
  T4 : x <= t
  T2 : forall x0 : nat, t1 <= x0 < x -> ~~ scheduled_at sched j x0
  T3 : scheduled_at sched j x
  ============================
  exists t0 : nat,
    t1 <= t0 < t2 /\
    scheduled_at sched j t0 /\ \sum_(t1 <= t3 < t0) service_at sched j t3 = 0

----------------------------------------------------------------------------- *)

      ∃ x; repeat split; try done.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 1196)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  LE : t1 <= t2
  SCHED : ~~ scheduled_at sched j t1
  t : nat_eqType
  SCHEDt : sched t == Some j
  IN1 : t1 <= t
  IN2 : t < t2
  x : nat
  T1 : t1 < x
  T4 : x <= t
  T2 : forall x0 : nat, t1 <= x0 < x -> ~~ scheduled_at sched j x0
  T3 : scheduled_at sched j x
  ============================
  t1 <= x < t2

subgoal 2 (ID 1201) is:
 \sum_(t1 <= t0 < x) service_at sched j t0 = 0

----------------------------------------------------------------------------- *)

      - apply/andP; split; first by apply ltnW.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 1274)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  LE : t1 <= t2
  SCHED : ~~ scheduled_at sched j t1
  t : nat_eqType
  SCHEDt : sched t == Some j
  IN1 : t1 <= t
  IN2 : t < t2
  x : nat
  T1 : t1 < x
  T4 : x <= t
  T2 : forall x0 : nat, t1 <= x0 < x -> ~~ scheduled_at sched j x0
  T3 : scheduled_at sched j x
  ============================
  x < t2

subgoal 2 (ID 1201) is:
 \sum_(t1 <= t0 < x) service_at sched j t0 = 0

----------------------------------------------------------------------------- *)

          by apply leq_ltn_trans with t.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1201)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  LE : t1 <= t2
  SCHED : ~~ scheduled_at sched j t1
  t : nat_eqType
  SCHEDt : sched t == Some j
  IN1 : t1 <= t
  IN2 : t < t2
  x : nat
  T1 : t1 < x
  T4 : x <= t
  T2 : forall x0 : nat, t1 <= x0 < x -> ~~ scheduled_at sched j x0
  T3 : scheduled_at sched j x
  ============================
  \sum_(t1 <= t0 < x) service_at sched j t0 = 0

----------------------------------------------------------------------------- *)

      - apply/eqP; rewrite big_nat_cond big1 //.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1352)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  LE : t1 <= t2
  SCHED : ~~ scheduled_at sched j t1
  t : nat_eqType
  SCHEDt : sched t == Some j
  IN1 : t1 <= t
  IN2 : t < t2
  x : nat
  T1 : t1 < x
  T4 : x <= t
  T2 : forall x0 : nat, t1 <= x0 < x -> ~~ scheduled_at sched j x0
  T3 : scheduled_at sched j x
  ============================
  forall i : nat, (t1 <= i < x) && true -> service_at sched j i = 0

----------------------------------------------------------------------------- *)

        move ⇒ y /andP [T5 _].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1419)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  LE : t1 <= t2
  SCHED : ~~ scheduled_at sched j t1
  t : nat_eqType
  SCHEDt : sched t == Some j
  IN1 : t1 <= t
  IN2 : t < t2
  x : nat
  T1 : t1 < x
  T4 : x <= t
  T2 : forall x0 : nat, t1 <= x0 < x -> ~~ scheduled_at sched j x0
  T3 : scheduled_at sched j x
  y : nat
  T5 : t1 <= y < x
  ============================
  service_at sched j y = 0

----------------------------------------------------------------------------- *)

        apply/eqP.

(* ----------------------------------[ coqtop ]---------------------------------

1 focused subgoal
(shelved: 1) (ID 1474)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  LE : t1 <= t2
  SCHED : ~~ scheduled_at sched j t1
  t : nat_eqType
  SCHEDt : sched t == Some j
  IN1 : t1 <= t
  IN2 : t < t2
  x : nat
  T1 : t1 < x
  T4 : x <= t
  T2 : forall x0 : nat, t1 <= x0 < x -> ~~ scheduled_at sched j x0
  T3 : scheduled_at sched j x
  y : nat
  T5 : t1 <= y < x
  ============================
  service_at sched j y == 0

----------------------------------------------------------------------------- *)

        rewrite service_at_def /= eqb0.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1485)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  LE : t1 <= t2
  SCHED : ~~ scheduled_at sched j t1
  t : nat_eqType
  SCHEDt : sched t == Some j
  IN1 : t1 <= t
  IN2 : t < t2
  x : nat
  T1 : t1 < x
  T4 : x <= t
  T2 : forall x0 : nat, t1 <= x0 < x -> ~~ scheduled_at sched j x0
  T3 : scheduled_at sched j x
  y : nat
  T5 : t1 <= y < x
  ============================
  sched y != Some j

----------------------------------------------------------------------------- *)

        by specialize (T2 y); rewrite scheduled_at_def/= in T2; apply T2.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

    }

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

  Qed.

  Lemma service_during_ge :
    ∀ j t1 t2 k,
      service_during sched j t1 t2 > k →
      t1 < t2.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 655)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  ============================
  forall (j : Job) (t1 t2 : instant) (k : nat),
  k < service_during sched j t1 t2 -> t1 < t2

----------------------------------------------------------------------------- *)

  Proof.
    move⇒ j t1 t2 k SERV.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 660)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  k : nat
  SERV : k < service_during sched j t1 t2
  ============================
  t1 < t2

----------------------------------------------------------------------------- *)

    rewrite leqNgt.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 664)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  k : nat
  SERV : k < service_during sched j t1 t2
  ============================
  ~~ (t2 < succn t1)

----------------------------------------------------------------------------- *)

    apply/negP ⇒ CONTR.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 686)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  k : nat
  SERV : k < service_during sched j t1 t2
  CONTR : t2 < succn t1
  ============================
  False

----------------------------------------------------------------------------- *)

    move: SERV.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 688)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  k : nat
  CONTR : t2 < succn t1
  ============================
  k < service_during sched j t1 t2 -> False

----------------------------------------------------------------------------- *)

    by rewrite /service_during big_geq.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

  Qed.

Next, we prove that if in some time interval [t1,t2) a job [j] receives [k] units of service, then there exists a time instant t ∈ [t1,t2) such that [j] is scheduled at time [t] and service of job [j] within interval [t1,t) is equal to [k].
  Lemma incremental_service_during:
    ∀ j t1 t2 k,
      service_during sched j t1 t2 > k →
      ∃ t, t1 ≤ t < t2 ∧ scheduled_at sched j t ∧ service_during sched j t1 t = k.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 676)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  ============================
  forall (j : Job) (t1 t2 : instant) (k : nat),
  k < service_during sched j t1 t2 ->
  exists t : nat,
    t1 <= t < t2 /\ scheduled_at sched j t /\ service_during sched j t1 t = k

----------------------------------------------------------------------------- *)

  Proof.
    move⇒ j t1 t2 k SERV.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 681)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  k : nat
  SERV : k < service_during sched j t1 t2
  ============================
  exists t : nat,
    t1 <= t < t2 /\ scheduled_at sched j t /\ service_during sched j t1 t = k

----------------------------------------------------------------------------- *)

    have LE: t1 < t2 by move: (service_during_ge _ _ _ _ SERV).

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 694)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  k : nat
  SERV : k < service_during sched j t1 t2
  LE : t1 < t2
  ============================
  exists t : nat,
    t1 <= t < t2 /\ scheduled_at sched j t /\ service_during sched j t1 t = k

----------------------------------------------------------------------------- *)

    induction k; first by apply positive_service_during in SERV.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 709)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  k : nat
  SERV : succn k < service_during sched j t1 t2
  LE : t1 < t2
  IHk : k < service_during sched j t1 t2 ->
        exists t : nat,
          t1 <= t < t2 /\
          scheduled_at sched j t /\ service_during sched j t1 t = k
  ============================
  exists t : nat,
    t1 <= t < t2 /\
    scheduled_at sched j t /\ service_during sched j t1 t = succn k

----------------------------------------------------------------------------- *)

    feed IHk; first by apply ltn_trans with k.+1.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 717)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  k : nat
  SERV : succn k < service_during sched j t1 t2
  LE : t1 < t2
  IHk : exists t : nat,
          t1 <= t < t2 /\
          scheduled_at sched j t /\ service_during sched j t1 t = k
  ============================
  exists t : nat,
    t1 <= t < t2 /\
    scheduled_at sched j t /\ service_during sched j t1 t = succn k

----------------------------------------------------------------------------- *)

    move: IHk ⇒ [t [/andP [NEQ1 NEQ2] [SCHEDt SERVk]]].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 791)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  k : nat
  SERV : succn k < service_during sched j t1 t2
  LE : t1 < t2
  t : nat
  NEQ1 : t1 <= t
  NEQ2 : t < t2
  SCHEDt : scheduled_at sched j t
  SERVk : service_during sched j t1 t = k
  ============================
  exists t0 : nat,
    t1 <= t0 < t2 /\
    scheduled_at sched j t0 /\ service_during sched j t1 t0 = succn k

----------------------------------------------------------------------------- *)

    have SERVk1: service_during sched j t1 t.+1 = k.+1.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 797)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  k : nat
  SERV : succn k < service_during sched j t1 t2
  LE : t1 < t2
  t : nat
  NEQ1 : t1 <= t
  NEQ2 : t < t2
  SCHEDt : scheduled_at sched j t
  SERVk : service_during sched j t1 t = k
  ============================
  service_during sched j t1 (succn t) = succn k

subgoal 2 (ID 799) is:
 exists t0 : nat,
   t1 <= t0 < t2 /\
   scheduled_at sched j t0 /\ service_during sched j t1 t0 = succn k

----------------------------------------------------------------------------- *)

    {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 797)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  k : nat
  SERV : succn k < service_during sched j t1 t2
  LE : t1 < t2
  t : nat
  NEQ1 : t1 <= t
  NEQ2 : t < t2
  SCHEDt : scheduled_at sched j t
  SERVk : service_during sched j t1 t = k
  ============================
  service_during sched j t1 (succn t) = succn k

----------------------------------------------------------------------------- *)

rewrite -(service_during_cat _ _ _ t); last by apply/andP; split.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 821)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  k : nat
  SERV : succn k < service_during sched j t1 t2
  LE : t1 < t2
  t : nat
  NEQ1 : t1 <= t
  NEQ2 : t < t2
  SCHEDt : scheduled_at sched j t
  SERVk : service_during sched j t1 t = k
  ============================
  service_during sched j t1 t + service_during sched j t (succn t) = succn k

----------------------------------------------------------------------------- *)

      rewrite SERVk -[X in _ = X]addn1; apply/eqP; rewrite eqn_add2l.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 922)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  k : nat
  SERV : succn k < service_during sched j t1 t2
  LE : t1 < t2
  t : nat
  NEQ1 : t1 <= t
  NEQ2 : t < t2
  SCHEDt : scheduled_at sched j t
  SERVk : service_during sched j t1 t = k
  ============================
  service_during sched j t (succn t) == 1

----------------------------------------------------------------------------- *)

      rewrite /service_during big_nat1 service_at_def /=.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 944)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  k : nat
  SERV : succn k < service_during sched j t1 t2
  LE : t1 < t2
  t : nat
  NEQ1 : t1 <= t
  NEQ2 : t < t2
  SCHEDt : scheduled_at sched j t
  SERVk : service_during sched j t1 t = k
  ============================
  (sched t == Some j) == 1

----------------------------------------------------------------------------- *)

      by rewrite eqb1 -scheduled_at_def /=.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 799)

subgoal 1 (ID 799) is:
 exists t0 : nat,
   t1 <= t0 < t2 /\
   scheduled_at sched j t0 /\ service_during sched j t1 t0 = succn k

----------------------------------------------------------------------------- *)

    }

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 799)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  k : nat
  SERV : succn k < service_during sched j t1 t2
  LE : t1 < t2
  t : nat
  NEQ1 : t1 <= t
  NEQ2 : t < t2
  SCHEDt : scheduled_at sched j t
  SERVk : service_during sched j t1 t = k
  SERVk1 : service_during sched j t1 (succn t) = succn k
  ============================
  exists t0 : nat,
    t1 <= t0 < t2 /\
    scheduled_at sched j t0 /\ service_during sched j t1 t0 = succn k

----------------------------------------------------------------------------- *)

    move: SERV; rewrite -(service_during_cat _ _ _ t.+1); last first.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 980)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  k : nat
  LE : t1 < t2
  t : nat
  NEQ1 : t1 <= t
  NEQ2 : t < t2
  SCHEDt : scheduled_at sched j t
  SERVk : service_during sched j t1 t = k
  SERVk1 : service_during sched j t1 (succn t) = succn k
  ============================
  t1 <= succn t <= t2

subgoal 2 (ID 979) is:
 succn k <
 service_during sched j t1 (succn t) + service_during sched j (succn t) t2 ->
 exists t0 : nat,
   t1 <= t0 < t2 /\
   scheduled_at sched j t0 /\ service_during sched j t1 t0 = succn k

----------------------------------------------------------------------------- *)

    {
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 980)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  k : nat
  LE : t1 < t2
  t : nat
  NEQ1 : t1 <= t
  NEQ2 : t < t2
  SCHEDt : scheduled_at sched j t
  SERVk : service_during sched j t1 t = k
  SERVk1 : service_during sched j t1 (succn t) = succn k
  ============================
  t1 <= succn t <= t2

----------------------------------------------------------------------------- *)

by apply/andP; split; first apply leq_trans with t.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 979)

subgoal 1 (ID 979) is:
 succn k <
 service_during sched j t1 (succn t) + service_during sched j (succn t) t2 ->
 exists t0 : nat,
   t1 <= t0 < t2 /\
   scheduled_at sched j t0 /\ service_during sched j t1 t0 = succn k

----------------------------------------------------------------------------- *)

}

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 979)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  k : nat
  LE : t1 < t2
  t : nat
  NEQ1 : t1 <= t
  NEQ2 : t < t2
  SCHEDt : scheduled_at sched j t
  SERVk : service_during sched j t1 t = k
  SERVk1 : service_during sched j t1 (succn t) = succn k
  ============================
  succn k <
  service_during sched j t1 (succn t) + service_during sched j (succn t) t2 ->
  exists t0 : nat,
    t1 <= t0 < t2 /\
    scheduled_at sched j t0 /\ service_during sched j t1 t0 = succn k

----------------------------------------------------------------------------- *)

    rewrite SERVk1 -addn1 leq_add2l; move ⇒ SERV.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1020)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  k : nat
  LE : t1 < t2
  t : nat
  NEQ1 : t1 <= t
  NEQ2 : t < t2
  SCHEDt : scheduled_at sched j t
  SERVk : service_during sched j t1 t = k
  SERVk1 : service_during sched j t1 (succn t) = succn k
  SERV : 0 < service_during sched j (succn t) t2
  ============================
  exists t0 : nat,
    t1 <= t0 < t2 /\
    scheduled_at sched j t0 /\ service_during sched j t1 t0 = succn k

----------------------------------------------------------------------------- *)

    destruct (scheduled_at sched j t.+1) eqn:SCHED.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 1033)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  k : nat
  LE : t1 < t2
  t : nat
  NEQ1 : t1 <= t
  NEQ2 : t < t2
  SCHEDt : scheduled_at sched j t
  SERVk : service_during sched j t1 t = k
  SERVk1 : service_during sched j t1 (succn t) = succn k
  SERV : 0 < service_during sched j (succn t) t2
  SCHED : scheduled_at sched j (succn t) = true
  ============================
  exists t0 : nat,
    t1 <= t0 < t2 /\
    scheduled_at sched j t0 /\ service_during sched j t1 t0 = succn k

subgoal 2 (ID 1034) is:
 exists t0 : nat,
   t1 <= t0 < t2 /\
   scheduled_at sched j t0 /\ service_during sched j t1 t0 = succn k

----------------------------------------------------------------------------- *)

    - ∃ t.+1; repeat split; try done.
(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 1038)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  k : nat
  LE : t1 < t2
  t : nat
  NEQ1 : t1 <= t
  NEQ2 : t < t2
  SCHEDt : scheduled_at sched j t
  SERVk : service_during sched j t1 t = k
  SERVk1 : service_during sched j t1 (succn t) = succn k
  SERV : 0 < service_during sched j (succn t) t2
  SCHED : scheduled_at sched j (succn t) = true
  ============================
  t1 <= succn t < t2

subgoal 2 (ID 1034) is:
 exists t0 : nat,
   t1 <= t0 < t2 /\
   scheduled_at sched j t0 /\ service_during sched j t1 t0 = succn k

----------------------------------------------------------------------------- *)

apply/andP; split.

(* ----------------------------------[ coqtop ]---------------------------------

3 subgoals (ID 1093)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  k : nat
  LE : t1 < t2
  t : nat
  NEQ1 : t1 <= t
  NEQ2 : t < t2
  SCHEDt : scheduled_at sched j t
  SERVk : service_during sched j t1 t = k
  SERVk1 : service_during sched j t1 (succn t) = succn k
  SERV : 0 < service_during sched j (succn t) t2
  SCHED : scheduled_at sched j (succn t) = true
  ============================
  t1 <= succn t

subgoal 2 (ID 1094) is:
 succn t < t2
subgoal 3 (ID 1034) is:
 exists t0 : nat,
   t1 <= t0 < t2 /\
   scheduled_at sched j t0 /\ service_during sched j t1 t0 = succn k

----------------------------------------------------------------------------- *)

      + apply leq_trans with t; by done.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 1094)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  k : nat
  LE : t1 < t2
  t : nat
  NEQ1 : t1 <= t
  NEQ2 : t < t2
  SCHEDt : scheduled_at sched j t
  SERVk : service_during sched j t1 t = k
  SERVk1 : service_during sched j t1 (succn t) = succn k
  SERV : 0 < service_during sched j (succn t) t2
  SCHED : scheduled_at sched j (succn t) = true
  ============================
  succn t < t2

subgoal 2 (ID 1034) is:
 exists t0 : nat,
   t1 <= t0 < t2 /\
   scheduled_at sched j t0 /\ service_during sched j t1 t0 = succn k

----------------------------------------------------------------------------- *)

      + rewrite ltnNge; apply/negP; intros CONTR.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 1122)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  k : nat
  LE : t1 < t2
  t : nat
  NEQ1 : t1 <= t
  NEQ2 : t < t2
  SCHEDt : scheduled_at sched j t
  SERVk : service_during sched j t1 t = k
  SERVk1 : service_during sched j t1 (succn t) = succn k
  SERV : 0 < service_during sched j (succn t) t2
  SCHED : scheduled_at sched j (succn t) = true
  CONTR : t2 <= succn t
  ============================
  False

subgoal 2 (ID 1034) is:
 exists t0 : nat,
   t1 <= t0 < t2 /\
   scheduled_at sched j t0 /\ service_during sched j t1 t0 = succn k

----------------------------------------------------------------------------- *)

          by move: SERV; rewrite /service_during big_geq.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1034)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  k : nat
  LE : t1 < t2
  t : nat
  NEQ1 : t1 <= t
  NEQ2 : t < t2
  SCHEDt : scheduled_at sched j t
  SERVk : service_during sched j t1 t = k
  SERVk1 : service_during sched j t1 (succn t) = succn k
  SERV : 0 < service_during sched j (succn t) t2
  SCHED : scheduled_at sched j (succn t) = false
  ============================
  exists t0 : nat,
    t1 <= t0 < t2 /\
    scheduled_at sched j t0 /\ service_during sched j t1 t0 = succn k

----------------------------------------------------------------------------- *)

    - apply negbT in SCHED.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1172)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  k : nat
  LE : t1 < t2
  t : nat
  NEQ1 : t1 <= t
  NEQ2 : t < t2
  SCHEDt : scheduled_at sched j t
  SERVk : service_during sched j t1 t = k
  SERVk1 : service_during sched j t1 (succn t) = succn k
  SERV : 0 < service_during sched j (succn t) t2
  SCHED : ~~ scheduled_at sched j (succn t)
  ============================
  exists t0 : nat,
    t1 <= t0 < t2 /\
    scheduled_at sched j t0 /\ service_during sched j t1 t0 = succn k

----------------------------------------------------------------------------- *)

       move: SERV; rewrite /service /service_during; move ⇒ /sum_seq_gt0P [x [INx SCHEDx]].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1240)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  k : nat
  LE : t1 < t2
  t : nat
  NEQ1 : t1 <= t
  NEQ2 : t < t2
  SCHEDt : scheduled_at sched j t
  SERVk : service_during sched j t1 t = k
  SERVk1 : service_during sched j t1 (succn t) = succn k
  SCHED : ~~ scheduled_at sched j (succn t)
  x : nat_eqType
  INx : x \in index_iota (succn t) t2
  SCHEDx : 0 < service_at sched j x
  ============================
  exists t0 : nat,
    t1 <= t0 < t2 /\
    scheduled_at sched j t0 /\
    \sum_(t1 <= t3 < t0) service_at sched j t3 = succn k

----------------------------------------------------------------------------- *)

       rewrite service_at_def lt0b in SCHEDx.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1277)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  k : nat
  LE : t1 < t2
  t : nat
  NEQ1 : t1 <= t
  NEQ2 : t < t2
  SCHEDt : scheduled_at sched j t
  SERVk : service_during sched j t1 t = k
  SERVk1 : service_during sched j t1 (succn t) = succn k
  SCHED : ~~ scheduled_at sched j (succn t)
  x : nat_eqType
  INx : x \in index_iota (succn t) t2
  SCHEDx : sched x == Some j
  ============================
  exists t0 : nat,
    t1 <= t0 < t2 /\
    scheduled_at sched j t0 /\
    \sum_(t1 <= t3 < t0) service_at sched j t3 = succn k

----------------------------------------------------------------------------- *)

       rewrite mem_iota subnKC in INx; last by done.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1315)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  k : nat
  LE : t1 < t2
  t : nat
  NEQ1 : t1 <= t
  NEQ2 : t < t2
  SCHEDt : scheduled_at sched j t
  SERVk : service_during sched j t1 t = k
  SERVk1 : service_during sched j t1 (succn t) = succn k
  SCHED : ~~ scheduled_at sched j (succn t)
  x : nat_eqType
  SCHEDx : sched x == Some j
  INx : t < x < t2
  ============================
  exists t0 : nat,
    t1 <= t0 < t2 /\
    scheduled_at sched j t0 /\
    \sum_(t1 <= t3 < t0) service_at sched j t3 = succn k

----------------------------------------------------------------------------- *)

       move: INx ⇒ /andP [INx1 INx2].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1379)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  k : nat
  LE : t1 < t2
  t : nat
  NEQ1 : t1 <= t
  NEQ2 : t < t2
  SCHEDt : scheduled_at sched j t
  SERVk : service_during sched j t1 t = k
  SERVk1 : service_during sched j t1 (succn t) = succn k
  SCHED : ~~ scheduled_at sched j (succn t)
  x : nat_eqType
  SCHEDx : sched x == Some j
  INx1 : t < x
  INx2 : x < t2
  ============================
  exists t0 : nat,
    t1 <= t0 < t2 /\
    scheduled_at sched j t0 /\
    \sum_(t1 <= t3 < t0) service_at sched j t3 = succn k

----------------------------------------------------------------------------- *)

       move: (exists_first_intermediate_point _ _ _ INx1 SCHED) ⇒ A.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1387)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  k : nat
  LE : t1 < t2
  t : nat
  NEQ1 : t1 <= t
  NEQ2 : t < t2
  SCHEDt : scheduled_at sched j t
  SERVk : service_during sched j t1 t = k
  SERVk1 : service_during sched j t1 (succn t) = succn k
  SCHED : ~~ scheduled_at sched j (succn t)
  x : nat_eqType
  SCHEDx : sched x == Some j
  INx1 : t < x
  INx2 : x < t2
  A : scheduled_at sched j x ->
      exists t0 : nat,
        succn t < t0 <= x /\
        (forall x : nat, t < x < t0 -> ~~ scheduled_at sched j x) /\
        scheduled_at sched j t0
  ============================
  exists t0 : nat,
    t1 <= t0 < t2 /\
    scheduled_at sched j t0 /\
    \sum_(t1 <= t3 < t0) service_at sched j t3 = succn k

----------------------------------------------------------------------------- *)

       feed A; first by rewrite scheduled_at_def/=.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1393)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  k : nat
  LE : t1 < t2
  t : nat
  NEQ1 : t1 <= t
  NEQ2 : t < t2
  SCHEDt : scheduled_at sched j t
  SERVk : service_during sched j t1 t = k
  SERVk1 : service_during sched j t1 (succn t) = succn k
  SCHED : ~~ scheduled_at sched j (succn t)
  x : nat_eqType
  SCHEDx : sched x == Some j
  INx1 : t < x
  INx2 : x < t2
  A : exists t0 : nat,
        succn t < t0 <= x /\
        (forall x : nat, t < x < t0 -> ~~ scheduled_at sched j x) /\
        scheduled_at sched j t0
  ============================
  exists t0 : nat,
    t1 <= t0 < t2 /\
    scheduled_at sched j t0 /\
    \sum_(t1 <= t3 < t0) service_at sched j t3 = succn k

----------------------------------------------------------------------------- *)

       move: A ⇒ [y [/andP [T1 T4] [T2 T3]]].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1473)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  k : nat
  LE : t1 < t2
  t : nat
  NEQ1 : t1 <= t
  NEQ2 : t < t2
  SCHEDt : scheduled_at sched j t
  SERVk : service_during sched j t1 t = k
  SERVk1 : service_during sched j t1 (succn t) = succn k
  SCHED : ~~ scheduled_at sched j (succn t)
  x : nat_eqType
  SCHEDx : sched x == Some j
  INx1 : t < x
  INx2 : x < t2
  y : nat
  T1 : succn t < y
  T4 : y <= x
  T2 : forall x : nat, t < x < y -> ~~ scheduled_at sched j x
  T3 : scheduled_at sched j y
  ============================
  exists t0 : nat,
    t1 <= t0 < t2 /\
    scheduled_at sched j t0 /\
    \sum_(t1 <= t3 < t0) service_at sched j t3 = succn k

----------------------------------------------------------------------------- *)

       ∃ y; repeat split ⇒ //.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 1477)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  k : nat
  LE : t1 < t2
  t : nat
  NEQ1 : t1 <= t
  NEQ2 : t < t2
  SCHEDt : scheduled_at sched j t
  SERVk : service_during sched j t1 t = k
  SERVk1 : service_during sched j t1 (succn t) = succn k
  SCHED : ~~ scheduled_at sched j (succn t)
  x : nat_eqType
  SCHEDx : sched x == Some j
  INx1 : t < x
  INx2 : x < t2
  y : nat
  T1 : succn t < y
  T4 : y <= x
  T2 : forall x : nat, t < x < y -> ~~ scheduled_at sched j x
  T3 : scheduled_at sched j y
  ============================
  t1 <= y < t2

subgoal 2 (ID 1552) is:
 \sum_(t1 <= t0 < y) service_at sched j t0 = succn k

----------------------------------------------------------------------------- *)

       + apply/andP; split.

(* ----------------------------------[ coqtop ]---------------------------------

3 subgoals (ID 1601)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  k : nat
  LE : t1 < t2
  t : nat
  NEQ1 : t1 <= t
  NEQ2 : t < t2
  SCHEDt : scheduled_at sched j t
  SERVk : service_during sched j t1 t = k
  SERVk1 : service_during sched j t1 (succn t) = succn k
  SCHED : ~~ scheduled_at sched j (succn t)
  x : nat_eqType
  SCHEDx : sched x == Some j
  INx1 : t < x
  INx2 : x < t2
  y : nat
  T1 : succn t < y
  T4 : y <= x
  T2 : forall x : nat, t < x < y -> ~~ scheduled_at sched j x
  T3 : scheduled_at sched j y
  ============================
  t1 <= y

subgoal 2 (ID 1602) is:
 y < t2
subgoal 3 (ID 1552) is:
 \sum_(t1 <= t0 < y) service_at sched j t0 = succn k

----------------------------------------------------------------------------- *)

         apply leq_trans with t; first by done.

(* ----------------------------------[ coqtop ]---------------------------------

3 subgoals (ID 1604)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  k : nat
  LE : t1 < t2
  t : nat
  NEQ1 : t1 <= t
  NEQ2 : t < t2
  SCHEDt : scheduled_at sched j t
  SERVk : service_during sched j t1 t = k
  SERVk1 : service_during sched j t1 (succn t) = succn k
  SCHED : ~~ scheduled_at sched j (succn t)
  x : nat_eqType
  SCHEDx : sched x == Some j
  INx1 : t < x
  INx2 : x < t2
  y : nat
  T1 : succn t < y
  T4 : y <= x
  T2 : forall x : nat, t < x < y -> ~~ scheduled_at sched j x
  T3 : scheduled_at sched j y
  ============================
  t <= y

subgoal 2 (ID 1602) is:
 y < t2
subgoal 3 (ID 1552) is:
 \sum_(t1 <= t0 < y) service_at sched j t0 = succn k

----------------------------------------------------------------------------- *)

         apply ltnW, ltn_trans with t.+1; by done.

(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 1602)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  k : nat
  LE : t1 < t2
  t : nat
  NEQ1 : t1 <= t
  NEQ2 : t < t2
  SCHEDt : scheduled_at sched j t
  SERVk : service_during sched j t1 t = k
  SERVk1 : service_during sched j t1 (succn t) = succn k
  SCHED : ~~ scheduled_at sched j (succn t)
  x : nat_eqType
  SCHEDx : sched x == Some j
  INx1 : t < x
  INx2 : x < t2
  y : nat
  T1 : succn t < y
  T4 : y <= x
  T2 : forall x : nat, t < x < y -> ~~ scheduled_at sched j x
  T3 : scheduled_at sched j y
  ============================
  y < t2

subgoal 2 (ID 1552) is:
 \sum_(t1 <= t0 < y) service_at sched j t0 = succn k

----------------------------------------------------------------------------- *)

           by apply leq_ltn_trans with x.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1552)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  k : nat
  LE : t1 < t2
  t : nat
  NEQ1 : t1 <= t
  NEQ2 : t < t2
  SCHEDt : scheduled_at sched j t
  SERVk : service_during sched j t1 t = k
  SERVk1 : service_during sched j t1 (succn t) = succn k
  SCHED : ~~ scheduled_at sched j (succn t)
  x : nat_eqType
  SCHEDx : sched x == Some j
  INx1 : t < x
  INx2 : x < t2
  y : nat
  T1 : succn t < y
  T4 : y <= x
  T2 : forall x : nat, t < x < y -> ~~ scheduled_at sched j x
  T3 : scheduled_at sched j y
  ============================
  \sum_(t1 <= t0 < y) service_at sched j t0 = succn k

----------------------------------------------------------------------------- *)

       + rewrite (@big_cat_nat _ _ _ t.+1) //=; [ | by apply leq_trans with t | by apply ltn_trans with t.+1].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1632)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  k : nat
  LE : t1 < t2
  t : nat
  NEQ1 : t1 <= t
  NEQ2 : t < t2
  SCHEDt : scheduled_at sched j t
  SERVk : service_during sched j t1 t = k
  SERVk1 : service_during sched j t1 (succn t) = succn k
  SCHED : ~~ scheduled_at sched j (succn t)
  x : nat_eqType
  SCHEDx : sched x == Some j
  INx1 : t < x
  INx2 : x < t2
  y : nat
  T1 : succn t < y
  T4 : y <= x
  T2 : forall x : nat, t < x < y -> ~~ scheduled_at sched j x
  T3 : scheduled_at sched j y
  ============================
  \sum_(t1 <= i < succn t) service_at sched j i +
  \sum_(succn t <= i < y) service_at sched j i = succn k

----------------------------------------------------------------------------- *)

         unfold service_during in SERVk1; rewrite SERVk1; apply/eqP.

(* ----------------------------------[ coqtop ]---------------------------------

1 focused subgoal
(shelved: 1) (ID 1762)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  k : nat
  LE : t1 < t2
  t : nat
  NEQ1 : t1 <= t
  NEQ2 : t < t2
  SCHEDt : scheduled_at sched j t
  SERVk : service_during sched j t1 t = k
  SERVk1 : \sum_(t1 <= t < succn t) service_at sched j t = succn k
  SCHED : ~~ scheduled_at sched j (succn t)
  x : nat_eqType
  SCHEDx : sched x == Some j
  INx1 : t < x
  INx2 : x < t2
  y : nat
  T1 : succn t < y
  T4 : y <= x
  T2 : forall x : nat, t < x < y -> ~~ scheduled_at sched j x
  T3 : scheduled_at sched j y
  ============================
  succn k + \sum_(succn t <= i < y) service_at sched j i == succn k

----------------------------------------------------------------------------- *)

         rewrite -{2}[k.+1]addn0 eqn_add2l.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1772)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  k : nat
  LE : t1 < t2
  t : nat
  NEQ1 : t1 <= t
  NEQ2 : t < t2
  SCHEDt : scheduled_at sched j t
  SERVk : service_during sched j t1 t = k
  SERVk1 : \sum_(t1 <= t < succn t) service_at sched j t = succn k
  SCHED : ~~ scheduled_at sched j (succn t)
  x : nat_eqType
  SCHEDx : sched x == Some j
  INx1 : t < x
  INx2 : x < t2
  y : nat
  T1 : succn t < y
  T4 : y <= x
  T2 : forall x : nat, t < x < y -> ~~ scheduled_at sched j x
  T3 : scheduled_at sched j y
  ============================
  \sum_(succn t <= i < y) service_at sched j i == 0

----------------------------------------------------------------------------- *)

         rewrite big_nat_cond big1 //; move ⇒ z /andP [H5 _].

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1859)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  k : nat
  LE : t1 < t2
  t : nat
  NEQ1 : t1 <= t
  NEQ2 : t < t2
  SCHEDt : scheduled_at sched j t
  SERVk : service_during sched j t1 t = k
  SERVk1 : \sum_(t1 <= t < succn t) service_at sched j t = succn k
  SCHED : ~~ scheduled_at sched j (succn t)
  x : nat_eqType
  SCHEDx : sched x == Some j
  INx1 : t < x
  INx2 : x < t2
  y : nat
  T1 : succn t < y
  T4 : y <= x
  T2 : forall x : nat, t < x < y -> ~~ scheduled_at sched j x
  T3 : scheduled_at sched j y
  z : nat
  H5 : t < z < y
  ============================
  service_at sched j z = 0

----------------------------------------------------------------------------- *)

         apply/eqP.

(* ----------------------------------[ coqtop ]---------------------------------

1 focused subgoal
(shelved: 1) (ID 1914)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  k : nat
  LE : t1 < t2
  t : nat
  NEQ1 : t1 <= t
  NEQ2 : t < t2
  SCHEDt : scheduled_at sched j t
  SERVk : service_during sched j t1 t = k
  SERVk1 : \sum_(t1 <= t < succn t) service_at sched j t = succn k
  SCHED : ~~ scheduled_at sched j (succn t)
  x : nat_eqType
  SCHEDx : sched x == Some j
  INx1 : t < x
  INx2 : x < t2
  y : nat
  T1 : succn t < y
  T4 : y <= x
  T2 : forall x : nat, t < x < y -> ~~ scheduled_at sched j x
  T3 : scheduled_at sched j y
  z : nat
  H5 : t < z < y
  ============================
  service_at sched j z == 0

----------------------------------------------------------------------------- *)

         rewrite service_at_def eqb0.

(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 1924)
  
  Job : JobType
  H : JobArrival Job
  H0 : JobCost Job
  arr_seq : arrival_sequence Job
  sched : schedule (processor_state Job)
  j : Job
  t1, t2 : instant
  k : nat
  LE : t1 < t2
  t : nat
  NEQ1 : t1 <= t
  NEQ2 : t < t2
  SCHEDt : scheduled_at sched j t
  SERVk : service_during sched j t1 t = k
  SERVk1 : \sum_(t1 <= t < succn t) service_at sched j t = succn k
  SCHED : ~~ scheduled_at sched j (succn t)
  x : nat_eqType
  SCHEDx : sched x == Some j
  INx1 : t < x
  INx2 : x < t2
  y : nat
  T1 : succn t < y
  T4 : y <= x
  T2 : forall x : nat, t < x < y -> ~~ scheduled_at sched j x
  T3 : scheduled_at sched j y
  z : nat
  H5 : t < z < y
  ============================
  sched z != Some j

----------------------------------------------------------------------------- *)

         by specialize (T2 z); rewrite scheduled_at_def/= in T2; apply T2.

(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

----------------------------------------------------------------------------- *)

  Qed.

End IncrementalService.

Automation

We add the above lemmas into a "Hint Database" basic_facts, so Coq will be able to apply them automatically.
Hint Resolve ideal_proc_model_is_a_uniprocessor_model
     ideal_proc_model_ensures_ideal_progress
     ideal_proc_model_provides_unit_service : basic_facts.

We also provide tactics for case analysis on ideal processor state.
The first tactic generates two sub-goals: one with idle processor and the other with processor executing a job named [JobName].
Ltac ideal_proc_model_sched_case_analysis sched t JobName :=
  let Idle := fresh "Idle" in
  let Sched := fresh "Sched_" JobName in
  destruct (ideal_proc_model_sched_case_analysis sched t) as [Idle | [JobName Sched]].

The second tactic is similar to the first, but it additionally generates two equalities: [sched t = None] and [sched t = Some j].
Ltac ideal_proc_model_sched_case_analysis_eq sched t JobName :=
  let Idle := fresh "Idle" in
  let IdleEq := fresh "Eq" Idle in
  let Sched := fresh "Sched_" JobName in
  let SchedEq := fresh "Eq" Sched in
  destruct (ideal_proc_model_sched_case_analysis sched t) as [Idle | [JobName Sched]];
  [move: (Idle) ⇒ /eqP IdleEq; rewrite ?IdleEq
  | move: (Sched); simpl; move ⇒ /eqP SchedEq; rewrite ?SchedEq].