Library prosa.analysis.facts.job_index


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

Welcome to Coq 8.11.2 (June 2020)

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

Require Export prosa.analysis.facts.model.task_arrivals.

In this section, we prove some properties related to [job_index].
Section JobIndexLemmas.

Consider any type of tasks ...
  Context {Task : TaskType}.

... and any jobs associated with the tasks.
  Context {Job : JobType}.
  Context `{JobTask Job Task}.
  Context `{JobArrival Job}.

Consider any arrival sequence with consistent and non-duplicate arrivals, ...
  Variable arr_seq : arrival_sequence Job.
  Hypothesis H_consistent_arrivals : consistent_arrival_times arr_seq.
  Hypothesis H_uniq_arr_seq : arrival_sequence_uniq arr_seq.

... and any two jobs [j1] and [j2] from this arrival sequence that stem from the same task.
  Variable j1 j2 : Job.
  Hypothesis H_j1_from_arrival_sequence: arrives_in arr_seq j1.
  Hypothesis H_j2_from_arrival_sequence: arrives_in arr_seq j2.
  Hypothesis H_same_task: job_task j1 = job_task j2.

In the next section, we prove some basic properties about jobs with equal indices.
  Section EqualJobIndex.

Assume that the jobs [j1] and [j2] have the same [job_index] in the arrival sequence.
    Hypothesis H_equal_index: job_index arr_seq j1 = job_index arr_seq j2.

To show that jobs [j1] and [j2] are equal, we'll perform case analysis on the relation between their arrival times.
Jobs with equal indices have to be equal regardless of their arrival times because of the way [job_index] is defined (i.e., jobs are first ordered according to their arrival times and ties are broken arbitrarily due to which no two unequal jobs have the same [job_index]).
In case job [j2] arrives after or at the same time as [j1] arrives, we show that the jobs are equal.
    Lemma case_arrival_lte_implies_equal_job:
      job_arrival j1 ≤ job_arrival j2 → j1 = j2.

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

1 subgoal (ID 61)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j1, j2 : Job
  H_j1_from_arrival_sequence : arrives_in arr_seq j1
  H_j2_from_arrival_sequence : arrives_in arr_seq j2
  H_same_task : job_task j1 = job_task j2
  H_equal_index : job_index arr_seq j1 = job_index arr_seq j2
  ============================
  job_arrival j1 <= job_arrival j2 -> j1 = j2

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

    Proof.
      move ⇒ ARR_LT.

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

1 subgoal (ID 62)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j1, j2 : Job
  H_j1_from_arrival_sequence : arrives_in arr_seq j1
  H_j2_from_arrival_sequence : arrives_in arr_seq j2
  H_same_task : job_task j1 = job_task j2
  H_equal_index : job_index arr_seq j1 = job_index arr_seq j2
  ARR_LT : job_arrival j1 <= job_arrival j2
  ============================
  j1 = j2

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

      move: H_equal_index ⇒ IND.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 64)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j1, j2 : Job
  H_j1_from_arrival_sequence : arrives_in arr_seq j1
  H_j2_from_arrival_sequence : arrives_in arr_seq j2
  H_same_task : job_task j1 = job_task j2
  H_equal_index : job_index arr_seq j1 = job_index arr_seq j2
  ARR_LT : job_arrival j1 <= job_arrival j2
  IND : job_index arr_seq j1 = job_index arr_seq j2
  ============================
  j1 = j2

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

      apply task_arrivals_up_to_prefix_cat with (arr_seq0 := arr_seq) in ARR_LT ⇒ //.

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

1 subgoal (ID 69)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j1, j2 : Job
  H_j1_from_arrival_sequence : arrives_in arr_seq j1
  H_j2_from_arrival_sequence : arrives_in arr_seq j2
  H_same_task : job_task j1 = job_task j2
  H_equal_index : job_index arr_seq j1 = job_index arr_seq j2
  ARR_LT : prefix Job (task_arrivals_up_to_job_arrival arr_seq j1)
             (task_arrivals_up_to_job_arrival arr_seq j2)
  IND : job_index arr_seq j1 = job_index arr_seq j2
  ============================
  j1 = j2

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

      move : ARR_LT ⇒ [xs ARR_CAT].
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 108)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j1, j2 : Job
  H_j1_from_arrival_sequence : arrives_in arr_seq j1
  H_j2_from_arrival_sequence : arrives_in arr_seq j2
  H_same_task : job_task j1 = job_task j2
  H_equal_index, IND : job_index arr_seq j1 = job_index arr_seq j2
  xs : seq Job
  ARR_CAT : task_arrivals_up_to_job_arrival arr_seq j1 ++ xs =
            task_arrivals_up_to_job_arrival arr_seq j2
  ============================
  j1 = j2

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

      apply eq_ind_in_seq with (xs := task_arrivals_up_to_job_arrival arr_seq j2) ⇒ //.

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

4 subgoals (ID 114)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j1, j2 : Job
  H_j1_from_arrival_sequence : arrives_in arr_seq j1
  H_j2_from_arrival_sequence : arrives_in arr_seq j2
  H_same_task : job_task j1 = job_task j2
  H_equal_index, IND : job_index arr_seq j1 = job_index arr_seq j2
  xs : seq Job
  ARR_CAT : task_arrivals_up_to_job_arrival arr_seq j1 ++ xs =
            task_arrivals_up_to_job_arrival arr_seq j2
  ============================
  index j1 (task_arrivals_up_to_job_arrival arr_seq j2) =
  index j2 (task_arrivals_up_to_job_arrival arr_seq j2)

subgoal 2 (ID 115) is:
 uniq (task_arrivals_up_to_job_arrival arr_seq j2)
subgoal 3 (ID 116) is:
 j1 \in task_arrivals_up_to_job_arrival arr_seq j2
subgoal 4 (ID 117) is:
 j2 \in task_arrivals_up_to_job_arrival arr_seq j2

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

      - now rewrite -/(job_index _ _) -IND -ARR_CAT index_cat ifT;
          try apply arrives_in_task_arrivals_up_to.

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

3 subgoals (ID 115)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j1, j2 : Job
  H_j1_from_arrival_sequence : arrives_in arr_seq j1
  H_j2_from_arrival_sequence : arrives_in arr_seq j2
  H_same_task : job_task j1 = job_task j2
  H_equal_index, IND : job_index arr_seq j1 = job_index arr_seq j2
  xs : seq Job
  ARR_CAT : task_arrivals_up_to_job_arrival arr_seq j1 ++ xs =
            task_arrivals_up_to_job_arrival arr_seq j2
  ============================
  uniq (task_arrivals_up_to_job_arrival arr_seq j2)

subgoal 2 (ID 116) is:
 j1 \in task_arrivals_up_to_job_arrival arr_seq j2
subgoal 3 (ID 117) is:
 j2 \in task_arrivals_up_to_job_arrival arr_seq j2

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

      - now apply uniq_task_arrivals.

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

2 subgoals (ID 116)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j1, j2 : Job
  H_j1_from_arrival_sequence : arrives_in arr_seq j1
  H_j2_from_arrival_sequence : arrives_in arr_seq j2
  H_same_task : job_task j1 = job_task j2
  H_equal_index, IND : job_index arr_seq j1 = job_index arr_seq j2
  xs : seq Job
  ARR_CAT : task_arrivals_up_to_job_arrival arr_seq j1 ++ xs =
            task_arrivals_up_to_job_arrival arr_seq j2
  ============================
  j1 \in task_arrivals_up_to_job_arrival arr_seq j2

subgoal 2 (ID 117) is:
 j2 \in task_arrivals_up_to_job_arrival arr_seq j2

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

      - rewrite -ARR_CAT mem_cat; apply /orP.

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

2 focused subgoals
(shelved: 1) (ID 288)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j1, j2 : Job
  H_j1_from_arrival_sequence : arrives_in arr_seq j1
  H_j2_from_arrival_sequence : arrives_in arr_seq j2
  H_same_task : job_task j1 = job_task j2
  H_equal_index, IND : job_index arr_seq j1 = job_index arr_seq j2
  xs : seq Job
  ARR_CAT : task_arrivals_up_to_job_arrival arr_seq j1 ++ xs =
            task_arrivals_up_to_job_arrival arr_seq j2
  ============================
  j1 \in task_arrivals_up_to_job_arrival arr_seq j1 \/ j1 \in xs

subgoal 2 (ID 117) is:
 j2 \in task_arrivals_up_to_job_arrival arr_seq j2

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

        now left; apply arrives_in_task_arrivals_up_to.

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

1 subgoal (ID 117)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j1, j2 : Job
  H_j1_from_arrival_sequence : arrives_in arr_seq j1
  H_j2_from_arrival_sequence : arrives_in arr_seq j2
  H_same_task : job_task j1 = job_task j2
  H_equal_index, IND : job_index arr_seq j1 = job_index arr_seq j2
  xs : seq Job
  ARR_CAT : task_arrivals_up_to_job_arrival arr_seq j1 ++ xs =
            task_arrivals_up_to_job_arrival arr_seq j2
  ============================
  j2 \in task_arrivals_up_to_job_arrival arr_seq j2

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

      - now apply arrives_in_task_arrivals_up_to.

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

No more subgoals.

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

    Qed.

And similarly if [j1] arrives after [j2], we show that the jobs are equal.
    Lemma case_arrival_gt_implies_equal_job:
      job_arrival j1 > job_arrival j2 → j1 = j2.

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

1 subgoal (ID 68)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j1, j2 : Job
  H_j1_from_arrival_sequence : arrives_in arr_seq j1
  H_j2_from_arrival_sequence : arrives_in arr_seq j2
  H_same_task : job_task j1 = job_task j2
  H_equal_index : job_index arr_seq j1 = job_index arr_seq j2
  ============================
  job_arrival j2 < job_arrival j1 -> j1 = j2

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

    Proof.
      move⇒ LT.

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

1 subgoal (ID 69)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j1, j2 : Job
  H_j1_from_arrival_sequence : arrives_in arr_seq j1
  H_j2_from_arrival_sequence : arrives_in arr_seq j2
  H_same_task : job_task j1 = job_task j2
  H_equal_index : job_index arr_seq j1 = job_index arr_seq j2
  LT : job_arrival j2 < job_arrival j1
  ============================
  j1 = j2

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

      move: H_equal_index ⇒ IND.

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

1 subgoal (ID 71)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j1, j2 : Job
  H_j1_from_arrival_sequence : arrives_in arr_seq j1
  H_j2_from_arrival_sequence : arrives_in arr_seq j2
  H_same_task : job_task j1 = job_task j2
  H_equal_index : job_index arr_seq j1 = job_index arr_seq j2
  LT : job_arrival j2 < job_arrival j1
  IND : job_index arr_seq j1 = job_index arr_seq j2
  ============================
  j1 = j2

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

      apply ltnW, (task_arrivals_up_to_prefix_cat arr_seq) in LT ⇒ //.

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

1 subgoal (ID 78)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j1, j2 : Job
  H_j1_from_arrival_sequence : arrives_in arr_seq j1
  H_j2_from_arrival_sequence : arrives_in arr_seq j2
  H_same_task : job_task j1 = job_task j2
  H_equal_index : job_index arr_seq j1 = job_index arr_seq j2
  LT : prefix Job (task_arrivals_up_to_job_arrival arr_seq j2)
         (task_arrivals_up_to_job_arrival arr_seq j1)
  IND : job_index arr_seq j1 = job_index arr_seq j2
  ============================
  j1 = j2

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

      move: LT ⇒ [xs ARR_CAT].

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

1 subgoal (ID 136)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j1, j2 : Job
  H_j1_from_arrival_sequence : arrives_in arr_seq j1
  H_j2_from_arrival_sequence : arrives_in arr_seq j2
  H_same_task : job_task j1 = job_task j2
  H_equal_index, IND : job_index arr_seq j1 = job_index arr_seq j2
  xs : seq Job
  ARR_CAT : task_arrivals_up_to_job_arrival arr_seq j2 ++ xs =
            task_arrivals_up_to_job_arrival arr_seq j1
  ============================
  j1 = j2

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

      apply (eq_ind_in_seq _ _ _ (task_arrivals_up_to_job_arrival arr_seq j1)) ⇒ //.

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

4 subgoals (ID 147)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j1, j2 : Job
  H_j1_from_arrival_sequence : arrives_in arr_seq j1
  H_j2_from_arrival_sequence : arrives_in arr_seq j2
  H_same_task : job_task j1 = job_task j2
  H_equal_index, IND : job_index arr_seq j1 = job_index arr_seq j2
  xs : seq Job
  ARR_CAT : task_arrivals_up_to_job_arrival arr_seq j2 ++ xs =
            task_arrivals_up_to_job_arrival arr_seq j1
  ============================
  index j1 (task_arrivals_up_to_job_arrival arr_seq j1) =
  index j2 (task_arrivals_up_to_job_arrival arr_seq j1)

subgoal 2 (ID 148) is:
 uniq (task_arrivals_up_to_job_arrival arr_seq j1)
subgoal 3 (ID 149) is:
 j1 \in task_arrivals_up_to_job_arrival arr_seq j1
subgoal 4 (ID 150) is:
 j2 \in task_arrivals_up_to_job_arrival arr_seq j1

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

      - now rewrite -/(job_index _ _) IND -ARR_CAT index_cat ifT;
          try apply arrives_in_task_arrivals_up_to.

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

3 subgoals (ID 148)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j1, j2 : Job
  H_j1_from_arrival_sequence : arrives_in arr_seq j1
  H_j2_from_arrival_sequence : arrives_in arr_seq j2
  H_same_task : job_task j1 = job_task j2
  H_equal_index, IND : job_index arr_seq j1 = job_index arr_seq j2
  xs : seq Job
  ARR_CAT : task_arrivals_up_to_job_arrival arr_seq j2 ++ xs =
            task_arrivals_up_to_job_arrival arr_seq j1
  ============================
  uniq (task_arrivals_up_to_job_arrival arr_seq j1)

subgoal 2 (ID 149) is:
 j1 \in task_arrivals_up_to_job_arrival arr_seq j1
subgoal 3 (ID 150) is:
 j2 \in task_arrivals_up_to_job_arrival arr_seq j1

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

      - now apply uniq_task_arrivals.

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

2 subgoals (ID 149)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j1, j2 : Job
  H_j1_from_arrival_sequence : arrives_in arr_seq j1
  H_j2_from_arrival_sequence : arrives_in arr_seq j2
  H_same_task : job_task j1 = job_task j2
  H_equal_index, IND : job_index arr_seq j1 = job_index arr_seq j2
  xs : seq Job
  ARR_CAT : task_arrivals_up_to_job_arrival arr_seq j2 ++ xs =
            task_arrivals_up_to_job_arrival arr_seq j1
  ============================
  j1 \in task_arrivals_up_to_job_arrival arr_seq j1

subgoal 2 (ID 150) is:
 j2 \in task_arrivals_up_to_job_arrival arr_seq j1

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

      - now apply arrives_in_task_arrivals_up_to.

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

1 subgoal (ID 150)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j1, j2 : Job
  H_j1_from_arrival_sequence : arrives_in arr_seq j1
  H_j2_from_arrival_sequence : arrives_in arr_seq j2
  H_same_task : job_task j1 = job_task j2
  H_equal_index, IND : job_index arr_seq j1 = job_index arr_seq j2
  xs : seq Job
  ARR_CAT : task_arrivals_up_to_job_arrival arr_seq j2 ++ xs =
            task_arrivals_up_to_job_arrival arr_seq j1
  ============================
  j2 \in task_arrivals_up_to_job_arrival arr_seq j1

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

      - rewrite -ARR_CAT mem_cat; apply /orP.

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

1 focused subgoal
(shelved: 1) (ID 327)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j1, j2 : Job
  H_j1_from_arrival_sequence : arrives_in arr_seq j1
  H_j2_from_arrival_sequence : arrives_in arr_seq j2
  H_same_task : job_task j1 = job_task j2
  H_equal_index, IND : job_index arr_seq j1 = job_index arr_seq j2
  xs : seq Job
  ARR_CAT : task_arrivals_up_to_job_arrival arr_seq j2 ++ xs =
            task_arrivals_up_to_job_arrival arr_seq j1
  ============================
  j2 \in task_arrivals_up_to_job_arrival arr_seq j2 \/ j2 \in xs

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

        now left; apply arrives_in_task_arrivals_up_to ⇒ //.

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

No more subgoals.

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

    Qed.

And finally we show that irrespective of the relation between the arrival of job [j1] and [j2], [j1] must be equal to [j2].
    Lemma equal_index_implies_equal_jobs:
      j1 = j2.

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

1 subgoal (ID 71)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j1, j2 : Job
  H_j1_from_arrival_sequence : arrives_in arr_seq j1
  H_j2_from_arrival_sequence : arrives_in arr_seq j2
  H_same_task : job_task j1 = job_task j2
  H_equal_index : job_index arr_seq j1 = job_index arr_seq j2
  ============================
  j1 = j2

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

    Proof.
      case: (ltngtP (job_arrival j1) (job_arrival j2)) ⇒ [LT|GT|EQ].

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

3 subgoals (ID 137)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j1, j2 : Job
  H_j1_from_arrival_sequence : arrives_in arr_seq j1
  H_j2_from_arrival_sequence : arrives_in arr_seq j2
  H_same_task : job_task j1 = job_task j2
  H_equal_index : job_index arr_seq j1 = job_index arr_seq j2
  LT : job_arrival j1 < job_arrival j2
  ============================
  j1 = j2

subgoal 2 (ID 138) is:
 j1 = j2
subgoal 3 (ID 139) is:
 j1 = j2

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

      - now apply case_arrival_lte_implies_equal_job; ssrlia.

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

2 subgoals (ID 138)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j1, j2 : Job
  H_j1_from_arrival_sequence : arrives_in arr_seq j1
  H_j2_from_arrival_sequence : arrives_in arr_seq j2
  H_same_task : job_task j1 = job_task j2
  H_equal_index : job_index arr_seq j1 = job_index arr_seq j2
  GT : job_arrival j2 < job_arrival j1
  ============================
  j1 = j2

subgoal 2 (ID 139) is:
 j1 = j2

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

      - now apply case_arrival_gt_implies_equal_job; ssrlia.

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

1 subgoal (ID 139)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j1, j2 : Job
  H_j1_from_arrival_sequence : arrives_in arr_seq j1
  H_j2_from_arrival_sequence : arrives_in arr_seq j2
  H_same_task : job_task j1 = job_task j2
  H_equal_index : job_index arr_seq j1 = job_index arr_seq j2
  EQ : job_arrival j1 = job_arrival j2
  ============================
  j1 = j2

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

      - now apply case_arrival_lte_implies_equal_job; ssrlia.

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

No more subgoals.

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

    Qed.

  End EqualJobIndex.

We show that jobs of a task are different if and only if they have different indices.
  Lemma diff_jobs_iff_diff_indices:
    j1 ≠ j2 ↔
    job_index arr_seq j1 ≠ job_index arr_seq j2.

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

1 subgoal (ID 57)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j1, j2 : Job
  H_j1_from_arrival_sequence : arrives_in arr_seq j1
  H_j2_from_arrival_sequence : arrives_in arr_seq j2
  H_same_task : job_task j1 = job_task j2
  ============================
  j1 <> j2 <-> job_index arr_seq j1 <> job_index arr_seq j2

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

  Proof.
    split.

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

2 subgoals (ID 59)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j1, j2 : Job
  H_j1_from_arrival_sequence : arrives_in arr_seq j1
  H_j2_from_arrival_sequence : arrives_in arr_seq j2
  H_same_task : job_task j1 = job_task j2
  ============================
  j1 <> j2 -> job_index arr_seq j1 <> job_index arr_seq j2

subgoal 2 (ID 60) is:
 job_index arr_seq j1 <> job_index arr_seq j2 -> j1 <> j2

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

    + move ⇒ NEQJ EQ.

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

2 subgoals (ID 63)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j1, j2 : Job
  H_j1_from_arrival_sequence : arrives_in arr_seq j1
  H_j2_from_arrival_sequence : arrives_in arr_seq j2
  H_same_task : job_task j1 = job_task j2
  NEQJ : j1 <> j2
  EQ : job_index arr_seq j1 = job_index arr_seq j2
  ============================
  False

subgoal 2 (ID 60) is:
 job_index arr_seq j1 <> job_index arr_seq j2 -> j1 <> j2

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

      now apply equal_index_implies_equal_jobs in EQ.

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

1 subgoal (ID 60)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j1, j2 : Job
  H_j1_from_arrival_sequence : arrives_in arr_seq j1
  H_j2_from_arrival_sequence : arrives_in arr_seq j2
  H_same_task : job_task j1 = job_task j2
  ============================
  job_index arr_seq j1 <> job_index arr_seq j2 -> j1 <> j2

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

    + move ⇒ NEQ EQ.

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

1 subgoal (ID 68)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j1, j2 : Job
  H_j1_from_arrival_sequence : arrives_in arr_seq j1
  H_j2_from_arrival_sequence : arrives_in arr_seq j2
  H_same_task : job_task j1 = job_task j2
  NEQ : job_index arr_seq j1 <> job_index arr_seq j2
  EQ : j1 = j2
  ============================
  False

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

      now move: EQ NEQ ⇒ →.

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

No more subgoals.

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

  Qed.

We show that [job_index j] can be written as a sum of [size (task_arrivals_before_job_arrival j)] and [index j (task_arrivals_at arr_seq (job_task j) (job_arrival j))].
  Lemma index_as_sum_size_and_index:
    job_index arr_seq j1 =
    size (task_arrivals_before_job_arrival arr_seq j1)
    + index j1 (task_arrivals_at_job_arrival arr_seq j1).

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

1 subgoal (ID 74)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j1, j2 : Job
  H_j1_from_arrival_sequence : arrives_in arr_seq j1
  H_j2_from_arrival_sequence : arrives_in arr_seq j2
  H_same_task : job_task j1 = job_task j2
  ============================
  job_index arr_seq j1 =
  size (task_arrivals_before_job_arrival arr_seq j1) +
  index j1 (task_arrivals_at_job_arrival arr_seq j1)

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

  Proof.
    rewrite /task_arrivals_at_job_arrival /job_index task_arrivals_up_to_cat //.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 105)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j1, j2 : Job
  H_j1_from_arrival_sequence : arrives_in arr_seq j1
  H_j2_from_arrival_sequence : arrives_in arr_seq j2
  H_same_task : job_task j1 = job_task j2
  ============================
  index j1
    (task_arrivals_before_job_arrival arr_seq j1 ++
     task_arrivals_at_job_arrival arr_seq j1) =
  size (task_arrivals_before_job_arrival arr_seq j1) +
  index j1 (task_arrivals_at arr_seq (job_task j1) (job_arrival j1))

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


    rewrite index_cat ifF; first by reflexivity.

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

1 subgoal (ID 142)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j1, j2 : Job
  H_j1_from_arrival_sequence : arrives_in arr_seq j1
  H_j2_from_arrival_sequence : arrives_in arr_seq j2
  H_same_task : job_task j1 = job_task j2
  ============================
  (j1 \in task_arrivals_before_job_arrival arr_seq j1) = false

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

    apply Bool.not_true_is_false; intro T.

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

1 subgoal (ID 146)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j1, j2 : Job
  H_j1_from_arrival_sequence : arrives_in arr_seq j1
  H_j2_from_arrival_sequence : arrives_in arr_seq j2
  H_same_task : job_task j1 = job_task j2
  T : (j1 \in task_arrivals_before_job_arrival arr_seq j1) = true
  ============================
  False

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

    move : T; rewrite mem_filter ⇒ /andP [/eqP SM_TSK JB_IN_ARR].

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

1 subgoal (ID 226)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j1, j2 : Job
  H_j1_from_arrival_sequence : arrives_in arr_seq j1
  H_j2_from_arrival_sequence : arrives_in arr_seq j2
  H_same_task : job_task j1 = job_task j2
  SM_TSK : job_task j1 = job_task j1
  JB_IN_ARR : j1 \in arrivals_between arr_seq 0 (job_arrival j1)
  ============================
  False

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

    apply mem_bigcat_nat_exists in JB_IN_ARR; move : JB_IN_ARR ⇒ [ind [JB_IN IND_INTR]].
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 251)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j1, j2 : Job
  H_j1_from_arrival_sequence : arrives_in arr_seq j1
  H_j2_from_arrival_sequence : arrives_in arr_seq j2
  H_same_task : job_task j1 = job_task j2
  SM_TSK : job_task j1 = job_task j1
  ind : nat
  JB_IN : j1 \in arrivals_at arr_seq ind
  IND_INTR : 0 <= ind < job_arrival j1
  ============================
  False

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

    erewrite H_consistent_arrivals in IND_INTR; eauto 2.

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

1 subgoal (ID 423)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j1, j2 : Job
  H_j1_from_arrival_sequence : arrives_in arr_seq j1
  H_j2_from_arrival_sequence : arrives_in arr_seq j2
  H_same_task : job_task j1 = job_task j2
  SM_TSK : job_task j1 = job_task j1
  ind : nat
  JB_IN : j1 \in arrivals_at arr_seq ind
  IND_INTR : 0 <= ind < ind
  ============================
  False

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

    now ssrlia.

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

No more subgoals.

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

  Qed.

Given jobs [j1] and [j2] in [arrivals_between_P arr_seq P t1 t2], the fact that [j2] arrives strictly before [j1] implies that [j2] also belongs in the sequence [arrivals_between_P arr_seq P t1 (job_arrival j1)].
  Lemma arrival_lt_implies_job_in_arrivals_between_P:
    ∀ (P : Job → bool) (t1 t2 : instant),
      (j1 \in arrivals_between_P arr_seq P t1 t2) →
      (j2 \in arrivals_between_P arr_seq P t1 t2) →
      job_arrival j2 < job_arrival j1 →
      j2 \in arrivals_between_P arr_seq P t1 (job_arrival j1).

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

1 subgoal (ID 96)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j1, j2 : Job
  H_j1_from_arrival_sequence : arrives_in arr_seq j1
  H_j2_from_arrival_sequence : arrives_in arr_seq j2
  H_same_task : job_task j1 = job_task j2
  ============================
  forall (P : Job -> bool) (t1 t2 : instant),
  j1 \in arrivals_between_P arr_seq P t1 t2 ->
  j2 \in arrivals_between_P arr_seq P t1 t2 ->
  job_arrival j2 < job_arrival j1 ->
  j2 \in arrivals_between_P arr_seq P t1 (job_arrival j1)

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

  Proof.
    intros × J1_IN J2_IN ARR_LT.

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

1 subgoal (ID 102)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j1, j2 : Job
  H_j1_from_arrival_sequence : arrives_in arr_seq j1
  H_j2_from_arrival_sequence : arrives_in arr_seq j2
  H_same_task : job_task j1 = job_task j2
  P : Job -> bool
  t1, t2 : instant
  J1_IN : j1 \in arrivals_between_P arr_seq P t1 t2
  J2_IN : j2 \in arrivals_between_P arr_seq P t1 t2
  ARR_LT : job_arrival j2 < job_arrival j1
  ============================
  j2 \in arrivals_between_P arr_seq P t1 (job_arrival j1)

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

    rewrite mem_filter in J2_IN; move : J2_IN ⇒ /andP [PJ2 J2ARR] ⇒ //.

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

1 subgoal (ID 175)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j1, j2 : Job
  H_j1_from_arrival_sequence : arrives_in arr_seq j1
  H_j2_from_arrival_sequence : arrives_in arr_seq j2
  H_same_task : job_task j1 = job_task j2
  P : Job -> bool
  t1, t2 : instant
  J1_IN : j1 \in arrivals_between_P arr_seq P t1 t2
  ARR_LT : job_arrival j2 < job_arrival j1
  PJ2 : P j2
  J2ARR : j2 \in arrivals_between arr_seq t1 t2
  ============================
  j2 \in arrivals_between_P arr_seq P t1 (job_arrival j1)

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

    rewrite mem_filter; apply /andP; split ⇒ //.

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

1 subgoal (ID 230)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j1, j2 : Job
  H_j1_from_arrival_sequence : arrives_in arr_seq j1
  H_j2_from_arrival_sequence : arrives_in arr_seq j2
  H_same_task : job_task j1 = job_task j2
  P : Job -> bool
  t1, t2 : instant
  J1_IN : j1 \in arrivals_between_P arr_seq P t1 t2
  ARR_LT : job_arrival j2 < job_arrival j1
  PJ2 : P j2
  J2ARR : j2 \in arrivals_between arr_seq t1 t2
  ============================
  j2 \in arrivals_between arr_seq t1 (job_arrival j1)

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

    apply mem_bigcat_nat_exists in J2ARR; move : J2ARR ⇒ [i [J2_IN INEQ]].

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

1 subgoal (ID 277)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j1, j2 : Job
  H_j1_from_arrival_sequence : arrives_in arr_seq j1
  H_j2_from_arrival_sequence : arrives_in arr_seq j2
  H_same_task : job_task j1 = job_task j2
  P : Job -> bool
  t1, t2 : instant
  J1_IN : j1 \in arrivals_between_P arr_seq P t1 t2
  ARR_LT : job_arrival j2 < job_arrival j1
  PJ2 : P j2
  i : nat
  J2_IN : j2 \in arrivals_at arr_seq i
  INEQ : t1 <= i < t2
  ============================
  j2 \in arrivals_between arr_seq t1 (job_arrival j1)

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

    apply mem_bigcat_nat with (j := i) ⇒ //.

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

1 subgoal (ID 278)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j1, j2 : Job
  H_j1_from_arrival_sequence : arrives_in arr_seq j1
  H_j2_from_arrival_sequence : arrives_in arr_seq j2
  H_same_task : job_task j1 = job_task j2
  P : Job -> bool
  t1, t2 : instant
  J1_IN : j1 \in arrivals_between_P arr_seq P t1 t2
  ARR_LT : job_arrival j2 < job_arrival j1
  PJ2 : P j2
  i : nat
  J2_IN : j2 \in arrivals_at arr_seq i
  INEQ : t1 <= i < t2
  ============================
  t1 <= i < job_arrival j1

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

    apply H_consistent_arrivals in J2_IN; rewrite J2_IN in ARR_LT.

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

1 subgoal (ID 333)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j1, j2 : Job
  H_j1_from_arrival_sequence : arrives_in arr_seq j1
  H_j2_from_arrival_sequence : arrives_in arr_seq j2
  H_same_task : job_task j1 = job_task j2
  P : Job -> bool
  t1, t2 : instant
  J1_IN : j1 \in arrivals_between_P arr_seq P t1 t2
  PJ2 : P j2
  i : nat
  J2_IN : job_arrival j2 = i
  INEQ : t1 <= i < t2
  ARR_LT : i < job_arrival j1
  ============================
  t1 <= i < job_arrival j1

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

    now ssrlia.

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

No more subgoals.

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

  Qed.

We show that jobs in the sequence [arrivals_between_P] are ordered by their arrival times, i.e., if index of a job [j2] is greater than or equal to index of any other job [j1] in the sequence, then [job_arrival j2] must be greater than or equal to [job_arrival j1].
  Lemma index_lte_implies_arrival_lte_P:
    ∀ (P : Job → bool) (t1 t2 : instant),
      (j1 \in arrivals_between_P arr_seq P t1 t2) →
      (j2 \in arrivals_between_P arr_seq P t1 t2) →
      index j1 (arrivals_between_P arr_seq P t1 t2) ≤ index j2 (arrivals_between_P arr_seq P t1 t2) →
      job_arrival j1 ≤ job_arrival j2.

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

1 subgoal (ID 115)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j1, j2 : Job
  H_j1_from_arrival_sequence : arrives_in arr_seq j1
  H_j2_from_arrival_sequence : arrives_in arr_seq j2
  H_same_task : job_task j1 = job_task j2
  ============================
  forall (P : Job -> bool) (t1 t2 : instant),
  j1 \in arrivals_between_P arr_seq P t1 t2 ->
  j2 \in arrivals_between_P arr_seq P t1 t2 ->
  index j1 (arrivals_between_P arr_seq P t1 t2) <=
  index j2 (arrivals_between_P arr_seq P t1 t2) ->
  job_arrival j1 <= job_arrival j2

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

  Proof.
    intros × IN1 IN2 LE.

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

1 subgoal (ID 121)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j1, j2 : Job
  H_j1_from_arrival_sequence : arrives_in arr_seq j1
  H_j2_from_arrival_sequence : arrives_in arr_seq j2
  H_same_task : job_task j1 = job_task j2
  P : Job -> bool
  t1, t2 : instant
  IN1 : j1 \in arrivals_between_P arr_seq P t1 t2
  IN2 : j2 \in arrivals_between_P arr_seq P t1 t2
  LE : index j1 (arrivals_between_P arr_seq P t1 t2) <=
       index j2 (arrivals_between_P arr_seq P t1 t2)
  ============================
  job_arrival j1 <= job_arrival j2

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

    move_neq_up LT; move_neq_down LE.

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

1 subgoal (ID 192)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j1, j2 : Job
  H_j1_from_arrival_sequence : arrives_in arr_seq j1
  H_j2_from_arrival_sequence : arrives_in arr_seq j2
  H_same_task : job_task j1 = job_task j2
  P : Job -> bool
  t1, t2 : instant
  IN1 : j1 \in arrivals_between_P arr_seq P t1 t2
  IN2 : j2 \in arrivals_between_P arr_seq P t1 t2
  LT : job_arrival j2 < job_arrival j1
  ============================
  index j2 (arrivals_between_P arr_seq P t1 t2) <
  index j1 (arrivals_between_P arr_seq P t1 t2)

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

    rewrite → arrivals_P_cat with (t := job_arrival j1); last by apply job_arrival_between in IN1 ⇒ //.

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

1 subgoal (ID 196)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j1, j2 : Job
  H_j1_from_arrival_sequence : arrives_in arr_seq j1
  H_j2_from_arrival_sequence : arrives_in arr_seq j2
  H_same_task : job_task j1 = job_task j2
  P : Job -> bool
  t1, t2 : instant
  IN1 : j1 \in arrivals_between_P arr_seq P t1 t2
  IN2 : j2 \in arrivals_between_P arr_seq P t1 t2
  LT : job_arrival j2 < job_arrival j1
  ============================
  index j2
    (arrivals_between_P arr_seq P t1 (job_arrival j1) ++
     arrivals_between_P arr_seq P (job_arrival j1) t2) <
  index j1
    (arrivals_between_P arr_seq P t1 (job_arrival j1) ++
     arrivals_between_P arr_seq P (job_arrival j1) t2)

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

    rewrite !index_cat ifT; last by eapply arrival_lt_implies_job_in_arrivals_between_P; eauto.

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

1 subgoal (ID 231)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j1, j2 : Job
  H_j1_from_arrival_sequence : arrives_in arr_seq j1
  H_j2_from_arrival_sequence : arrives_in arr_seq j2
  H_same_task : job_task j1 = job_task j2
  P : Job -> bool
  t1, t2 : instant
  IN1 : j1 \in arrivals_between_P arr_seq P t1 t2
  IN2 : j2 \in arrivals_between_P arr_seq P t1 t2
  LT : job_arrival j2 < job_arrival j1
  ============================
  index j2 (arrivals_between_P arr_seq P t1 (job_arrival j1)) <
  (if j1 \in arrivals_between_P arr_seq P t1 (job_arrival j1)
   then index j1 (arrivals_between_P arr_seq P t1 (job_arrival j1))
   else
    size (arrivals_between_P arr_seq P t1 (job_arrival j1)) +
    index j1 (arrivals_between_P arr_seq P (job_arrival j1) t2))

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

    rewrite ifF.

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

2 subgoals (ID 250)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j1, j2 : Job
  H_j1_from_arrival_sequence : arrives_in arr_seq j1
  H_j2_from_arrival_sequence : arrives_in arr_seq j2
  H_same_task : job_task j1 = job_task j2
  P : Job -> bool
  t1, t2 : instant
  IN1 : j1 \in arrivals_between_P arr_seq P t1 t2
  IN2 : j2 \in arrivals_between_P arr_seq P t1 t2
  LT : job_arrival j2 < job_arrival j1
  ============================
  index j2 (arrivals_between_P arr_seq P t1 (job_arrival j1)) <
  size (arrivals_between_P arr_seq P t1 (job_arrival j1)) +
  index j1 (arrivals_between_P arr_seq P (job_arrival j1) t2)

subgoal 2 (ID 251) is:
 (j1 \in arrivals_between_P arr_seq P t1 (job_arrival j1)) = false

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

    - eapply ltn_leq_trans; [ | now erewrite leq_addr].

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

2 subgoals (ID 253)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j1, j2 : Job
  H_j1_from_arrival_sequence : arrives_in arr_seq j1
  H_j2_from_arrival_sequence : arrives_in arr_seq j2
  H_same_task : job_task j1 = job_task j2
  P : Job -> bool
  t1, t2 : instant
  IN1 : j1 \in arrivals_between_P arr_seq P t1 t2
  IN2 : j2 \in arrivals_between_P arr_seq P t1 t2
  LT : job_arrival j2 < job_arrival j1
  ============================
  index j2 (arrivals_between_P arr_seq P t1 (job_arrival j1)) <
  size (arrivals_between_P arr_seq P t1 (job_arrival j1))

subgoal 2 (ID 251) is:
 (j1 \in arrivals_between_P arr_seq P t1 (job_arrival j1)) = false

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

      rewrite index_mem.

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

2 subgoals (ID 466)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j1, j2 : Job
  H_j1_from_arrival_sequence : arrives_in arr_seq j1
  H_j2_from_arrival_sequence : arrives_in arr_seq j2
  H_same_task : job_task j1 = job_task j2
  P : Job -> bool
  t1, t2 : instant
  IN1 : j1 \in arrivals_between_P arr_seq P t1 t2
  IN2 : j2 \in arrivals_between_P arr_seq P t1 t2
  LT : job_arrival j2 < job_arrival j1
  ============================
  j2 \in arrivals_between_P arr_seq P t1 (job_arrival j1)

subgoal 2 (ID 251) is:
 (j1 \in arrivals_between_P arr_seq P t1 (job_arrival j1)) = false

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

      now eapply arrival_lt_implies_job_in_arrivals_between_P; eauto.

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

1 subgoal (ID 251)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j1, j2 : Job
  H_j1_from_arrival_sequence : arrives_in arr_seq j1
  H_j2_from_arrival_sequence : arrives_in arr_seq j2
  H_same_task : job_task j1 = job_task j2
  P : Job -> bool
  t1, t2 : instant
  IN1 : j1 \in arrivals_between_P arr_seq P t1 t2
  IN2 : j2 \in arrivals_between_P arr_seq P t1 t2
  LT : job_arrival j2 < job_arrival j1
  ============================
  (j1 \in arrivals_between_P arr_seq P t1 (job_arrival j1)) = false

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

    - apply Bool.not_true_is_false; intro T.

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

1 subgoal (ID 480)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j1, j2 : Job
  H_j1_from_arrival_sequence : arrives_in arr_seq j1
  H_j2_from_arrival_sequence : arrives_in arr_seq j2
  H_same_task : job_task j1 = job_task j2
  P : Job -> bool
  t1, t2 : instant
  IN1 : j1 \in arrivals_between_P arr_seq P t1 t2
  IN2 : j2 \in arrivals_between_P arr_seq P t1 t2
  LT : job_arrival j2 < job_arrival j1
  T : (j1 \in arrivals_between_P arr_seq P t1 (job_arrival j1)) = true
  ============================
  False

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

      now apply job_arrival_between in T; try ssrlia.

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

No more subgoals.

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

  Qed.

We observe that index of job [j1] is same in the sequences [task_arrivals_up_to_job_arrival j1] and [task_arrivals_up_to_job_arrival j2] provided [j2] arrives after [j1].
  Lemma job_index_same_in_task_arrivals:
    job_arrival j1 ≤ job_arrival j2 →
    index j1 (task_arrivals_up_to_job_arrival arr_seq j1) = index j1 (task_arrivals_up_to_job_arrival arr_seq j2).

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

1 subgoal (ID 132)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j1, j2 : Job
  H_j1_from_arrival_sequence : arrives_in arr_seq j1
  H_j2_from_arrival_sequence : arrives_in arr_seq j2
  H_same_task : job_task j1 = job_task j2
  ============================
  job_arrival j1 <= job_arrival j2 ->
  index j1 (task_arrivals_up_to_job_arrival arr_seq j1) =
  index j1 (task_arrivals_up_to_job_arrival arr_seq j2)

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

  Proof.
    rewrite leq_eqVlt ⇒ /orP [/eqP LT|LT]; first by rewrite /task_arrivals_up_to_job_arrival LT H_same_task.

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

1 subgoal (ID 212)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j1, j2 : Job
  H_j1_from_arrival_sequence : arrives_in arr_seq j1
  H_j2_from_arrival_sequence : arrives_in arr_seq j2
  H_same_task : job_task j1 = job_task j2
  LT : job_arrival j1 < job_arrival j2
  ============================
  index j1 (task_arrivals_up_to_job_arrival arr_seq j1) =
  index j1 (task_arrivals_up_to_job_arrival arr_seq j2)

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

    specialize (arrival_lt_implies_strict_prefix _ H_consistent_arrivals (job_task j1) j1 j2) ⇒ SUB.

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

1 subgoal (ID 237)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j1, j2 : Job
  H_j1_from_arrival_sequence : arrives_in arr_seq j1
  H_j2_from_arrival_sequence : arrives_in arr_seq j2
  H_same_task : job_task j1 = job_task j2
  LT : job_arrival j1 < job_arrival j2
  SUB : job_task j1 = job_task j1 ->
        job_task j2 = job_task j1 ->
        arrives_in arr_seq j1 ->
        arrives_in arr_seq j2 ->
        job_arrival j1 < job_arrival j2 ->
        strict_prefix Job (task_arrivals_up_to_job_arrival arr_seq j1)
          (task_arrivals_up_to_job_arrival arr_seq j2)
  ============================
  index j1 (task_arrivals_up_to_job_arrival arr_seq j1) =
  index j1 (task_arrivals_up_to_job_arrival arr_seq j2)

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

    feed_n 5 SUB ⇒ //; move: SUB ⇒ [xs2 [NEMPT2 CAT2]].

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

1 subgoal (ID 331)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j1, j2 : Job
  H_j1_from_arrival_sequence : arrives_in arr_seq j1
  H_j2_from_arrival_sequence : arrives_in arr_seq j2
  H_same_task : job_task j1 = job_task j2
  LT : job_arrival j1 < job_arrival j2
  xs2 : seq Job
  NEMPT2 : xs2 <> [::]
  CAT2 : task_arrivals_up_to_job_arrival arr_seq j1 ++ xs2 =
         task_arrivals_up_to_job_arrival arr_seq j2
  ============================
  index j1 (task_arrivals_up_to_job_arrival arr_seq j1) =
  index j1 (task_arrivals_up_to_job_arrival arr_seq j2)

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

    now rewrite -CAT2 index_cat ifT; last by apply arrives_in_task_arrivals_up_to ⇒ //.

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

No more subgoals.

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

  Qed.

We show that the [job_index] of a job [j1] is strictly less than the size of [task_arrivals_up_to_job_arrival arr_seq j1].
  Lemma index_job_lt_size_task_arrivals_up_to_job:
    job_index arr_seq j1 < size (task_arrivals_up_to_job_arrival arr_seq j1).

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

1 subgoal (ID 142)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j1, j2 : Job
  H_j1_from_arrival_sequence : arrives_in arr_seq j1
  H_j2_from_arrival_sequence : arrives_in arr_seq j2
  H_same_task : job_task j1 = job_task j2
  ============================
  job_index arr_seq j1 < size (task_arrivals_up_to_job_arrival arr_seq j1)

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

  Proof.
    rewrite /job_index index_mem.

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

1 subgoal (ID 156)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j1, j2 : Job
  H_j1_from_arrival_sequence : arrives_in arr_seq j1
  H_j2_from_arrival_sequence : arrives_in arr_seq j2
  H_same_task : job_task j1 = job_task j2
  ============================
  j1 \in task_arrivals_up_to_job_arrival arr_seq j1

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

    now apply arrives_in_task_arrivals_up_to.

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

No more subgoals.

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

  Qed.

Finally, we show that a lower job index implies an earlier arrival time.
  Lemma index_lte_implies_arrival_lte:
    job_index arr_seq j2 ≤ job_index arr_seq j1 →
    job_arrival j2 ≤ job_arrival j1.

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

1 subgoal (ID 155)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j1, j2 : Job
  H_j1_from_arrival_sequence : arrives_in arr_seq j1
  H_j2_from_arrival_sequence : arrives_in arr_seq j2
  H_same_task : job_task j1 = job_task j2
  ============================
  job_index arr_seq j2 <= job_index arr_seq j1 ->
  job_arrival j2 <= job_arrival j1

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

  Proof.
    intros IND_LT.

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

1 subgoal (ID 156)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j1, j2 : Job
  H_j1_from_arrival_sequence : arrives_in arr_seq j1
  H_j2_from_arrival_sequence : arrives_in arr_seq j2
  H_same_task : job_task j1 = job_task j2
  IND_LT : job_index arr_seq j2 <= job_index arr_seq j1
  ============================
  job_arrival j2 <= job_arrival j1

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

    rewrite /job_index in IND_LT.

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

1 subgoal (ID 185)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j1, j2 : Job
  H_j1_from_arrival_sequence : arrives_in arr_seq j1
  H_j2_from_arrival_sequence : arrives_in arr_seq j2
  H_same_task : job_task j1 = job_task j2
  IND_LT : index j2 (task_arrivals_up_to_job_arrival arr_seq j2) <=
           index j1 (task_arrivals_up_to_job_arrival arr_seq j1)
  ============================
  job_arrival j2 <= job_arrival j1

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

    move_neq_up ARR_GT; move_neq_down IND_LT.

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

1 subgoal (ID 256)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j1, j2 : Job
  H_j1_from_arrival_sequence : arrives_in arr_seq j1
  H_j2_from_arrival_sequence : arrives_in arr_seq j2
  H_same_task : job_task j1 = job_task j2
  ARR_GT : job_arrival j1 < job_arrival j2
  ============================
  index j1 (task_arrivals_up_to_job_arrival arr_seq j1) <
  index j2 (task_arrivals_up_to_job_arrival arr_seq j2)

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

    rewrite job_index_same_in_task_arrivals /task_arrivals_up_to_job_arrival; try by ssrlia.

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

1 subgoal (ID 269)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j1, j2 : Job
  H_j1_from_arrival_sequence : arrives_in arr_seq j1
  H_j2_from_arrival_sequence : arrives_in arr_seq j2
  H_same_task : job_task j1 = job_task j2
  ARR_GT : job_arrival j1 < job_arrival j2
  ============================
  index j1 (task_arrivals_up_to arr_seq (job_task j2) (job_arrival j2)) <
  index j2 (task_arrivals_up_to arr_seq (job_task j2) (job_arrival j2))

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

    rewrite → task_arrivals_cat with (t_m := job_arrival j1); try by ssrlia.

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

1 subgoal (ID 552)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j1, j2 : Job
  H_j1_from_arrival_sequence : arrives_in arr_seq j1
  H_j2_from_arrival_sequence : arrives_in arr_seq j2
  H_same_task : job_task j1 = job_task j2
  ARR_GT : job_arrival j1 < job_arrival j2
  ============================
  index j1
    (task_arrivals_up_to arr_seq (job_task j2) (job_arrival j1) ++
     task_arrivals_between arr_seq (job_task j2) (job_arrival j1).+1
       (job_arrival j2).+1) <
  index j2
    (task_arrivals_up_to arr_seq (job_task j2) (job_arrival j1) ++
     task_arrivals_between arr_seq (job_task j2) (job_arrival j1).+1
       (job_arrival j2).+1)

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

    rewrite -H_same_task !index_cat ifT; try by apply arrives_in_task_arrivals_up_to.

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

1 subgoal (ID 856)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j1, j2 : Job
  H_j1_from_arrival_sequence : arrives_in arr_seq j1
  H_j2_from_arrival_sequence : arrives_in arr_seq j2
  H_same_task : job_task j1 = job_task j2
  ARR_GT : job_arrival j1 < job_arrival j2
  ============================
  index j1 (task_arrivals_up_to arr_seq (job_task j1) (job_arrival j1)) <
  (if j2 \in task_arrivals_up_to arr_seq (job_task j1) (job_arrival j1)
   then index j2 (task_arrivals_up_to arr_seq (job_task j1) (job_arrival j1))
   else
    size (task_arrivals_up_to arr_seq (job_task j1) (job_arrival j1)) +
    index j2
      (task_arrivals_between arr_seq (job_task j1) 
         (job_arrival j1).+1 (job_arrival j2).+1))

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

    rewrite ifF.

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

2 subgoals (ID 874)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j1, j2 : Job
  H_j1_from_arrival_sequence : arrives_in arr_seq j1
  H_j2_from_arrival_sequence : arrives_in arr_seq j2
  H_same_task : job_task j1 = job_task j2
  ARR_GT : job_arrival j1 < job_arrival j2
  ============================
  index j1 (task_arrivals_up_to arr_seq (job_task j1) (job_arrival j1)) <
  size (task_arrivals_up_to arr_seq (job_task j1) (job_arrival j1)) +
  index j2
    (task_arrivals_between arr_seq (job_task j1) (job_arrival j1).+1
       (job_arrival j2).+1)

subgoal 2 (ID 875) is:
 (j2 \in task_arrivals_up_to arr_seq (job_task j1) (job_arrival j1)) = false

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

    - now eapply ltn_leq_trans;
        [apply index_job_lt_size_task_arrivals_up_to_job | rewrite leq_addr].

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

1 subgoal (ID 875)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j1, j2 : Job
  H_j1_from_arrival_sequence : arrives_in arr_seq j1
  H_j2_from_arrival_sequence : arrives_in arr_seq j2
  H_same_task : job_task j1 = job_task j2
  ARR_GT : job_arrival j1 < job_arrival j2
  ============================
  (j2 \in task_arrivals_up_to arr_seq (job_task j1) (job_arrival j1)) = false

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

    - apply Bool.not_true_is_false; intro T.

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

1 subgoal (ID 885)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j1, j2 : Job
  H_j1_from_arrival_sequence : arrives_in arr_seq j1
  H_j2_from_arrival_sequence : arrives_in arr_seq j2
  H_same_task : job_task j1 = job_task j2
  ARR_GT : job_arrival j1 < job_arrival j2
  T : (j2 \in task_arrivals_up_to arr_seq (job_task j1) (job_arrival j1)) =
      true
  ============================
  False

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

      now apply job_arrival_between in T; try ssrlia.

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

No more subgoals.

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

  Qed.

We show that if job [j1] arrives earlier than job [j2] then [job_index arr_seq j1] is strictly less than [job_index arr_seq j2].
  Lemma earlier_arrival_implies_lower_index:
    job_arrival j1 < job_arrival j2 →
    job_index arr_seq j1 < job_index arr_seq j2.

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

1 subgoal (ID 168)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j1, j2 : Job
  H_j1_from_arrival_sequence : arrives_in arr_seq j1
  H_j2_from_arrival_sequence : arrives_in arr_seq j2
  H_same_task : job_task j1 = job_task j2
  ============================
  job_arrival j1 < job_arrival j2 ->
  job_index arr_seq j1 < job_index arr_seq j2

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

  Proof.
    intros ARR_LT.

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

1 subgoal (ID 169)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j1, j2 : Job
  H_j1_from_arrival_sequence : arrives_in arr_seq j1
  H_j2_from_arrival_sequence : arrives_in arr_seq j2
  H_same_task : job_task j1 = job_task j2
  ARR_LT : job_arrival j1 < job_arrival j2
  ============================
  job_index arr_seq j1 < job_index arr_seq j2

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

    move_neq_up IND_LT; move_neq_down ARR_LT.

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

1 subgoal (ID 234)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j1, j2 : Job
  H_j1_from_arrival_sequence : arrives_in arr_seq j1
  H_j2_from_arrival_sequence : arrives_in arr_seq j2
  H_same_task : job_task j1 = job_task j2
  IND_LT : job_index arr_seq j2 <= job_index arr_seq j1
  ============================
  job_arrival j2 <= job_arrival j1

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

    now apply index_lte_implies_arrival_lte.

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

No more subgoals.

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

  Qed.

We prove a weaker version of the lemma [index_job_lt_size_task_arrivals_up_to_job], given that the [job_index] of [j] is positive.
  Lemma job_index_minus_one_lt_size_task_arrivals_up_to:
    job_index arr_seq j1 - 1 < size (task_arrivals_up_to_job_arrival arr_seq j1).

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

1 subgoal (ID 178)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j1, j2 : Job
  H_j1_from_arrival_sequence : arrives_in arr_seq j1
  H_j2_from_arrival_sequence : arrives_in arr_seq j2
  H_same_task : job_task j1 = job_task j2
  ============================
  job_index arr_seq j1 - 1 <
  size (task_arrivals_up_to_job_arrival arr_seq j1)

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

  Proof.
    apply leq_ltn_trans with (n := job_index arr_seq j1); try by ssrlia.

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

1 subgoal (ID 184)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j1, j2 : Job
  H_j1_from_arrival_sequence : arrives_in arr_seq j1
  H_j2_from_arrival_sequence : arrives_in arr_seq j2
  H_same_task : job_task j1 = job_task j2
  ============================
  job_index arr_seq j1 < size (task_arrivals_up_to_job_arrival arr_seq j1)

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

    now apply index_job_lt_size_task_arrivals_up_to_job.

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

No more subgoals.

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

  Qed.

Since [task_arrivals_up_to_job_arrival arr_seq j] has at least the job [j] in it, its size has to be positive.
  Lemma positive_job_index_implies_positive_size_of_task_arrivals:
    size (task_arrivals_up_to_job_arrival arr_seq j1) > 0.

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

1 subgoal (ID 184)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j1, j2 : Job
  H_j1_from_arrival_sequence : arrives_in arr_seq j1
  H_j2_from_arrival_sequence : arrives_in arr_seq j2
  H_same_task : job_task j1 = job_task j2
  ============================
  0 < size (task_arrivals_up_to_job_arrival arr_seq j1)

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

  Proof.
    rewrite lt0n; apply /eqP; intro Z.

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

1 subgoal (ID 227)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j1, j2 : Job
  H_j1_from_arrival_sequence : arrives_in arr_seq j1
  H_j2_from_arrival_sequence : arrives_in arr_seq j2
  H_same_task : job_task j1 = job_task j2
  Z : size (task_arrivals_up_to_job_arrival arr_seq j1) = 0
  ============================
  False

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

    apply size0nil in Z.

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

1 subgoal (ID 228)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j1, j2 : Job
  H_j1_from_arrival_sequence : arrives_in arr_seq j1
  H_j2_from_arrival_sequence : arrives_in arr_seq j2
  H_same_task : job_task j1 = job_task j2
  Z : task_arrivals_up_to_job_arrival arr_seq j1 = [::]
  ============================
  False

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

    have J_IN : (j1 \in task_arrivals_up_to_job_arrival arr_seq j1)
      by apply arrives_in_task_arrivals_up_to ⇒ //.

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

1 subgoal (ID 246)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j1, j2 : Job
  H_j1_from_arrival_sequence : arrives_in arr_seq j1
  H_j2_from_arrival_sequence : arrives_in arr_seq j2
  H_same_task : job_task j1 = job_task j2
  Z : task_arrivals_up_to_job_arrival arr_seq j1 = [::]
  J_IN : j1 \in task_arrivals_up_to_job_arrival arr_seq j1
  ============================
  False

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

    now rewrite Z in J_IN.

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

No more subgoals.

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

  Qed.

End JobIndexLemmas.

In this section, we prove a few basic properties of function [prev_job].
Section PreviousJob.

Consider any type of tasks ...
  Context {Task : TaskType}.

... and any jobs associated with the tasks.
  Context {Job : JobType}.
  Context `{JobTask Job Task}.
  Context `{JobArrival Job}.

Consider any unique arrival sequence with consistent arrivals ...
  Variable arr_seq : arrival_sequence Job.
  Hypothesis H_consistent_arrivals : consistent_arrival_times arr_seq.
  Hypothesis H_uniq_arr_seq : arrival_sequence_uniq arr_seq.

... and an arbitrary job with a positive [job_index].
  Variable j : Job.
  Hypothesis H_arrives_in_arr_seq: arrives_in arr_seq j.
  Hypothesis H_positive_job_index: job_index arr_seq j > 0.

We observe that the fact that job [j] is in the arrival sequence implies that job [prev_job j] is in the arrival sequence.
  Lemma prev_job_arr:
    arrives_in arr_seq (prev_job arr_seq j).

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

1 subgoal (ID 45)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j : Job
  H_arrives_in_arr_seq : arrives_in arr_seq j
  H_positive_job_index : 0 < job_index arr_seq j
  ============================
  arrives_in arr_seq (prev_job arr_seq j)

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

  Proof.
    destruct (default_or_in _ (job_index arr_seq j - 1) j (task_arrivals_up_to_job_arrival arr_seq j)) as [EQ|IN].

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

2 subgoals (ID 62)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j : Job
  H_arrives_in_arr_seq : arrives_in arr_seq j
  H_positive_job_index : 0 < job_index arr_seq j
  EQ : nth j (task_arrivals_up_to_job_arrival arr_seq j)
         (job_index arr_seq j - 1) = j
  ============================
  arrives_in arr_seq (prev_job arr_seq j)

subgoal 2 (ID 63) is:
 arrives_in arr_seq (prev_job arr_seq j)

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

    + now rewrite /prev_job EQ.

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

1 subgoal (ID 63)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j : Job
  H_arrives_in_arr_seq : arrives_in arr_seq j
  H_positive_job_index : 0 < job_index arr_seq j
  IN : nth j (task_arrivals_up_to_job_arrival arr_seq j)
         (job_index arr_seq j - 1)
         \in task_arrivals_up_to_job_arrival arr_seq j
  ============================
  arrives_in arr_seq (prev_job arr_seq j)

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

    + apply in_arrivals_implies_arrived with (t1 := 0) (t2 := (job_arrival j).+1).

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

1 subgoal (ID 78)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j : Job
  H_arrives_in_arr_seq : arrives_in arr_seq j
  H_positive_job_index : 0 < job_index arr_seq j
  IN : nth j (task_arrivals_up_to_job_arrival arr_seq j)
         (job_index arr_seq j - 1)
         \in task_arrivals_up_to_job_arrival arr_seq j
  ============================
  prev_job arr_seq j \in arrivals_between arr_seq 0 (job_arrival j).+1

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

       now move: IN; rewrite mem_filter ⇒ /andP [_ IN].

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

No more subgoals.

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

  Qed.

We show that the index of [prev_job j] in task arrivals up to [j] is one less than [job_index arr_seq j].
  Lemma prev_job_index:
    index (prev_job arr_seq j) (task_arrivals_up_to_job_arrival arr_seq j) = job_index arr_seq j - 1.

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

1 subgoal (ID 61)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j : Job
  H_arrives_in_arr_seq : arrives_in arr_seq j
  H_positive_job_index : 0 < job_index arr_seq j
  ============================
  index (prev_job arr_seq j) (task_arrivals_up_to_job_arrival arr_seq j) =
  job_index arr_seq j - 1

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

  Proof.
    apply index_uniq; last by apply uniq_task_arrivals.

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

1 subgoal (ID 62)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j : Job
  H_arrives_in_arr_seq : arrives_in arr_seq j
  H_positive_job_index : 0 < job_index arr_seq j
  ============================
  job_index arr_seq j - 1 < size (task_arrivals_up_to_job_arrival arr_seq j)

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

    apply leq_ltn_trans with (n := job_index arr_seq j); try by ssrlia.

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

1 subgoal (ID 75)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j : Job
  H_arrives_in_arr_seq : arrives_in arr_seq j
  H_positive_job_index : 0 < job_index arr_seq j
  ============================
  job_index arr_seq j < size (task_arrivals_up_to_job_arrival arr_seq j)

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

    now apply index_job_lt_size_task_arrivals_up_to_job.

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

No more subgoals.

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

  Qed.

Observe that job [j] and [prev_job j] stem from the same task.
  Lemma prev_job_task:
    job_task (prev_job arr_seq j) = job_task j.

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

1 subgoal (ID 74)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j : Job
  H_arrives_in_arr_seq : arrives_in arr_seq j
  H_positive_job_index : 0 < job_index arr_seq j
  ============================
  job_task (prev_job arr_seq j) = job_task j

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

  Proof.
    specialize (job_index_minus_one_lt_size_task_arrivals_up_to arr_seq H_consistent_arrivals j H_arrives_in_arr_seq) ⇒ SIZEL.

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

1 subgoal (ID 81)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j : Job
  H_arrives_in_arr_seq : arrives_in arr_seq j
  H_positive_job_index : 0 < job_index arr_seq j
  SIZEL : job_index arr_seq j - 1 <
          size (task_arrivals_up_to_job_arrival arr_seq j)
  ============================
  job_task (prev_job arr_seq j) = job_task j

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

    rewrite -prev_job_index index_mem mem_filter in SIZEL.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 112)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j : Job
  H_arrives_in_arr_seq : arrives_in arr_seq j
  H_positive_job_index : 0 < job_index arr_seq j
  SIZEL : (job_task (prev_job arr_seq j) == job_task j) &&
          (prev_job arr_seq j
             \in arrivals_between arr_seq 0 (job_arrival j).+1)
  ============================
  job_task (prev_job arr_seq j) = job_task j

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

    now move : SIZEL ⇒ /andP [/eqP TSK PREV_IN].

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

No more subgoals.

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

  Qed.

We show that [prev_job arr_seq j] belongs in [task_arrivals_up_to_job_arrival arr_seq j].
  Lemma prev_job_in_task_arrivals_up_to_j:
    prev_job arr_seq j \in task_arrivals_up_to_job_arrival arr_seq j.

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

1 subgoal (ID 87)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j : Job
  H_arrives_in_arr_seq : arrives_in arr_seq j
  H_positive_job_index : 0 < job_index arr_seq j
  ============================
  prev_job arr_seq j \in task_arrivals_up_to_job_arrival arr_seq j

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

  Proof.
    rewrite /prev_job -index_mem index_uniq;
      try by apply job_index_minus_one_lt_size_task_arrivals_up_to.

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

1 subgoal (ID 111)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j : Job
  H_arrives_in_arr_seq : arrives_in arr_seq j
  H_positive_job_index : 0 < job_index arr_seq j
  ============================
  uniq (task_arrivals_up_to_job_arrival arr_seq j)

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

    now apply uniq_task_arrivals.

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

No more subgoals.

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

  Qed.

We observe that for any job [j] the arrival time of [prev_job j] is strictly less than the arrival time of [j] in context of periodic tasks.
  Lemma prev_job_arr_lte:
    job_arrival (prev_job arr_seq j) ≤ job_arrival j.

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

1 subgoal (ID 96)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j : Job
  H_arrives_in_arr_seq : arrives_in arr_seq j
  H_positive_job_index : 0 < job_index arr_seq j
  ============================
  job_arrival (prev_job arr_seq j) <= job_arrival j

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

  Proof.
    move : (prev_job_in_task_arrivals_up_to_j) ⇒ PREV_JOB_IN.

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

1 subgoal (ID 98)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j : Job
  H_arrives_in_arr_seq : arrives_in arr_seq j
  H_positive_job_index : 0 < job_index arr_seq j
  PREV_JOB_IN : prev_job arr_seq j
                  \in task_arrivals_up_to_job_arrival arr_seq j
  ============================
  job_arrival (prev_job arr_seq j) <= job_arrival j

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

    rewrite mem_filter in PREV_JOB_IN; move : PREV_JOB_IN ⇒ /andP [TSK PREV_IN].

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

1 subgoal (ID 164)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j : Job
  H_arrives_in_arr_seq : arrives_in arr_seq j
  H_positive_job_index : 0 < job_index arr_seq j
  TSK : job_task (prev_job arr_seq j) == job_task j
  PREV_IN : prev_job arr_seq j
              \in arrivals_between arr_seq 0 (job_arrival j).+1
  ============================
  job_arrival (prev_job arr_seq j) <= job_arrival j

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

    apply mem_bigcat_nat_exists in PREV_IN; move : PREV_IN ⇒ [i [PREV_IN INEQ]].

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

1 subgoal (ID 189)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j : Job
  H_arrives_in_arr_seq : arrives_in arr_seq j
  H_positive_job_index : 0 < job_index arr_seq j
  TSK : job_task (prev_job arr_seq j) == job_task j
  i : nat
  PREV_IN : prev_job arr_seq j \in arrivals_at arr_seq i
  INEQ : 0 <= i < (job_arrival j).+1
  ============================
  job_arrival (prev_job arr_seq j) <= job_arrival j

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

    apply H_consistent_arrivals in PREV_IN; rewrite -PREV_IN in INEQ.

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

1 subgoal (ID 214)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j : Job
  H_arrives_in_arr_seq : arrives_in arr_seq j
  H_positive_job_index : 0 < job_index arr_seq j
  TSK : job_task (prev_job arr_seq j) == job_task j
  i : nat
  PREV_IN : job_arrival (prev_job arr_seq j) = i
  INEQ : 0 <= job_arrival (prev_job arr_seq j) < (job_arrival j).+1
  ============================
  job_arrival (prev_job arr_seq j) <= job_arrival j

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

    now ssrlia.

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

No more subgoals.

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

  Qed.

We show that for any job [j] the job index of [prev_job j] is one less than the job index of [j].
  Lemma prev_job_index_j:
    job_index arr_seq j > 0 →
    job_index arr_seq (prev_job arr_seq j) = job_index arr_seq j - 1.

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

1 subgoal (ID 115)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j : Job
  H_arrives_in_arr_seq : arrives_in arr_seq j
  H_positive_job_index : 0 < job_index arr_seq j
  ============================
  0 < job_index arr_seq j ->
  job_index arr_seq (prev_job arr_seq j) = job_index arr_seq j - 1

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

  Proof.
    intros NZ_IND.

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

1 subgoal (ID 116)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j : Job
  H_arrives_in_arr_seq : arrives_in arr_seq j
  H_positive_job_index, NZ_IND : 0 < job_index arr_seq j
  ============================
  job_index arr_seq (prev_job arr_seq j) = job_index arr_seq j - 1

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

    rewrite -prev_job_index.

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

1 subgoal (ID 118)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j : Job
  H_arrives_in_arr_seq : arrives_in arr_seq j
  H_positive_job_index, NZ_IND : 0 < job_index arr_seq j
  ============================
  job_index arr_seq (prev_job arr_seq j) =
  index (prev_job arr_seq j) (task_arrivals_up_to_job_arrival arr_seq j)

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

    apply job_index_same_in_task_arrivals ⇒ //.

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

3 subgoals (ID 124)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j : Job
  H_arrives_in_arr_seq : arrives_in arr_seq j
  H_positive_job_index, NZ_IND : 0 < job_index arr_seq j
  ============================
  arrives_in arr_seq (prev_job arr_seq j)

subgoal 2 (ID 126) is:
 job_task (prev_job arr_seq j) = job_task j
subgoal 3 (ID 127) is:
 job_arrival (prev_job arr_seq j) <= job_arrival j

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

    - now apply prev_job_arr.

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

2 subgoals (ID 126)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j : Job
  H_arrives_in_arr_seq : arrives_in arr_seq j
  H_positive_job_index, NZ_IND : 0 < job_index arr_seq j
  ============================
  job_task (prev_job arr_seq j) = job_task j

subgoal 2 (ID 127) is:
 job_arrival (prev_job arr_seq j) <= job_arrival j

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

    - now apply prev_job_task.

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

1 subgoal (ID 127)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j : Job
  H_arrives_in_arr_seq : arrives_in arr_seq j
  H_positive_job_index, NZ_IND : 0 < job_index arr_seq j
  ============================
  job_arrival (prev_job arr_seq j) <= job_arrival j

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

    - now apply prev_job_arr_lte.

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

No more subgoals.

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

  Qed.

We also show that for any job [j] there are no task arrivals between [prev_job j] and [j].
  Lemma no_jobs_between_consecutive_jobs:
    job_index arr_seq j > 0 →
    task_arrivals_between arr_seq (job_task j)
                          (job_arrival (prev_job arr_seq j)).+1 (job_arrival j) = [::].

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

1 subgoal (ID 137)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j : Job
  H_arrives_in_arr_seq : arrives_in arr_seq j
  H_positive_job_index : 0 < job_index arr_seq j
  ============================
  0 < job_index arr_seq j ->
  task_arrivals_between arr_seq (job_task j)
    (job_arrival (prev_job arr_seq j)).+1 (job_arrival j) = [::]

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

  Proof.
    move ⇒ POS_IND.

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

1 subgoal (ID 138)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j : Job
  H_arrives_in_arr_seq : arrives_in arr_seq j
  H_positive_job_index, POS_IND : 0 < job_index arr_seq j
  ============================
  task_arrivals_between arr_seq (job_task j)
    (job_arrival (prev_job arr_seq j)).+1 (job_arrival j) = [::]

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

    move : (prev_job_arr_lte); rewrite leq_eqVlt; move ⇒ /orP [/eqP EQ | LT].

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

2 subgoals (ID 218)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j : Job
  H_arrives_in_arr_seq : arrives_in arr_seq j
  H_positive_job_index, POS_IND : 0 < job_index arr_seq j
  EQ : job_arrival (prev_job arr_seq j) = job_arrival j
  ============================
  task_arrivals_between arr_seq (job_task j)
    (job_arrival (prev_job arr_seq j)).+1 (job_arrival j) = [::]

subgoal 2 (ID 219) is:
 task_arrivals_between arr_seq (job_task j)
   (job_arrival (prev_job arr_seq j)).+1 (job_arrival j) = [::]

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

    - rewrite EQ.

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

2 subgoals (ID 221)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j : Job
  H_arrives_in_arr_seq : arrives_in arr_seq j
  H_positive_job_index, POS_IND : 0 < job_index arr_seq j
  EQ : job_arrival (prev_job arr_seq j) = job_arrival j
  ============================
  task_arrivals_between arr_seq (job_task j) (job_arrival j).+1
    (job_arrival j) = [::]

subgoal 2 (ID 219) is:
 task_arrivals_between arr_seq (job_task j)
   (job_arrival (prev_job arr_seq j)).+1 (job_arrival j) = [::]

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

      apply/eqP/negPn/negP; rewrite -has_filter ⇒ /hasP [j' IN /eqP TASK].

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

2 subgoals (ID 423)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j : Job
  H_arrives_in_arr_seq : arrives_in arr_seq j
  H_positive_job_index, POS_IND : 0 < job_index arr_seq j
  EQ : job_arrival (prev_job arr_seq j) = job_arrival j
  j' : Job
  IN : j' \in arrivals_between arr_seq (job_arrival j).+1 (job_arrival j)
  TASK : job_task j' = job_task j
  ============================
  False

subgoal 2 (ID 219) is:
 task_arrivals_between arr_seq (job_task j)
   (job_arrival (prev_job arr_seq j)).+1 (job_arrival j) = [::]

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

      apply mem_bigcat_nat_exists in IN; move : IN ⇒ [i [J'_IN ARR_INEQ]].

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

2 subgoals (ID 448)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j : Job
  H_arrives_in_arr_seq : arrives_in arr_seq j
  H_positive_job_index, POS_IND : 0 < job_index arr_seq j
  EQ : job_arrival (prev_job arr_seq j) = job_arrival j
  j' : Job
  TASK : job_task j' = job_task j
  i : nat
  J'_IN : j' \in arrivals_at arr_seq i
  ARR_INEQ : job_arrival j < i < job_arrival j
  ============================
  False

subgoal 2 (ID 219) is:
 task_arrivals_between arr_seq (job_task j)
   (job_arrival (prev_job arr_seq j)).+1 (job_arrival j) = [::]

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

      now ssrlia.

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

1 subgoal (ID 219)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j : Job
  H_arrives_in_arr_seq : arrives_in arr_seq j
  H_positive_job_index, POS_IND : 0 < job_index arr_seq j
  LT : job_arrival (prev_job arr_seq j) < job_arrival j
  ============================
  task_arrivals_between arr_seq (job_task j)
    (job_arrival (prev_job arr_seq j)).+1 (job_arrival j) = [::]

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

    - apply/eqP/negPn/negP; rewrite -has_filter ⇒ /hasP [j3 IN /eqP TASK].

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

1 subgoal (ID 919)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j : Job
  H_arrives_in_arr_seq : arrives_in arr_seq j
  H_positive_job_index, POS_IND : 0 < job_index arr_seq j
  LT : job_arrival (prev_job arr_seq j) < job_arrival j
  j3 : Job
  IN : j3
         \in arrivals_between arr_seq (job_arrival (prev_job arr_seq j)).+1
               (job_arrival j)
  TASK : job_task j3 = job_task j
  ============================
  False

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

      apply mem_bigcat_nat_exists in IN; move : IN ⇒ [i [J3_IN ARR_INEQ]].

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

1 subgoal (ID 944)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j : Job
  H_arrives_in_arr_seq : arrives_in arr_seq j
  H_positive_job_index, POS_IND : 0 < job_index arr_seq j
  LT : job_arrival (prev_job arr_seq j) < job_arrival j
  j3 : Job
  TASK : job_task j3 = job_task j
  i : nat
  J3_IN : j3 \in arrivals_at arr_seq i
  ARR_INEQ : job_arrival (prev_job arr_seq j) < i < job_arrival j
  ============================
  False

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

      have J3_ARR : (arrives_in arr_seq j3) by apply in_arrseq_implies_arrives with (t := i).

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

1 subgoal (ID 950)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j : Job
  H_arrives_in_arr_seq : arrives_in arr_seq j
  H_positive_job_index, POS_IND : 0 < job_index arr_seq j
  LT : job_arrival (prev_job arr_seq j) < job_arrival j
  j3 : Job
  TASK : job_task j3 = job_task j
  i : nat
  J3_IN : j3 \in arrivals_at arr_seq i
  ARR_INEQ : job_arrival (prev_job arr_seq j) < i < job_arrival j
  J3_ARR : arrives_in arr_seq j3
  ============================
  False

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

      apply H_consistent_arrivals in J3_IN; rewrite -J3_IN in ARR_INEQ.

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

1 subgoal (ID 979)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j : Job
  H_arrives_in_arr_seq : arrives_in arr_seq j
  H_positive_job_index, POS_IND : 0 < job_index arr_seq j
  LT : job_arrival (prev_job arr_seq j) < job_arrival j
  j3 : Job
  TASK : job_task j3 = job_task j
  i : nat
  J3_IN : job_arrival j3 = i
  J3_ARR : arrives_in arr_seq j3
  ARR_INEQ : job_arrival (prev_job arr_seq j) < job_arrival j3 <
             job_arrival j
  ============================
  False

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

      move : ARR_INEQ ⇒ /andP [PJ_L_J3 J3_L_J].

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

1 subgoal (ID 1021)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j : Job
  H_arrives_in_arr_seq : arrives_in arr_seq j
  H_positive_job_index, POS_IND : 0 < job_index arr_seq j
  LT : job_arrival (prev_job arr_seq j) < job_arrival j
  j3 : Job
  TASK : job_task j3 = job_task j
  i : nat
  J3_IN : job_arrival j3 = i
  J3_ARR : arrives_in arr_seq j3
  PJ_L_J3 : job_arrival (prev_job arr_seq j) < job_arrival j3
  J3_L_J : job_arrival j3 < job_arrival j
  ============================
  False

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

      apply (earlier_arrival_implies_lower_index arr_seq H_consistent_arrivals _ _) in PJ_L_J3 ⇒ //; try by
          rewrite prev_job_task.

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

2 subgoals (ID 1030)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j : Job
  H_arrives_in_arr_seq : arrives_in arr_seq j
  H_positive_job_index, POS_IND : 0 < job_index arr_seq j
  LT : job_arrival (prev_job arr_seq j) < job_arrival j
  j3 : Job
  TASK : job_task j3 = job_task j
  i : nat
  J3_IN : job_arrival j3 = i
  J3_ARR : arrives_in arr_seq j3
  PJ_L_J3 : job_index arr_seq (prev_job arr_seq j) < job_index arr_seq j3
  J3_L_J : job_arrival j3 < job_arrival j
  ============================
  False

subgoal 2 (ID 1032) is:
 arrives_in arr_seq (prev_job arr_seq j)

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

      + apply (earlier_arrival_implies_lower_index arr_seq H_consistent_arrivals _ _) in J3_L_J ⇒ //.

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

2 subgoals (ID 1139)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j : Job
  H_arrives_in_arr_seq : arrives_in arr_seq j
  H_positive_job_index, POS_IND : 0 < job_index arr_seq j
  LT : job_arrival (prev_job arr_seq j) < job_arrival j
  j3 : Job
  TASK : job_task j3 = job_task j
  i : nat
  J3_IN : job_arrival j3 = i
  J3_ARR : arrives_in arr_seq j3
  PJ_L_J3 : job_index arr_seq (prev_job arr_seq j) < job_index arr_seq j3
  J3_L_J : job_index arr_seq j3 < job_index arr_seq j
  ============================
  False

subgoal 2 (ID 1032) is:
 arrives_in arr_seq (prev_job arr_seq j)

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

        now rewrite prev_job_index_j in PJ_L_J3; try by ssrlia.

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

1 subgoal (ID 1032)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j : Job
  H_arrives_in_arr_seq : arrives_in arr_seq j
  H_positive_job_index, POS_IND : 0 < job_index arr_seq j
  LT : job_arrival (prev_job arr_seq j) < job_arrival j
  j3 : Job
  TASK : job_task j3 = job_task j
  i : nat
  J3_IN : job_arrival j3 = i
  J3_ARR : arrives_in arr_seq j3
  PJ_L_J3 : job_arrival (prev_job arr_seq j) < job_arrival j3
  J3_L_J : job_arrival j3 < job_arrival j
  ============================
  arrives_in arr_seq (prev_job arr_seq j)

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

      + now apply prev_job_arr.

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

No more subgoals.

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

  Qed.

We show that there always exists a job of lesser [job_index] than a job with a positive [job_index] that arrives in the arrival sequence.
  Lemma exists_jobs_before_j:
    ∀ k,
      k < job_index arr_seq j →
      ∃ j',
        j ≠ j' ∧
        job_task j' = job_task j ∧
        arrives_in arr_seq j' ∧
        job_index arr_seq j' = k.

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

1 subgoal (ID 162)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j : Job
  H_arrives_in_arr_seq : arrives_in arr_seq j
  H_positive_job_index : 0 < job_index arr_seq j
  ============================
  forall k : nat,
  k < job_index arr_seq j ->
  exists j' : Job,
    j <> j' /\
    job_task j' = job_task j /\
    arrives_in arr_seq j' /\ job_index arr_seq j' = k

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

  Proof.
    intros k K_LT.

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

1 subgoal (ID 164)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j : Job
  H_arrives_in_arr_seq : arrives_in arr_seq j
  H_positive_job_index : 0 < job_index arr_seq j
  k : nat
  K_LT : k < job_index arr_seq j
  ============================
  exists j' : Job,
    j <> j' /\
    job_task j' = job_task j /\
    arrives_in arr_seq j' /\ job_index arr_seq j' = k

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

    ∃ (nth j (task_arrivals_up_to_job_arrival arr_seq j) k).

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

1 subgoal (ID 171)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j : Job
  H_arrives_in_arr_seq : arrives_in arr_seq j
  H_positive_job_index : 0 < job_index arr_seq j
  k : nat
  K_LT : k < job_index arr_seq j
  ============================
  j <> nth j (task_arrivals_up_to_job_arrival arr_seq j) k /\
  job_task (nth j (task_arrivals_up_to_job_arrival arr_seq j) k) = job_task j /\
  arrives_in arr_seq (nth j (task_arrivals_up_to_job_arrival arr_seq j) k) /\
  job_index arr_seq (nth j (task_arrivals_up_to_job_arrival arr_seq j) k) = k

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

    set (jk := nth j (task_arrivals_up_to_job_arrival arr_seq j) k).

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

1 subgoal (ID 178)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j : Job
  H_arrives_in_arr_seq : arrives_in arr_seq j
  H_positive_job_index : 0 < job_index arr_seq j
  k : nat
  K_LT : k < job_index arr_seq j
  jk := nth j (task_arrivals_up_to_job_arrival arr_seq j) k : Job
  ============================
  j <> jk /\
  job_task jk = job_task j /\
  arrives_in arr_seq jk /\ job_index arr_seq jk = k

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

    have K_LT_SIZE : (k < size (task_arrivals_up_to_job_arrival arr_seq j)) by
        apply ltn_leq_trans with (n := job_index arr_seq j) ⇒ //; first by apply index_size.

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

1 subgoal (ID 214)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j : Job
  H_arrives_in_arr_seq : arrives_in arr_seq j
  H_positive_job_index : 0 < job_index arr_seq j
  k : nat
  K_LT : k < job_index arr_seq j
  jk := nth j (task_arrivals_up_to_job_arrival arr_seq j) k : Job
  K_LT_SIZE : k < size (task_arrivals_up_to_job_arrival arr_seq j)
  ============================
  j <> jk /\
  job_task jk = job_task j /\
  arrives_in arr_seq jk /\ job_index arr_seq jk = k

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

    have JK_IN : (jk \in task_arrivals_up_to_job_arrival arr_seq j) by rewrite /jk; apply mem_nth ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 227)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j : Job
  H_arrives_in_arr_seq : arrives_in arr_seq j
  H_positive_job_index : 0 < job_index arr_seq j
  k : nat
  K_LT : k < job_index arr_seq j
  jk := nth j (task_arrivals_up_to_job_arrival arr_seq j) k : Job
  K_LT_SIZE : k < size (task_arrivals_up_to_job_arrival arr_seq j)
  JK_IN : jk \in task_arrivals_up_to_job_arrival arr_seq j
  ============================
  j <> jk /\
  job_task jk = job_task j /\
  arrives_in arr_seq jk /\ job_index arr_seq jk = k

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

    rewrite mem_filter in JK_IN; move : JK_IN ⇒ /andP [/eqP TSK JK_IN].

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

1 subgoal (ID 329)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j : Job
  H_arrives_in_arr_seq : arrives_in arr_seq j
  H_positive_job_index : 0 < job_index arr_seq j
  k : nat
  K_LT : k < job_index arr_seq j
  jk := nth j (task_arrivals_up_to_job_arrival arr_seq j) k : Job
  K_LT_SIZE : k < size (task_arrivals_up_to_job_arrival arr_seq j)
  TSK : job_task jk = job_task j
  JK_IN : jk \in arrivals_between arr_seq 0 (job_arrival j).+1
  ============================
  j <> jk /\
  job_task jk = job_task j /\
  arrives_in arr_seq jk /\ job_index arr_seq jk = k

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

    apply mem_bigcat_nat_exists in JK_IN; move : JK_IN ⇒ [i [JK_IN I_INEQ]].
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 354)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j : Job
  H_arrives_in_arr_seq : arrives_in arr_seq j
  H_positive_job_index : 0 < job_index arr_seq j
  k : nat
  K_LT : k < job_index arr_seq j
  jk := nth j (task_arrivals_up_to_job_arrival arr_seq j) k : Job
  K_LT_SIZE : k < size (task_arrivals_up_to_job_arrival arr_seq j)
  TSK : job_task jk = job_task j
  i : nat
  JK_IN : jk \in arrivals_at arr_seq i
  I_INEQ : 0 <= i < (job_arrival j).+1
  ============================
  j <> jk /\
  job_task jk = job_task j /\
  arrives_in arr_seq jk /\ job_index arr_seq jk = k

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

    have JK_ARR : (arrives_in arr_seq jk) by apply in_arrseq_implies_arrives with (t := i) ⇒ //.

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

1 subgoal (ID 360)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j : Job
  H_arrives_in_arr_seq : arrives_in arr_seq j
  H_positive_job_index : 0 < job_index arr_seq j
  k : nat
  K_LT : k < job_index arr_seq j
  jk := nth j (task_arrivals_up_to_job_arrival arr_seq j) k : Job
  K_LT_SIZE : k < size (task_arrivals_up_to_job_arrival arr_seq j)
  TSK : job_task jk = job_task j
  i : nat
  JK_IN : jk \in arrivals_at arr_seq i
  I_INEQ : 0 <= i < (job_arrival j).+1
  JK_ARR : arrives_in arr_seq jk
  ============================
  j <> jk /\
  job_task jk = job_task j /\
  arrives_in arr_seq jk /\ job_index arr_seq jk = k

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

    have INDJK : (index jk (task_arrivals_up_to_job_arrival arr_seq j) = k).

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

2 subgoals (ID 368)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j : Job
  H_arrives_in_arr_seq : arrives_in arr_seq j
  H_positive_job_index : 0 < job_index arr_seq j
  k : nat
  K_LT : k < job_index arr_seq j
  jk := nth j (task_arrivals_up_to_job_arrival arr_seq j) k : Job
  K_LT_SIZE : k < size (task_arrivals_up_to_job_arrival arr_seq j)
  TSK : job_task jk = job_task j
  i : nat
  JK_IN : jk \in arrivals_at arr_seq i
  I_INEQ : 0 <= i < (job_arrival j).+1
  JK_ARR : arrives_in arr_seq jk
  ============================
  index jk (task_arrivals_up_to_job_arrival arr_seq j) = k

subgoal 2 (ID 370) is:
 j <> jk /\
 job_task jk = job_task j /\
 arrives_in arr_seq jk /\ job_index arr_seq jk = k

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

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

1 subgoal (ID 368)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j : Job
  H_arrives_in_arr_seq : arrives_in arr_seq j
  H_positive_job_index : 0 < job_index arr_seq j
  k : nat
  K_LT : k < job_index arr_seq j
  jk := nth j (task_arrivals_up_to_job_arrival arr_seq j) k : Job
  K_LT_SIZE : k < size (task_arrivals_up_to_job_arrival arr_seq j)
  TSK : job_task jk = job_task j
  i : nat
  JK_IN : jk \in arrivals_at arr_seq i
  I_INEQ : 0 <= i < (job_arrival j).+1
  JK_ARR : arrives_in arr_seq jk
  ============================
  index jk (task_arrivals_up_to_job_arrival arr_seq j) = k

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

apply index_uniq ⇒ //.

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

1 subgoal (ID 372)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j : Job
  H_arrives_in_arr_seq : arrives_in arr_seq j
  H_positive_job_index : 0 < job_index arr_seq j
  k : nat
  K_LT : k < job_index arr_seq j
  jk := nth j (task_arrivals_up_to_job_arrival arr_seq j) k : Job
  K_LT_SIZE : k < size (task_arrivals_up_to_job_arrival arr_seq j)
  TSK : job_task jk = job_task j
  i : nat
  JK_IN : jk \in arrivals_at arr_seq i
  I_INEQ : 0 <= i < (job_arrival j).+1
  JK_ARR : arrives_in arr_seq jk
  ============================
  uniq (task_arrivals_up_to_job_arrival arr_seq j)

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

      now apply uniq_task_arrivals ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 370)

subgoal 1 (ID 370) is:
 j <> jk /\
 job_task jk = job_task j /\
 arrives_in arr_seq jk /\ job_index arr_seq jk = k

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

}

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

1 subgoal (ID 370)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j : Job
  H_arrives_in_arr_seq : arrives_in arr_seq j
  H_positive_job_index : 0 < job_index arr_seq j
  k : nat
  K_LT : k < job_index arr_seq j
  jk := nth j (task_arrivals_up_to_job_arrival arr_seq j) k : Job
  K_LT_SIZE : k < size (task_arrivals_up_to_job_arrival arr_seq j)
  TSK : job_task jk = job_task j
  i : nat
  JK_IN : jk \in arrivals_at arr_seq i
  I_INEQ : 0 <= i < (job_arrival j).+1
  JK_ARR : arrives_in arr_seq jk
  INDJK : index jk (task_arrivals_up_to_job_arrival arr_seq j) = k
  ============================
  j <> jk /\
  job_task jk = job_task j /\
  arrives_in arr_seq jk /\ job_index arr_seq jk = k

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

    repeat split ⇒ //.
(* ----------------------------------[ coqtop ]---------------------------------

2 subgoals (ID 402)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j : Job
  H_arrives_in_arr_seq : arrives_in arr_seq j
  H_positive_job_index : 0 < job_index arr_seq j
  k : nat
  K_LT : k < job_index arr_seq j
  jk := nth j (task_arrivals_up_to_job_arrival arr_seq j) k : Job
  K_LT_SIZE : k < size (task_arrivals_up_to_job_arrival arr_seq j)
  TSK : job_task jk = job_task j
  i : nat
  JK_IN : jk \in arrivals_at arr_seq i
  I_INEQ : 0 <= i < (job_arrival j).+1
  JK_ARR : arrives_in arr_seq jk
  INDJK : index jk (task_arrivals_up_to_job_arrival arr_seq j) = k
  ============================
  j <> jk

subgoal 2 (ID 558) is:
 job_index arr_seq jk = k

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


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

1 subgoal (ID 402)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j : Job
  H_arrives_in_arr_seq : arrives_in arr_seq j
  H_positive_job_index : 0 < job_index arr_seq j
  k : nat
  K_LT : k < job_index arr_seq j
  jk := nth j (task_arrivals_up_to_job_arrival arr_seq j) k : Job
  K_LT_SIZE : k < size (task_arrivals_up_to_job_arrival arr_seq j)
  TSK : job_task jk = job_task j
  i : nat
  JK_IN : jk \in arrivals_at arr_seq i
  I_INEQ : 0 <= i < (job_arrival j).+1
  JK_ARR : arrives_in arr_seq jk
  INDJK : index jk (task_arrivals_up_to_job_arrival arr_seq j) = k
  ============================
  j <> jk

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

rewrite → diff_jobs_iff_diff_indices ⇒ //; last by auto.

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

1 subgoal (ID 596)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j : Job
  H_arrives_in_arr_seq : arrives_in arr_seq j
  H_positive_job_index : 0 < job_index arr_seq j
  k : nat
  K_LT : k < job_index arr_seq j
  jk := nth j (task_arrivals_up_to_job_arrival arr_seq j) k : Job
  K_LT_SIZE : k < size (task_arrivals_up_to_job_arrival arr_seq j)
  TSK : job_task jk = job_task j
  i : nat
  JK_IN : jk \in arrivals_at arr_seq i
  I_INEQ : 0 <= i < (job_arrival j).+1
  JK_ARR : arrives_in arr_seq jk
  INDJK : index jk (task_arrivals_up_to_job_arrival arr_seq j) = k
  ============================
  job_index arr_seq j <> job_index arr_seq jk

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

      rewrite /job_index; rewrite [in X in _ ≠ X] (job_index_same_in_task_arrivals _ _ jk j) ⇒ //.

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

2 subgoals (ID 739)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j : Job
  H_arrives_in_arr_seq : arrives_in arr_seq j
  H_positive_job_index : 0 < job_index arr_seq j
  k : nat
  K_LT : k < job_index arr_seq j
  jk := nth j (task_arrivals_up_to_job_arrival arr_seq j) k : Job
  K_LT_SIZE : k < size (task_arrivals_up_to_job_arrival arr_seq j)
  TSK : job_task jk = job_task j
  i : nat
  JK_IN : jk \in arrivals_at arr_seq i
  I_INEQ : 0 <= i < (job_arrival j).+1
  JK_ARR : arrives_in arr_seq jk
  INDJK : index jk (task_arrivals_up_to_job_arrival arr_seq j) = k
  ============================
  index j (task_arrivals_up_to_job_arrival arr_seq j) <>
  index jk (task_arrivals_up_to_job_arrival arr_seq j)

subgoal 2 (ID 744) is:
 job_arrival jk <= job_arrival j

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

      - rewrite index_uniq -/(job_index arr_seq j)=> //; last by apply uniq_task_arrivals.

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

2 subgoals (ID 812)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j : Job
  H_arrives_in_arr_seq : arrives_in arr_seq j
  H_positive_job_index : 0 < job_index arr_seq j
  k : nat
  K_LT : k < job_index arr_seq j
  jk := nth j (task_arrivals_up_to_job_arrival arr_seq j) k : Job
  K_LT_SIZE : k < size (task_arrivals_up_to_job_arrival arr_seq j)
  TSK : job_task jk = job_task j
  i : nat
  JK_IN : jk \in arrivals_at arr_seq i
  I_INEQ : 0 <= i < (job_arrival j).+1
  JK_ARR : arrives_in arr_seq jk
  INDJK : index jk (task_arrivals_up_to_job_arrival arr_seq j) = k
  ============================
  job_index arr_seq j <> k

subgoal 2 (ID 744) is:
 job_arrival jk <= job_arrival j

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

        now ssrlia.

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

1 subgoal (ID 744)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j : Job
  H_arrives_in_arr_seq : arrives_in arr_seq j
  H_positive_job_index : 0 < job_index arr_seq j
  k : nat
  K_LT : k < job_index arr_seq j
  jk := nth j (task_arrivals_up_to_job_arrival arr_seq j) k : Job
  K_LT_SIZE : k < size (task_arrivals_up_to_job_arrival arr_seq j)
  TSK : job_task jk = job_task j
  i : nat
  JK_IN : jk \in arrivals_at arr_seq i
  I_INEQ : 0 <= i < (job_arrival j).+1
  JK_ARR : arrives_in arr_seq jk
  INDJK : index jk (task_arrivals_up_to_job_arrival arr_seq j) = k
  ============================
  job_arrival jk <= job_arrival j

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

      - apply H_consistent_arrivals in JK_IN; rewrite -JK_IN in I_INEQ.

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

1 subgoal (ID 1227)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j : Job
  H_arrives_in_arr_seq : arrives_in arr_seq j
  H_positive_job_index : 0 < job_index arr_seq j
  k : nat
  K_LT : k < job_index arr_seq j
  jk := nth j (task_arrivals_up_to_job_arrival arr_seq j) k : Job
  K_LT_SIZE : k < size (task_arrivals_up_to_job_arrival arr_seq j)
  TSK : job_task jk = job_task j
  i : nat
  JK_IN : job_arrival jk = i
  JK_ARR : arrives_in arr_seq jk
  INDJK : index jk (task_arrivals_up_to_job_arrival arr_seq j) = k
  I_INEQ : 0 <= job_arrival jk < (job_arrival j).+1
  ============================
  job_arrival jk <= job_arrival j

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

        now ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------

1 subgoal (ID 558)

subgoal 1 (ID 558) is:
 job_index arr_seq jk = k

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

}

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

1 subgoal (ID 558)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j : Job
  H_arrives_in_arr_seq : arrives_in arr_seq j
  H_positive_job_index : 0 < job_index arr_seq j
  k : nat
  K_LT : k < job_index arr_seq j
  jk := nth j (task_arrivals_up_to_job_arrival arr_seq j) k : Job
  K_LT_SIZE : k < size (task_arrivals_up_to_job_arrival arr_seq j)
  TSK : job_task jk = job_task j
  i : nat
  JK_IN : jk \in arrivals_at arr_seq i
  I_INEQ : 0 <= i < (job_arrival j).+1
  JK_ARR : arrives_in arr_seq jk
  INDJK : index jk (task_arrivals_up_to_job_arrival arr_seq j) = k
  ============================
  job_index arr_seq jk = k

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

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

1 subgoal (ID 558)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j : Job
  H_arrives_in_arr_seq : arrives_in arr_seq j
  H_positive_job_index : 0 < job_index arr_seq j
  k : nat
  K_LT : k < job_index arr_seq j
  jk := nth j (task_arrivals_up_to_job_arrival arr_seq j) k : Job
  K_LT_SIZE : k < size (task_arrivals_up_to_job_arrival arr_seq j)
  TSK : job_task jk = job_task j
  i : nat
  JK_IN : jk \in arrivals_at arr_seq i
  I_INEQ : 0 <= i < (job_arrival j).+1
  JK_ARR : arrives_in arr_seq jk
  INDJK : index jk (task_arrivals_up_to_job_arrival arr_seq j) = k
  ============================
  job_index arr_seq jk = k

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

rewrite /job_index; rewrite [in X in X = _] (job_index_same_in_task_arrivals _ _ jk j) ⇒ //.

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

1 subgoal (ID 1610)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j : Job
  H_arrives_in_arr_seq : arrives_in arr_seq j
  H_positive_job_index : 0 < job_index arr_seq j
  k : nat
  K_LT : k < job_index arr_seq j
  jk := nth j (task_arrivals_up_to_job_arrival arr_seq j) k : Job
  K_LT_SIZE : k < size (task_arrivals_up_to_job_arrival arr_seq j)
  TSK : job_task jk = job_task j
  i : nat
  JK_IN : jk \in arrivals_at arr_seq i
  I_INEQ : 0 <= i < (job_arrival j).+1
  JK_ARR : arrives_in arr_seq jk
  INDJK : index jk (task_arrivals_up_to_job_arrival arr_seq j) = k
  ============================
  job_arrival jk <= job_arrival j

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

      apply H_consistent_arrivals in JK_IN; rewrite -JK_IN in I_INEQ.

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

1 subgoal (ID 1663)
  
  Task : TaskType
  Job : JobType
  H : JobTask Job Task
  H0 : JobArrival Job
  arr_seq : arrival_sequence Job
  H_consistent_arrivals : consistent_arrival_times arr_seq
  H_uniq_arr_seq : arrival_sequence_uniq arr_seq
  j : Job
  H_arrives_in_arr_seq : arrives_in arr_seq j
  H_positive_job_index : 0 < job_index arr_seq j
  k : nat
  K_LT : k < job_index arr_seq j
  jk := nth j (task_arrivals_up_to_job_arrival arr_seq j) k : Job
  K_LT_SIZE : k < size (task_arrivals_up_to_job_arrival arr_seq j)
  TSK : job_task jk = job_task j
  i : nat
  JK_IN : job_arrival jk = i
  JK_ARR : arrives_in arr_seq jk
  INDJK : index jk (task_arrivals_up_to_job_arrival arr_seq j) = k
  I_INEQ : 0 <= job_arrival jk < (job_arrival j).+1
  ============================
  job_arrival jk <= job_arrival j

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

      now ssrlia.
(* ----------------------------------[ coqtop ]---------------------------------

No more subgoals.

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

}

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

No more subgoals.

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

  Qed.

End PreviousJob.