Add platform for models with bounded nonpreemptive segments

model/schedule/uni/limited/platform/definitions.v

+Require Import rt.util.all.
+Require Import rt.model.arrival.basic.job
+               rt.model.arrival.basic.task
+               rt.model.priority
+               rt.model.arrival.basic.task_arrival.
+Require Import rt.model.schedule.uni.schedule
+               rt.model.schedule.uni.service
+               rt.model.schedule.uni.basic.platform.
+Require Import rt.model.schedule.uni.nonpreemptive.schedule.
+
+From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
+
+(** * Platform with limited preemptions *)
+(** In this module we introduce the notion of whether a job can be preempted at a given time 
+   (using a predicate can_be_preempted). In addition, we provide instantiations of the 
+   predicate for various preemption models. *)
+Module LimitedPreemptionPlatform.
+
+  Import Epsilon Job SporadicTaskset UniprocessorSchedule Priority Service.
+  
+  (* In this section, we define a processor platform with limited preemptions. *)
+  Section Properties.
+
+    Context {Task: eqType}.
+    Variable task_cost: Task -> time.
+    
+    Context {Job: eqType}.
+    Variable job_arrival: Job -> time.
+    Variable job_cost: Job -> time.
+    Variable job_task: Job -> Task.
+     
+    (* Consider any job arrival sequence... *)
+    Variable arr_seq: arrival_sequence Job.
+    
+    (* ...and any uniprocessor schedule of these jobs. *)
+    Variable sched: schedule Job.
+
+    (* For simplicity, let's define some local names. *)
+    Let job_pending := pending job_arrival job_cost sched.
+    Let job_completed_by := completed_by job_cost sched.
+    Let job_scheduled_at := scheduled_at sched.
+
+    (* First, we define the notion of a preemption time. *)
+    Section PreemptionTime. 
+
+      (* Let can_be_preempted be a function that maps a job j and the progress of j
+         at some time instant t to a boolean value, i.e., true if job j can be 
+         preempted at this point of execution and false otherwise. *)  
+      Variable can_be_preempted: Job -> time -> bool.
+      
+      (* We say that a time instant t is a preemption time iff there's no job currently 
+         scheduled at t that cannot be preempted (according to the predicate). *)
+      Definition preemption_time (t: time) :=
+        if sched t is Some j then
+          can_be_preempted j (service sched j t)
+        else true. 
+
+      (* Since the notion of preemption time is based on an user-provided 
+         predicate (variable can_be_preempted), it does not guarantee that 
+         the scheduler will enforce correct behavior. For that, we must 
+         define additional predicates. *)
+      Section CorrectPreemptionModel.
+
+        (* First, if a job j is not preemptive at some time instant t, 
+           then j must be scheduled at time t. *)
+        Definition not_preemptive_implies_scheduled (j: Job) :=
+          forall t,
+            ~~ can_be_preempted j (service sched j t) ->
+            job_scheduled_at j t. 
+
+        (* A job can start its execution only from a preemption point. *)
+        Definition execution_starts_with_preemption_point (j: Job) := 
+          forall prt,
+            ~~ job_scheduled_at j prt ->
+            job_scheduled_at j prt.+1 ->
+            can_be_preempted j (service sched j prt.+1).
+
+        (* We say that a model is a correct preemption model if both
+           definitions given above are satisfied for any job. *)
+        Definition correct_preemption_model :=
+          forall j,
+            arrives_in arr_seq j ->
+            not_preemptive_implies_scheduled j
+            /\ execution_starts_with_preemption_point j.
+        
+      End CorrectPreemptionModel.
+
+      (* Note that for analysis purposes, it is important that the distance 
+         between preemption points of a job is bounded. To ensure that, we 
+         define next the model of bounded nonpreemptive segment. *)
+      Section ModelWithBoundedNonpreemptiveRegions.
+
+        (* We require that a job has to be executed at least one time instant
+           in order to reach a nonpreemptive segment. *)
+        Definition job_cannot_become_nonpreemptive_before_execution (j: Job) :=
+          can_be_preempted j 0.
+ 
+        (* And vice versa, a job cannot remain nonpreemptive after its completion. *)
+        Definition job_cannot_be_nonpreemptive_after_completion (j: Job) := 
+          can_be_preempted j (job_cost j).
+
+        (* Consider a function that maps a job to the length of 
+           its maximal nonpreemptive segment. *)
+        Variable job_max_nps: Job -> time.
+        
+        (* And a function task_max_nps... *)
+        Variable task_max_nps: Task -> time.
+                  
+        (* ...that gives an upper bound for values of the function job_max_nps. *)
+        Definition job_max_nonpreemptive_segment_le_task_max_nonpreemptive_segment (j: Job) :=
+          arrives_in arr_seq j ->
+          job_max_nps j <= task_max_nps (job_task j).
+        
+        (* Next, we say that all the segments of a job j have bounded length iff for any 
+           progress progr of job j there exists a preemption point preeemption_point such that
+           [progr <= preemption_point <= progr + (job_max_nps j - ε)]. That is, in any time 
+           interval of length [job_max_nps j], there exists a preeemption point which     
+           lies in this interval. *)
+        Definition nonpreemptive_regions_have_bounded_length (j: Job) :=
+          forall progr,
+            0 <= progr <= job_cost j -> 
+            exists preemption_point,
+              progr <= preemption_point <= progr + (job_max_nps j - ε) /\
+              can_be_preempted j preemption_point.
+        
+        (* Finally, we say that the schedule enforces bounded nonpreemptive segments 
+           iff the predicate can_be_preempted satisfies the two conditions above. *)
+        Definition model_with_bounded_nonpreemptive_segments :=
+          forall j,
+            arrives_in arr_seq j ->
+            job_cannot_become_nonpreemptive_before_execution j
+            /\ job_cannot_be_nonpreemptive_after_completion j
+            /\ job_max_nonpreemptive_segment_le_task_max_nonpreemptive_segment j
+            /\ nonpreemptive_regions_have_bounded_length j.
+        
+      End ModelWithBoundedNonpreemptiveRegions.
+
+      (* In this section we prove a few basic properties of the can_be_preempted predicate. *)
+      Section Lemmas.
+
+        Variable job_max_nps: Job -> time.
+        Variable task_max_nps: Task -> time.
+
+        (* Consider the correct model with bounded nonpreemptive segments. *)
+        Hypothesis H_correct_preemption_model: correct_preemption_model.
+        Hypothesis H_model_with_bounded_np_segments:
+          model_with_bounded_nonpreemptive_segments job_max_nps task_max_nps.
+
+        (* Assume jobs come from some arrival sequence. *)
+        Hypothesis H_jobs_come_from_arrival_sequence:
+          jobs_come_from_arrival_sequence sched arr_seq.
+
+        (* Then, we can show that time 0 is a preemption time. *)
+        Lemma zero_is_pt: preemption_time 0.
+        Proof.
+          unfold preemption_time.
+          case SCHED: (sched 0) => [j | ]; last by done.
+          move: (SCHED) => /eqP ARR.
+          apply H_jobs_come_from_arrival_sequence in ARR.
+          rewrite /service /service_during big_geq; last by done.
+            by move: (H_model_with_bounded_np_segments j ARR) => [PP _]; apply PP.
+        Qed.
+
+        (* Also, we show that the first instant of execution is a preemption time. *)
+        Lemma first_moment_is_pt:
+          forall j prt,
+            arrives_in arr_seq j -> 
+            ~~ job_scheduled_at j prt ->
+            job_scheduled_at j prt.+1 ->
+            preemption_time prt.+1.
+        Proof.
+          intros s pt ARR NSCHED SCHED.
+          unfold preemption_time. 
+          move: (SCHED) => /eqP SCHED2; rewrite SCHED2; clear SCHED2.
+            by move: (H_correct_preemption_model s ARR) => [_ FHF]; auto.
+        Qed. 
+        
+      End Lemmas. 
+      
+    End PreemptionTime.
+    
+    (* Next, we define properties related to execution. *)
+    Section Execution.
+
+      (* Similarly to preemptive scheduling, we say that the schedule is 
+         work-conserving iff whenever a job is backlogged, the processor 
+         is always busy scheduling another job. *)
+      (* Imported from the preemptive schedule. *)
+      Definition work_conserving := Platform.work_conserving job_cost.
+
+    End Execution.
+
+    (* Next, we define properties related to FP scheduling. *)
+    Section FP.
+      
+      (* Consider any preemption model. *)
+      Variable preemption_model: Job -> time -> bool.
+     
+      (* We say that an FP policy...*)
+      Variable higher_eq_priority: FP_policy Task.
+
+      (* ...is respected by the schedule iff, at every preemption point, 
+         a scheduled task has higher (or same) priority than (as) 
+         any backlogged task. *)
+      Definition respects_FP_policy_at_preemption_point :=
+        forall j j_hp t,
+          preemption_time preemption_model t ->
+          arrives_in arr_seq j ->
+          backlogged job_arrival job_cost sched j t ->
+          scheduled_at sched j_hp t ->
+          higher_eq_priority (job_task j_hp) (job_task j).
+       
+    End FP.
+     
+    (* Next, we define properties related to JLFP policies. *)
+    Section JLFP.
+
+      (* Consider a scheduling model. *)
+      Variable preemption_model: Job -> time -> bool.
+      
+      (* We say that a JLFP policy ...*)
+      Variable higher_eq_priority: JLFP_policy Job.
+
+      (* ...is respected by the schedule iff, at every preemption point, 
+         a scheduled task has higher (or same) priority than (as) 
+         any backlogged task. *)
+      Definition respects_JLFP_policy_at_preemption_point :=
+        forall j j_hp t,
+          preemption_time preemption_model t ->
+          arrives_in arr_seq j ->
+          backlogged job_arrival job_cost sched j t ->
+          scheduled_at sched j_hp t ->
+          higher_eq_priority j_hp j.
+      
+    End JLFP.
+
+  End Properties.
+  
+End LimitedPreemptionPlatform.
\ No newline at end of file

model/schedule/uni/limited/platform/limited.v

+Require Import rt.util.all.  
+Require Import rt.model.arrival.basic.job rt.model.arrival.basic.task.
+Require Import rt.model.schedule.uni.schedule. 
+Require Export rt.model.schedule.uni.limited.platform.definitions.
+Require Export rt.model.schedule.uni.limited.platform.util.
+
+From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
+
+(** * Platform for models with limited preemptions *)
+(** In module uni.limited.platform we introduce the notion of whether a job can be
+    preempted at a given time (using a predicate can_be_preempted). In this section,
+    we instantiate can_be_preempted for the model with fixed preemption points and 
+    model with floating nonpreemptive regions. *)
+Module ModelWithLimitedPreemptions.
+
+  Import Epsilon Job NondecreasingSequence UniprocessorSchedule LimitedPreemptionPlatform.
+
+  (* In this section, we instantiate can_be_preempted for the model with fixed preemption points and
+     the model with floating nonpreemptive regions. We also prove that the definitions are correct. *)
+  Section ModelsWithLimitedPreemptions.
+    
+    Context {Task: eqType}.
+    Variable task_cost: Task -> time.
+    
+    Context {Job: eqType}.
+    Variable job_arrival: Job -> time.
+    Variable job_cost: Job -> time.
+    Variable job_task: Job -> Task.
+
+    (* Consider any job arrival sequence. *)
+    Variable arr_seq: arrival_sequence Job.
+        
+    (* Next, consider a function that maps a job to the sequence of its preemption points. *)
+    Variable job_preemption_points: Job -> seq time.
+
+    (* In this section, we provide a set of hypotheses for the models with limited preemptions. *)
+    Section Definitions.
+
+      (* In this section, we introduce the job-level definitions.
+         They are the same for both models. *)
+      Section ModelWithLimitedPreemptions.
+        
+        (* First, we define a function that maps a job to the 
+           sequence of lengths of its nonpreemptive segments. *)
+        Definition lengths_of_segments j := distances (job_preemption_points j).
+
+        (* Next, we define a function that maps a job to the
+           length of the longest nonpreemptive segment of job j. *)
+        Definition job_max_nps (j: Job) := max (lengths_of_segments j).
+
+        (* Similarly, job_last is a function that maps a job to the  
+           length of the last nonpreemptive segment. *)
+        Definition job_last_nps (j: Job) := last (lengths_of_segments j).
+
+        (* Next, we describe some structural properties that
+           a sequence of preemption points should satisfy. *)
+
+        (* (1) The sequence of preemption points of a job with zero cost is equal to [0; 0]. *)
+        Definition job_with_zero_cost_consists_of_one_empty_segment :=
+          forall j, arrives_in arr_seq j -> job_cost j = 0 -> job_preemption_points j = [::0; 0].
+
+        (* (2) The last nonpreemptive segment of a job with positive cost cannot be empty. *)
+        Definition last_segment_is_positive :=
+          forall j, arrives_in arr_seq j -> job_cost j > 0 -> job_last_nps j > 0.
+        
+        (* (3) We also require the sequence of preemption points to contain the beginning... *)
+        Definition beginning_of_execution_in_preemption_points :=
+          forall j, arrives_in arr_seq j -> first (job_preemption_points j) = 0.
+
+        (* ... and (4) the end of execution for any job j.*)
+        Definition end_of_execution_in_preemption_points :=
+          forall j, arrives_in arr_seq j -> last (job_preemption_points j) = job_cost j.
+
+        (* (5) We require the sequence of preemption points to be a nondecreasing sequence. *)
+        Definition preemption_points_is_nondecreasing_sequence :=
+          forall (j: Job),
+            arrives_in arr_seq j -> 
+            nondecreasing_sequence (job_preemption_points j).
+
+        (* Finally, we define a job-level model with limited preemptions 
+           as a concatenation of the hypotheses above.  *)
+        Definition limited_preemptions_job_model :=
+          job_with_zero_cost_consists_of_one_empty_segment /\
+          last_segment_is_positive /\ 
+          beginning_of_execution_in_preemption_points /\
+          end_of_execution_in_preemption_points /\
+          preemption_points_is_nondecreasing_sequence.
+                  
+      End ModelWithLimitedPreemptions.
+
+      (* In this section, we define the model with fixed preemption points. *)
+      Section ModelWithFixedPreemptionPoints.
+
+        (* Consider a function that maps a task to the sequence of its preemption points. *)
+        Variable task_preemption_points: Task -> seq time.
+
+        (* Similarly to job's nonpreemptive segments, we define the length of the max
+           nonpreemptive segment and lenght of the last nonpreemptive segment. *)
+        Definition task_last_nps tsk := last (distances (task_preemption_points tsk)).
+        Definition task_max_nps tsk := max (distances (task_preemption_points tsk)).
+         
+        (* Consider an arbitrary task set ts. *)     
+        Variable ts: list Task.
+
+        (* Next, we describe some structural properties that
+           a sequence of preemption points of task should satisfy. *)
+        
+        (* (1) We require the sequence of preemption points to contain the beginning... *)
+        Definition task_beginning_of_execution_in_preemption_points :=
+          forall tsk, tsk \in ts -> first (task_preemption_points tsk) = 0.
+
+        (* ... and (2) the end of execution for any job j.*)
+        Definition task_end_of_execution_in_preemption_points :=
+          forall tsk, tsk \in ts -> last (task_preemption_points tsk) = task_cost tsk.
+
+        (* (3) We require the sequence of preemption points 
+           to be a nondecreasing sequence. *)
+        Definition task_preemption_points_is_nondecreasing_sequence :=
+          forall tsk, tsk \in ts -> nondecreasing_sequence (task_preemption_points tsk).
+
+        (* (4) Next, we require the number of nonpreemptive segments of a job to be 
+           equal to the number of nonpreemptive segments of its task. Note that 
+           some of nonpreemptive segments of a job can have zero length, nonetheless
+           the number of segments should match. *)
+        Definition job_consists_of_the_same_number_of_segments_as_task :=
+          forall j,
+            arrives_in arr_seq j -> 
+            size (job_preemption_points j) = size (task_preemption_points (job_task j)).
+
+        (* (5) We require lengths of nonpreemptive segments of a job to be bounded 
+           by lenghts of the corresponding segments of its task.  *)
+        Definition lengths_of_task_segments_bound_length_of_job_segments :=
+          forall j n,
+            arrives_in arr_seq j -> 
+            nth 0 (distances (job_preemption_points j)) n
+            <= nth 0 (distances (task_preemption_points (job_task j))) n.
+
+        (* (6) Lastly, we ban empty nonpreemptive segments for tasks. *)
+        Definition task_segments_are_nonempty :=
+          forall tsk n,
+            (tsk \in ts) ->
+            n < size (distances (task_preemption_points tsk)) ->
+            ε <= nth 0 (distances (task_preemption_points tsk)) n.
+
+        (* We define a task-level model with fixed preemption points 
+           as a concatenation of the hypotheses above. *) 
+        Definition fixed_preemption_points_task_model :=
+          task_beginning_of_execution_in_preemption_points /\
+          task_end_of_execution_in_preemption_points /\
+          task_preemption_points_is_nondecreasing_sequence /\
+          job_consists_of_the_same_number_of_segments_as_task /\
+          lengths_of_task_segments_bound_length_of_job_segments /\
+          task_segments_are_nonempty.
+
+        (* We define the model with fixed preemption points as 
+           the model with fixed preemptions points at the task-level
+           and model with limited preemptions at the job-level. *)
+        Definition fixed_preemption_points_model :=
+          limited_preemptions_job_model /\
+          fixed_preemption_points_task_model.
+        
+      End ModelWithFixedPreemptionPoints.
+      
+      (* In this section, we define the model with floating nonpreemptive regions. *)
+      Section ModelWithFloatingNonpreemptiveRegions.
+
+        (* Consider a function task_max_nps that maps a task to 
+           the lenght of its max nonpreemptive segment. *)
+        Variable task_max_nps: Task -> time.
+        
+        (* We require [task_max_nps (job_task j)] to be an upper bound 
+           of the lenght of the max nonpreemptive segment of job j. *)
+        Definition job_max_np_segment_le_task_max_np_segment :=
+          forall (j: Job),
+            arrives_in arr_seq j ->
+            job_max_nps j <= task_max_nps (job_task j).
+
+        (* We define the model with floating nonpreemptive regions as 
+           the model with floating nonpreemptive regions at the task-level
+           and model with limited preemptions at the job-level.  *)
+        Definition model_with_floating_nonpreemptive_regions :=
+          limited_preemptions_job_model /\
+          job_max_np_segment_le_task_max_np_segment.        
+
+      End ModelWithFloatingNonpreemptiveRegions.
+
+      (* Given a list of preemption points for each job, we define the function 
+         can_be_preempted for the model with limited preemptions as follows. We say 
+         that job j can be preempted at time t iff the service received by j at 
+         time t belongs to the list of preemptions points. *)
+      Definition can_be_preempted_for_model_with_limited_preemptions (j: Job) (progr: time) :=
+        progr \in job_preemption_points j.
+
+      (* Based on the definition of the model with limited preemptions, 
+         we define a schedule with limited preemptions. *)
+      Definition is_schedule_with_limited_preemptions (sched: schedule Job) := 
+        forall j t,
+          arrives_in arr_seq j ->
+          ~~ can_be_preempted_for_model_with_limited_preemptions j (service sched j t) -> 
+          scheduled_at sched j t.      
+      
+    End Definitions.
+
+    (* In this section, we prove correctness of the model defined by 
+       function model_with_limited_preemptions. *)
+    Section Lemmas.
+
+      (* Consider any uniprocessor schedule with limited preemptions...*)
+      Variable sched: schedule Job.
+      Hypothesis H_is_schedule_with_limited_preemptions:
+        is_schedule_with_limited_preemptions sched.
+
+      (* ...where jobs do not execute after their completion. *)
+      Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute job_cost sched.
+
+      (* Next, we assume that preemption points are defined by the model with 
+         floating nonpreemptive regions. Note that the assumptions of the
+         model with floating nonpreemptive regions are a strict subset of
+         the assumptions of the model with fixed preemption points. This 
+         guaranties that the results below work for both models. *)
+      Variable task_max_nps: Task -> time.
+      Hypothesis H_limited_preemptions_job_model: limited_preemptions_job_model.
+      Hypothesis H_job_max_np_segment_le_task_max_np_segment:
+        job_max_np_segment_le_task_max_np_segment task_max_nps.
+
+      (* First, we prove a few basic auxiliary lemmas. *)
+      Section AuxiliaryLemmas.
+
+        (* Consider a job j. *)
+        Variable j: Job.
+        Hypothesis H_j_arrives: arrives_in arr_seq j.
+
+        (* We prove that the list of preemption points is not empty. *)
+        Lemma list_of_preemption_point_is_not_empty:
+          0 < size (job_preemption_points j).
+        Proof.
+          move: H_limited_preemptions_job_model => [EMPT [LS [BEG [END _]]]].
+          move: (posnP (job_cost j)) => [ZERO|POS].
+          { by specialize (EMPT j H_j_arrives ZERO); rewrite EMPT. }
+          apply/negPn/negP; rewrite -eqn0Ngt; intros CONTR; move: CONTR => /eqP CONTR.
+          move: (END _ H_j_arrives) => EQ.
+          move: EQ; rewrite /last -nth_last nth_default; last by rewrite CONTR.
+          intros.
+            by rewrite /job_cost_positive -EQ in POS.
+        Qed.
+
+        (* We prove that 0 is a preemption point. *)
+        Lemma zero_in_preemption_points: 0 \in job_preemption_points j.
+        Proof.
+          move: H_limited_preemptions_job_model => [EMPT [LS [BEG [END _]]]].
+          move: (BEG _ H_j_arrives) => EQ.
+          rewrite -EQ; clear EQ.
+          rewrite /first -nth0. 
+          apply/(nthP 0).
+          exists 0.
+          - by apply list_of_preemption_point_is_not_empty.
+          - by done.
+        Qed.
+
+        (* Next, we prove that the cost of a job is a preemption point. *)
+        Lemma job_cost_in_nonpreemptive_points: job_cost j \in job_preemption_points j.
+        Proof.
+          move: H_limited_preemptions_job_model => [EMPT [LS [BEG [END _]]]].
+          move: (END _ H_j_arrives) => EQ.
+          rewrite -EQ; clear EQ.
+          rewrite /last -nth_last.
+          apply/(nthP 0).
+          exists ((size (job_preemption_points j)).-1); last by done. 
+          rewrite -(leq_add2r 1) !addn1 prednK //.
+            by apply list_of_preemption_point_is_not_empty.
+        Qed.
+
+        (* As a corollary, we prove that the size of the sequence of nonpreemptive points is at least 2. *)
+        Corollary number_of_preemption_points_at_least_two: 2 <= size (job_preemption_points j).
+        Proof.
+          move: H_limited_preemptions_job_model => [EMPT [LS [BEG [END _]]]]. 
+          move: (posnP (job_cost j)) => [ZERO|POS].
+          { by specialize (EMPT j H_j_arrives ZERO); rewrite EMPT. }
+          have EQ: 2 = size [::0; job_cost j]; first by done. 
+          rewrite EQ; clear EQ.
+          apply subseq_leq_size.
+          rewrite !cons_uniq.
+          { apply/andP; split.
+            rewrite in_cons negb_or; apply/andP; split; last by done.
+            rewrite neq_ltn; apply/orP; left; eauto 2.
+            apply/andP; split; by done. } 
+          intros t EQ; move: EQ; rewrite !in_cons.
+          move => /orP [/eqP EQ| /orP [/eqP EQ|EQ]]; last by done.
+          - by rewrite EQ; apply zero_in_preemption_points.
+          - by rewrite EQ; apply job_cost_in_nonpreemptive_points.
+        Qed.
+
+      End AuxiliaryLemmas.
+      
+      (* We prove that the fixed_preemption_point_model function defines 
+         a correct preemption model. *)
+      Lemma model_with_fixed_preemption_points_is_correct:
+        correct_preemption_model arr_seq sched can_be_preempted_for_model_with_limited_preemptions.
+      Proof.
+        intros j ARR; split. 
+        { move => t NPP.
+            by apply H_is_schedule_with_limited_preemptions. }
+        { intros t NSCHED SCHED. 
+          have SERV: service sched j t = service sched j t.+1.
+          { rewrite -[service sched j t]addn0 /service /service_during; apply/eqP. 
+            rewrite big_nat_recr //=.
+            rewrite eqn_add2l eq_sym.
+              by rewrite /service_at eqb0. }
+          rewrite -[can_be_preempted_for_model_with_limited_preemptions _ _]Bool.negb_involutive.
+          apply/negP; intros CONTR.
+          move: NSCHED => /negP NSCHED; apply: NSCHED.
+          apply H_is_schedule_with_limited_preemptions; first by done.
+            by rewrite SERV.
+        }            
+      Qed.
+
+      (* Next we prove that the fixed_preemption_point_model function defines 
+         a model with bounded nonpremtive regions. *)
+      Lemma model_with_fixed_preemption_points_is_model_with_bounded_nonpreemptive_regions:
+        model_with_bounded_nonpreemptive_segments
+          job_cost job_task arr_seq can_be_preempted_for_model_with_limited_preemptions
+          job_max_nps task_max_nps. 
+      Proof.
+        intros j ARR.
+        move: H_limited_preemptions_job_model => [EMPT [LS [BEG [END NDEC]]]].
+        move: (posnP (job_cost j)) => [ZERO|POS]. 
+        { specialize (EMPT j ARR ZERO).
+          split; last split; last split.
+          - by rewrite /job_cannot_become_nonpreemptive_before_execution /can_be_preempted_for_model_with_limited_preemptions EMPT.
+          - by rewrite /job_cannot_be_nonpreemptive_after_completion /can_be_preempted_for_model_with_limited_preemptions EMPT ZERO.
+          - by intros _; rewrite /job_max_nps /lengths_of_segments EMPT /distances; simpl; rewrite subn0. 
+          - move => progr; rewrite ZERO leqn0; move => /andP [_ /eqP LE].
+            exists 0; rewrite LE; split.
+            + by apply/andP; split.
+            + by rewrite /can_be_preempted_for_model_with_limited_preemptions EMPT.
+        }
+        split; last split; last split.
+        { by rewrite /job_cannot_become_nonpreemptive_before_execution; eauto; apply zero_in_preemption_points. }
+        { by apply job_cost_in_nonpreemptive_points. }
+        { by intros ARR2; apply H_job_max_np_segment_le_task_max_np_segment. } 
+        { unfold nonpreemptive_regions_have_bounded_length, can_be_preempted_for_model_with_limited_preemptions.
+          move => progr /andP [_ LE]. 
+          specialize (NDEC j).
+          specialize (H_is_schedule_with_limited_preemptions j).
+          destruct (progr \in job_preemption_points j) eqn:NotIN.
+          { exists progr; split; first apply/andP; first split; try done.
+              by rewrite leq_addr. 
+          }
+          set (preemptions := job_preemption_points j).
+          set (serv := progr).
+          have Fact1: job_cost j <= last preemptions. 
+          { by apply last_is_max_in_nondecreasing_seq; eauto 2; apply job_cost_in_nonpreemptive_points. }
+          have Fact2: first preemptions <= serv < last preemptions.
+          { apply/andP; split.
+            - by rewrite /preemptions BEG.
+            - rewrite /serv /preemptions END; last by done.
+              rewrite ltn_neqAle; apply/andP; split; last by done.
+              apply/negP; intros CONTR; move: CONTR => /eqP CONTR.
+              rewrite CONTR in NotIN.
+              move: NotIN => /eqP; rewrite eqbF_neg; move => /negP NIN; apply: NIN.
+                by apply job_cost_in_nonpreemptive_points.
+          }
+          have EX: exists n,
+              n.+1 < size preemptions /\
+              nth 0 preemptions n < serv < nth 0 preemptions n.+1.
+          { intros.
+            move: (belonging_to_segment_of_seq_is_total
+                     preemptions serv (number_of_preemption_points_at_least_two _ ARR) Fact2) => [n [SIZE2 /andP [N1 N2]]].
+            exists n; split; first by done.
+            apply/andP; split; last by done.
+            move: N1; rewrite leq_eqVlt; move => /orP [/eqP EQ | G]; last by done.
+            exfalso.
+            move: NotIN => /negP CONTR; apply: CONTR.
+            unfold serv, fixed_preemption_points_model in *.
+            rewrite -EQ; clear EQ.
+            rewrite mem_nth //.
+              by apply ltnW.
+          }
+          move: EX => [x [SIZE2 /andP [N1 N2]]].
+          set ptl := nth 0 preemptions x.
+          set ptr := nth 0 preemptions x.+1.
+          exists ptr.
+          split.
+          { apply/andP; split.
+            { by apply ltnW. } 
+            {
+              apply leq_trans with (ptl + (job_max_nps j - ε) + 1).
+              { unfold job_max_nps.
+                rewrite -addnA -leq_subLR.
+                rewrite -(leq_add2r 1).
+                rewrite [in X in _ <= X]addnC -leq_subLR.                
+                rewrite !subn1 !addn1 prednK. 
+                { by rewrite -[_.+1.-1]pred_Sn; apply distance_between_neighboring_elements_le_max_distance_in_seq. }
+                { apply max_distance_in_nontrivial_seq_is_positive; first by eauto 2.
+                  exists 0, (job_cost j); repeat split. 
+                  - by apply zero_in_preemption_points.
+                  - by apply job_cost_in_nonpreemptive_points.
+                  - apply/eqP; rewrite eq_sym -lt0n. 
+                      by apply POS.
+                } 
+              } 
+              { rewrite addn1. rewrite ltn_add2r. apply N1. }
+            }
+          }
+          { by apply mem_nth. }
+        }         
+      Qed. 
+
+    End Lemmas. 
+      
+  End ModelsWithLimitedPreemptions.
+ 
+End ModelWithLimitedPreemptions.
\ No newline at end of file

model/schedule/uni/limited/platform/nonpreemptive.v

+Require Import rt.util.all.
+Require Import rt.model.arrival.basic.job
+               rt.model.arrival.basic.task 
+               rt.model.priority
+               rt.model.arrival.basic.task_arrival.
+Require Import rt.model.schedule.uni.schedule
+               rt.model.schedule.uni.service
+               rt.model.schedule.uni.basic.platform.
+Require Import rt.model.schedule.uni.nonpreemptive.schedule.
+Require Export rt.model.schedule.uni.limited.platform.definitions.
+
+From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
+
+(** * Platform for fully nonpreemptive model *)
+(** In module uni.limited.platform we introduce the notion of whether a job can be preempted 
+   at a given time (using a predicate can_be_preempted). In this section, we instantiate 
+   can_be_preempted for the fully nonpreemptive model and prove its correctness. *)
+Module FullyNonPreemptivePlatform.
+
+  Import Epsilon Job SporadicTaskset UniprocessorSchedule Priority
+         Service LimitedPreemptionPlatform.
+  
+  Section FullyNonPreemptiveModel.
+    
+    Context {Task: eqType}.
+    Variable task_cost: Task -> time.
+    
+    Context {Job: eqType}.
+    Variable job_arrival: Job -> time.
+    Variable job_cost: Job -> time.
+    Variable job_task: Job -> Task.
+
+    (* Consider any arrival sequence with consistent, non-duplicate arrivals. *)
+    Variable arr_seq: arrival_sequence Job.
+    Hypothesis H_arrival_times_are_consistent: arrival_times_are_consistent job_arrival arr_seq.
+    Hypothesis H_arr_seq_is_a_set: arrival_sequence_is_a_set arr_seq.
+    
+    (* Next, consider any uniprocessor nonpreemptive schedule of this arrival sequence...*)
+    Variable sched: schedule Job.
+    Hypothesis H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq.
+    Hypothesis H_nonpreemptive_sched:
+      NonpreemptiveSchedule.is_nonpreemptive_schedule job_cost sched.
+
+    (* ... where jobs do not execute before their arrival nor after completion. *)
+    Hypothesis H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute job_arrival sched.
+    Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute job_cost sched.
+    
+    (* For simplicity, let's define some local names. *)
+    Let job_pending := pending job_arrival job_cost sched.
+    Let job_completed_by := completed_by job_cost sched.
+    Let job_scheduled_at := scheduled_at sched.
+
+    (* Assume that a job cost cannot be larger than a task cost. *)
+    Hypothesis H_job_cost_le_task_cost:
+      cost_of_jobs_from_arrival_sequence_le_task_cost
+        task_cost job_cost job_task arr_seq.
+    
+    (* We say that the model is fully nonpreemptive 
+       iff every job cannot be preempted until its completion. *)
+    Definition can_be_preempted_for_fully_nonpreemptive_model (j: Job) (progr: time) :=
+      (progr == 0) || (progr == job_cost j).
+
+    (* Since in a fully nonpreemptive model a job cannot be preempted after 
+       it starts the execution, job_max_nps is equal to job_cost. *) 
+    Let job_max_nps (j: Job) := job_cost j.
+
+    (* In order to bound job_max_nps, task_max_nps should be equal to task_cost. *)
+    Let task_max_nps (tsk: Task) := task_cost tsk.
+    
+    (* Then, we prove that fully_nonpreemptive_model is a correct preemption model... *)
+    Lemma fully_nonpreemptive_model_is_correct:
+      correct_preemption_model arr_seq sched can_be_preempted_for_fully_nonpreemptive_model.
+    Proof.
+      intros j; split.
+      { move => t. 
+        rewrite /can_be_preempted_for_fully_nonpreemptive_model Bool.negb_orb -lt0n. 
+        move => /andP [POS NCOMPL].
+        unfold NonpreemptiveSchedule.is_nonpreemptive_schedule in *. 
+        move: (incremental_service_during _ _ _ _ _ POS) => [ft [/andP [_ LT] [SCHED SERV]]].
+        apply H_nonpreemptive_sched with ft.
+        { by apply ltnW. }
+        { by done. } 
+        { rewrite /completed_by neq_ltn; apply/orP; left.
+          move: NCOMPL; rewrite neq_ltn; move => /orP [LE|GE]; [by done | exfalso].
+          move: GE; rewrite ltnNge; move => /negP GE; apply: GE.
+            by eauto 2.
+        }
+      }
+      { intros t NSCHED SCHED.
+        rewrite /can_be_preempted_for_fully_nonpreemptive_model. 
+        apply/orP; left. 
+        apply/negP; intros CONTR. 
+        move: CONTR => /negP; rewrite -lt0n; intros POS. 
+        move: (incremental_service_during _ _ _ _ _ POS) => [ft [/andP [_ LT] [SCHEDn SERV]]].
+        move: NSCHED => /negP NSCHED; apply: NSCHED.
+        apply H_nonpreemptive_sched with ft.
+        { by rewrite -ltnS. }
+        { by done. }
+        { rewrite /completed_by neq_ltn; apply/orP; left.
+          apply leq_ltn_trans with (service sched j t.+1).  
+          { by rewrite /service /service_during big_nat_recr //= leq_addr. }
+          { rewrite -addn1.
+            apply leq_trans with (service sched j t.+2).
+            - unfold service, service_during.
+              have EQ: (service_at sched j t.+1) = 1.
+              { by apply/eqP; rewrite eqb1. }
+                by rewrite -EQ -big_nat_recr //=.
+            - by eauto 2.
+          }
+        } 
+      }
+    Qed.
+
+    (* ... and has bounded nonpreemptive regions. *)
+    Lemma fully_nonpreemptive_model_is_model_with_bounded_nonpreemptive_regions:
+      model_with_bounded_nonpreemptive_segments
+        job_cost job_task arr_seq can_be_preempted_for_fully_nonpreemptive_model job_max_nps task_max_nps.
+    Proof. 
+      have F: forall n, n = 0 \/ n > 0.
+      { by intros n; destruct n; [left | right]. }
+      intros j; split; last split; last split.
+      { by done. }
+      { by apply/orP; right. }
+      { intros ARR.
+        rewrite /job_max_nps /task_max_nps.
+          by eauto 2.
+      } 
+      { intros progr.
+        move: (F (progr)) => [EQ | GT].
+        { exists progr; split.
+          - by apply/andP; split; [done | rewrite leq_addr].
+          - by rewrite /can_be_preempted_for_fully_nonpreemptive_model EQ. }
+        { exists (maxn progr (job_cost j)).
+          have POS: 0 < job_cost j.
+          { by apply leq_trans with progr; last move: H0 => /andP [_ H0]. } 
+          split.
+          { apply/andP; split; first by rewrite leq_maxl. 
+            rewrite /job_max_nps addnBA; last eauto 2.
+            rewrite geq_max; apply/andP; split.
+            - rewrite -addnBA; last by eauto 2.
+                  by rewrite leq_addr.
+            - by rewrite addnC -addnBA // leq_addr.
+          }
+          { unfold can_be_preempted_for_fully_nonpreemptive_model.
+            apply/orP; right.
+            move: H0 => /andP [_ LE].
+            rewrite eqn_leq; apply/andP; split.
+            - by rewrite geq_max; apply/andP; split.
+            - by rewrite leq_max; apply/orP; right.
+          }
+        }
+      }
+    Qed.
+
+  End FullyNonPreemptiveModel.
+
+End FullyNonPreemptivePlatform.
\ No newline at end of file

model/schedule/uni/limited/platform/preemptive.v

+Require Import rt.util.all.
+Require Import rt.model.arrival.basic.job
+               rt.model.arrival.basic.task
+               rt.model.priority
+               rt.model.arrival.basic.task_arrival.
+Require Import rt.model.schedule.uni.schedule
+               rt.model.schedule.uni.service
+               rt.model.schedule.uni.basic.platform.
+Require Export rt.model.schedule.uni.limited.platform.definitions.
+
+From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
+
+(** * Platform for fully premptive model *)
+(** In module uni.limited.platform we introduce the notion of whether a job can be preempted 
+   at a given time (using a predicate can_be_preempted). In this section, we instantiate 
+   can_be_preempted for the fully preemptive model and prove its correctness. *)
+Module FullyPreemptivePlatform.
+
+  Import Epsilon Job SporadicTaskset UniprocessorSchedule Priority
+         Service LimitedPreemptionPlatform.
+  
+  Section FullyPreemptiveModel.
+    
+    Context {Task: eqType}.
+    
+    Context {Job: eqType}.
+    Variable job_arrival: Job -> time.
+    Variable job_cost: Job -> time.
+    Variable job_task: Job -> Task.
+
+    (* Consider any job arrival sequence ...*)
+    Variable arr_seq: arrival_sequence Job.
+    
+    (* ...and any uniprocessor schedule of these jobs. *)  
+    Variable sched: schedule Job. 
+
+    (* For simplicity, let's define some local names. *)
+    Let job_pending := pending job_arrival job_cost sched.
+    Let job_completed_by := completed_by job_cost sched.
+    Let job_scheduled_at := scheduled_at sched.
+
+    (* In the fully preemptive model any job can be preempted at any time. *)
+    Definition can_be_preempted_for_fully_preemptive_model (j: Job) (progr: time) := true.
+    
+    (* Since in a fully preemptive model a job can be preempted at 
+       any time job_max_nps cannot be greater than ε. *) 
+    Let job_max_nps (j: Job) := ε.
+
+    (*  In order to bound job_max_nps, we can choose task_max_nps that is equal to ε for any task. *)
+    Let task_max_nps (tsk: Task) := ε.
+    
+    (* Then, we prove that fully_preemptive_model is a correct preemption model... *)
+    Lemma fully_preemptive_model_is_correct:
+      correct_preemption_model arr_seq sched can_be_preempted_for_fully_preemptive_model.
+    Proof. by intros j; split; intros t CONTR. Qed.
+
+    (* ... and has bounded nonpreemptive regions. *)
+    Lemma fully_preemptive_model_is_model_with_bounded_nonpreemptive_regions:
+      model_with_bounded_nonpreemptive_segments
+        job_cost job_task arr_seq can_be_preempted_for_fully_preemptive_model job_max_nps task_max_nps.
+    Proof.
+      intros j; repeat split; try done. 
+      intros t; exists t; split.
+      { by apply/andP; split; [ done | rewrite subnn addn0]. }
+      { by done. }
+    Qed.
+
+  End FullyPreemptiveModel.
+
+End FullyPreemptivePlatform.
\ No newline at end of file

model/schedule/uni/limited/platform/priority_inversion_is_bounded.v

+Require Import rt.util.all.
+Require Import rt.model.arrival.basic.job
+               rt.model.arrival.basic.task_arrival
+               rt.model.priority.
+Require Import rt.model.schedule.uni.service
+               rt.model.schedule.uni.schedule.
+Require Import rt.model.schedule.uni.limited.platform.definitions
+               rt.model.schedule.uni.limited.busy_interval.
+
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
+
+(** * Priority inversion is bounded *)
+(** In this module we prove that any priority inversion that occurs in the model with bounded 
+    nonpreemptive segments defined in module rt.model.schedule.uni.limited.platform.definitions 
+    is bounded. *)
+Module PriorityInversionIsBounded.
+
+  Import Epsilon Job Priority UniprocessorSchedule LimitedPreemptionPlatform BusyIntervalJLFP. 
+
+  Section PriorityInversionIsBounded.
+
+    Context {Task: eqType}.
+    Variable task_max_nps task_cost: Task -> time.    
+    
+    Context {Job: eqType}.
+    Variable job_arrival: Job -> time.
+    Variable job_max_nps job_cost: Job -> time.
+    Variable job_task: Job -> Task.
+    
+    (* Consider any arrival sequence. *)
+    Variable arr_seq: arrival_sequence Job.
+    Hypothesis H_arrival_times_are_consistent: arrival_times_are_consistent job_arrival arr_seq.
+    
+    (* Next, consider any uniprocessor schedule of this arrival sequence...*)
+    Variable sched: schedule Job.
+    Hypothesis H_jobs_come_from_arrival_sequence: jobs_come_from_arrival_sequence sched arr_seq.
+
+    (* ... where jobs do not execute before their arrival nor after completion. *)
+    Hypothesis H_jobs_must_arrive_to_execute: jobs_must_arrive_to_execute job_arrival sched.
+    Hypothesis H_completed_jobs_dont_execute: completed_jobs_dont_execute job_cost sched. 
+    
+    (* Consider a JLFP policy that indicates a higher-or-equal priority relation,
+       and assume that the relation is reflexive and transitive. *)
+    Variable higher_eq_priority: JLFP_policy Job.
+    Hypothesis H_priority_is_reflexive: JLFP_is_reflexive higher_eq_priority.
+    Hypothesis H_priority_is_transitive: JLFP_is_transitive higher_eq_priority.
+
+    (* We consider an arbitrary function can_be_preempted which defines 
+       a preemption model with bounded nonpreemptive segments. *)
+    Variable can_be_preempted: Job -> time -> bool.
+    Let preemption_time := preemption_time sched can_be_preempted.
+    Hypothesis H_correct_preemption_model:
+      correct_preemption_model arr_seq sched can_be_preempted.
+    Hypothesis H_model_with_bounded_nonpreemptive_segments:
+      model_with_bounded_nonpreemptive_segments
+        job_cost job_task arr_seq can_be_preempted job_max_nps task_max_nps. 
+
+    (* Next, we assume that the schedule is a work-conserving schedule... *)
+    Hypothesis H_work_conserving: work_conserving job_arrival job_cost arr_seq sched.
+
+    (* ... and the schedule respects the policy defined by the 
+       can_be_preempted function (i.e., bounded nonpreemptive segments). *)
+    Hypothesis H_respects_policy:
+      respects_JLFP_policy_at_preemption_point
+        job_arrival job_cost arr_seq sched can_be_preempted higher_eq_priority.
+
+    (* Let's define some local names for clarity. *)
+    Let job_scheduled_at := scheduled_at sched.
+    Let job_completed_by := completed_by job_cost sched.
+
+    (* Finally, we introduce the notion of the maximal length of (potential) priority 
+       inversion at a time instant t, which is defined as the maximum length of 
+       nonpreemptive segments among all jobs that arrived so far. Note that 
+       the value [job_max_nps j_lp] is at least ε for any job j_lp, so the maximal
+       length of priority inversion cannot be negative. *)
+    Definition max_length_of_priority_inversion (j: Job) (t: time) :=
+      \max_(j_lp <- jobs_arrived_before arr_seq t | ~~ higher_eq_priority j_lp j)
+       (job_max_nps j_lp - ε).
+
+    (** Next we prove that a priority inversion of a job is bounded by 
+        function max_length_of_priority_inversion. *)
+
+    (** Note that any bound on function max_length_of_priority_inversion will also be 
+        a bound on the maximal priority inversion. This bound may be different 
+        for different scheduler and/or task models. Thus, we don't define such a bound 
+        in this module. *)
+
+    (* Consider any job j of tsk with positive job cost. *)
+    Variable j: Job.
+    Hypothesis H_j_arrives: arrives_in arr_seq j.
+    Hypothesis H_job_cost_positive: job_cost_positive job_cost j.
+    
+    (* Consider any busy interval prefix [t1, t2) of job j. *)
+    Variable t1 t2: time.
+    Hypothesis H_busy_interval_prefix:
+      busy_interval_prefix job_arrival job_cost arr_seq sched higher_eq_priority j t1 t2.
+    
+    (* In this section, we prove that at any time instant after any preemption point
+       (inside the busy interval), the processor is always busy scheduling a 
+       job with higher or equal priority. *)
+    Section PreemptionTimeAndPriorityInversion. 
+      
+      (* First, we show that the processor at any preemptive point is always 
+         busy scheduling a job with higher or equal priority. *)
+      Lemma not_quiet_implies_exists_scheduled_hp_job_at_preemption_point:
+        forall t, 
+          t1 <= t < t2 ->
+          preemption_time t ->
+          exists j_hp,
+            arrived_between job_arrival j_hp t1 t2 /\
+            higher_eq_priority j_hp j /\
+            job_scheduled_at j_hp t.
+      Proof.
+        move: (H_busy_interval_prefix) => [SL [QUIET [NOTQUIET INBI]]].
+        rename H_work_conserving into WORK, H_respects_policy into PRIO,
+        H_jobs_come_from_arrival_sequence into CONS.
+        move => t /andP [GEt LEt] PREEMPTP.            
+        have NOTIDLE := not_quiet_implies_not_idle
+                          job_arrival job_cost arr_seq _
+                          sched higher_eq_priority j _ _ _ _ _ _ t1 t2 _ t.
+        feed_n 9 NOTIDLE; eauto 2.
+        unfold is_idle, FP_is_transitive, transitive in *.
+        destruct (sched t) as [j_hp|] eqn:SCHED; [clear NOTIDLE | by exfalso; apply NOTIDLE].
+        move: SCHED => /eqP SCHED.
+        exists j_hp.
+        have HP: higher_eq_priority j_hp j.
+        { apply contraT; move => /negP NOTHP; exfalso.
+          have TEMP: t <= t2.-1; first by rewrite -subn1 subh3 //; [by rewrite addn1 | by apply leq_ltn_trans with t1].
+          rewrite leq_eqVlt in TEMP; move: TEMP => /orP [/eqP EQUALt2m1 | LTt2m1];
+                                                    first rewrite leq_eqVlt in GEt; first move: GEt => /orP [/eqP EQUALt1 | LARGERt1].
+          { subst t; clear LEt.
+            rewrite -EQUALt1 in SCHED; move: EQUALt1 => /eqP EQUALt1.
+            destruct (job_scheduled_at j t1) eqn:SCHEDj.
+            { simpl. have EQ:= only_one_job_scheduled sched j j_hp t1 SCHEDj SCHED.
+                by subst j; apply NOTHP. 
+            }
+            { apply NOTHP.
+              apply PRIO with t1; try done.
+              - by move: EQUALt1 => /eqP EQUALt1; rewrite EQUALt1.
+              - apply/andP; split; last first.
+                + by move: SCHEDj; rewrite /job_scheduled_at; move => /negP /negP SCHEDj.
+                + have EQ: t1 = job_arrival j.
+                  { rewrite -eqSS in EQUALt1.
+                    have EQ: t2 = t1.+1.
+                    { rewrite prednK in EQUALt1; first by apply/eqP; rewrite eq_sym.
+                      apply negbNE; rewrite -eqn0Ngt; apply/neqP; intros EQ0.
+                      move: INBI; rewrite EQ0; move => /andP [_ CONTR].
+                        by rewrite ltn0 in CONTR.
+                    } clear EQUALt1.
+                      by move: INBI; rewrite EQ ltnS -eqn_leq; move => /eqP INBI.
+                  }
+                    by rewrite EQ; eapply job_pending_at_arrival; eauto 2.
+            } 
+          }
+          { feed (NOTQUIET t); first by apply/andP; split.
+            apply NOTQUIET; intros j_hp' IN HP ARR.
+            apply contraT; move => /negP NOTCOMP'; exfalso.
+            have BACK: backlogged job_arrival job_cost sched j_hp' t.
+            { apply/andP; split.
+              - apply/andP; split. unfold arrived_before, has_arrived in *. by rewrite ltnW. 
+                apply/negP; intro COMP; apply NOTCOMP'.
+                  by apply completion_monotonic with (t0 := t).
+              - apply/negP; intro SCHED'.
+                apply only_one_job_scheduled with (j1 := j_hp) in SCHED'; last by done.
+                  by apply NOTHP; subst. 
+            }
+            feed (PRIO j_hp' j_hp t PREEMPTP IN BACK); first by done.
+              by apply NOTHP; apply H_priority_is_transitive with j_hp'. 
+          }
+          {
+            unfold quiet_time in *.
+            feed (NOTQUIET t.+1). apply/andP; split.
+            - by apply leq_ltn_trans with t1.
+            - rewrite -subn1 ltn_subRL addnC in LTt2m1.
+                by rewrite -[t.+1]addn1.
+                apply NOTQUIET.
+                unfold quiet_time in *; intros j_hp' IN HP ARR.
+                apply contraT; move => /negP NOTCOMP'; exfalso.
+                have BACK: backlogged job_arrival job_cost sched j_hp' t.
+                { apply/andP; split; last first.
+                  { apply/negP; intro SCHED'.
+                    apply only_one_job_scheduled with (j1 := j_hp) in SCHED'; last by done.
+                    apply NOTHP.
+                      by subst. 
+                  }
+                  apply/andP; split. unfold arrived_before, has_arrived in *. by done. 
+                  apply/negP; intro COMP; apply NOTCOMP'.
+                    by apply completion_monotonic with (t0 := t).
+                }
+                feed (PRIO j_hp' j_hp t PREEMPTP IN BACK); first by done.
+                  by apply NOTHP; apply H_priority_is_transitive with j_hp'. 
+          }
+        }
+        repeat split; [| by done | by done].
+        move: (SCHED) => PENDING.
+        eapply scheduled_implies_pending with (job_cost0 := job_cost) in PENDING; [| by eauto | by done].
+        apply/andP; split; last by apply leq_ltn_trans with (n := t); first by move: PENDING => /andP [ARR _]. 
+        apply contraT; rewrite -ltnNge; intro LT; exfalso.
+        feed (QUIET j_hp); first by eapply CONS, SCHED.
+        specialize (QUIET HP LT).
+        have COMP: job_completed_by j_hp t by apply completion_monotonic with (t0 := t1).
+        apply completed_implies_not_scheduled in COMP; last by done.
+          by move: COMP => /negP COMP; apply COMP.
+      Qed.
+
+      (* In addition, we prove that every nonpreemptive segment 
+         always begins with a preemption time. *)
+      Lemma scheduling_of_any_segment_starts_with_preemption_time: 
+        forall j t,
+          job_scheduled_at j t ->
+          exists pt,
+            job_arrival j <= pt <= t /\
+            preemption_time pt /\
+            (forall t', pt <= t' <= t -> job_scheduled_at j t').
+      Proof. 
+        intros s t SCHEDst.
+        have EX: exists t',
+            (t' <= t)
+              && (job_scheduled_at s t')
+              && (all (fun t'' => job_scheduled_at s t'') (iota t' (t - t').+1 )).
+        { exists t.
+          apply/andP; split; [ by apply/andP; split | ].
+          apply/allP; intros t'.
+          rewrite mem_iota.
+          rewrite subnn addn1 ltnS -eqn_leq.
+            by move => /eqP EQ; subst t'. } 
+        have MIN := ex_minnP EX. 
+        move: MIN => [mpt /andP [/andP [LT1 SCHEDsmpt] /allP ALL] MIN]; clear EX.
+        destruct mpt.
+        { exists 0; repeat split.
+          - apply/andP; split; last by done.
+              by apply H_jobs_must_arrive_to_execute in SCHEDsmpt.
+          - by eapply zero_is_pt; eauto 2.
+          - by intros; apply ALL; rewrite mem_iota subn0 add0n ltnS. }
+        { have NSCHED: ~~ job_scheduled_at s mpt.
+          { apply/negP; intros SCHED. 
+            feed (MIN mpt).
+            apply/andP; split; [by apply/andP; split; [ apply ltnW | ] | ].
+            apply/allP; intros t'.
+            rewrite mem_iota addnS ltnS. 
+            move => /andP [GE LE].
+            move: GE; rewrite leq_eqVlt; move => /orP [/eqP EQ| LT].
+            subst t'. by done.
+            apply ALL.
+            rewrite mem_iota addnS ltnS.
+            apply/andP; split; first by done.
+            apply leq_trans with (mpt + (t - mpt)); first by done.
+            rewrite !subnKC; last rewrite ltnW; by done.
+              by rewrite ltnn in MIN. }
+          have PP: preemption_time mpt.+1.
+          { apply first_moment_is_pt with (arr_seq0 := arr_seq) (j0 := s); eauto 2. }
+          exists mpt.+1; repeat split; try done.
+          - apply/andP; split; last by done.
+              by apply H_jobs_must_arrive_to_execute in SCHEDsmpt.
+          - move => t' /andP [GE LE].
+            apply ALL; rewrite mem_iota.
+            rewrite addnS ltnS subnKC; last by done.
+              by apply/andP; split.
+        }
+      Qed. 
+      
+      (* Next we prove that at any time instant after a preemption point the
+         processor is always busy with a job with higher or equal priority. *) 
+      Lemma not_quiet_implies_exists_scheduled_hp_job_after_preemption_point:
+        forall tp t,
+          preemption_time tp ->
+          t1 <= tp < t2 ->
+          tp <= t < t2 ->
+          exists j_hp,
+            arrived_between job_arrival j_hp t1 t.+1 /\ 
+            higher_eq_priority j_hp j /\
+            job_scheduled_at j_hp t.
+      Proof.
+        move: (H_jobs_come_from_arrival_sequence) (H_work_conserving) => CONS WORK.
+        move: (H_respects_policy) => PRIO.              
+        move => tp t PRPOINT /andP [GEtp LTtp] /andP [LEtp LTt].
+        have NOTIDLE := not_quiet_implies_not_idle
+                          job_arrival job_cost arr_seq _ sched higher_eq_priority
+                          j _ _ _ _ _ _ t1 t2 _ t.
+        feed_n 9 NOTIDLE; eauto 2.
+        apply/andP; split; [by apply leq_trans with tp | by done].
+        destruct (sched t) as [j_hp|] eqn:SCHED;
+          last by exfalso; apply NOTIDLE; rewrite /is_idle SCHED.
+        move: SCHED => /eqP SCHED.
+        exists j_hp.
+        have HP: higher_eq_priority j_hp j.
+        { intros.
+          have SOAS := scheduling_of_any_segment_starts_with_preemption_time _ _ SCHED.
+          move: SOAS => [prt [/andP [_ LE] [PR SCH]]].
+          case E:(t1 <= prt).
+          - move: E => /eqP /eqP E; rewrite subn_eq0 in E.
+            have EXISTS := not_quiet_implies_exists_scheduled_hp_job_at_preemption_point prt.
+            feed_n 2 EXISTS; try done.
+            { by apply /andP; split; last by apply leq_ltn_trans with t. }
+            move: EXISTS => [j_lp [_ [HEP SCHEDjhp]]].
+            have EQ: j_hp = j_lp.
+            { by apply (only_one_job_scheduled sched _ _ prt); first (apply SCH; apply/andP; split). }
+              by subst j_hp. 
+          - move: E => /eqP /neqP E; rewrite -lt0n subn_gt0 in E.
+            apply negbNE; apply/negP; intros LP.
+            rename j_hp into j_lp.
+            have EXISTS := not_quiet_implies_exists_scheduled_hp_job_at_preemption_point tp.
+            feed_n 2 EXISTS; try done.
+            { by apply /andP; split. }
+            move: EXISTS => [j_hp [_ [HEP SCHEDjhp]]].
+            have EQ: j_hp = j_lp.
+            { apply (only_one_job_scheduled sched _ _ tp). 
+                by done.
+                apply SCH; apply/andP; split.
+                apply leq_trans with t1. rewrite ltnW //. by done.
+                  by done.
+            }
+              by subst j_hp; move: LP => /negP LP; apply: LP.
+        } 
+        repeat split; [| by done | by done].
+        move: (H_busy_interval_prefix) => [SL [QUIET [NOTQUIET EXj]]]. 
+        move: (SCHED) => PENDING.
+        eapply scheduled_implies_pending with (job_cost0 := job_cost) in PENDING;
+          [| by eauto | by done].
+        apply/andP; split; 
+          last by apply leq_ltn_trans with (n := t); first by move: PENDING => /andP [ARR _].
+        apply contraT; rewrite -ltnNge; intro LT; exfalso.
+        feed (QUIET j_hp); first by eapply CONS, SCHED.
+        specialize (QUIET HP LT).
+        have COMP: job_completed_by j_hp t.
+        { by apply completion_monotonic with (t0 := t1); [ | apply leq_trans with tp | ]. }
+        apply completed_implies_not_scheduled in COMP; last by done.
+          by move: COMP => /negP COMP; apply COMP.
+      Qed.
+
+      (* Now, suppose there exists some constant K that bounds the distance to 
+         a preemption time from the beginning of the busy interval. *)
+      Variable K: time.
+      Hypothesis H_preemption_time_exists:
+        exists pr_t, preemption_time pr_t /\ t1 <= pr_t <= t1 + K.
+
+      (* Then we prove that the processor is always busy with a job with 
+         higher-or-equal priority after time instant [t1 + K]. *)
+      Lemma not_quiet_implies_exists_scheduled_hp_job:
+        forall t,
+          t1 + K <= t < t2 ->
+          exists j_hp,
+            arrived_between job_arrival j_hp t1 t.+1 /\ 
+            higher_eq_priority j_hp j /\
+            job_scheduled_at j_hp t.
+      Proof. 
+        move => t /andP [GE LT].
+        move: H_preemption_time_exists => [prt [PR /andP [GEprt LEprt]]].
+        apply not_quiet_implies_exists_scheduled_hp_job_after_preemption_point with (tp := prt); eauto 2. 
+        -  apply/andP; split; first by done.
+           apply leq_ltn_trans with (t1 + K); first by done.
+             by apply leq_ltn_trans with t.
+        - apply/andP; split; last by done.
+            by apply leq_trans with (t1 + K).
+      Qed.
+      
+    End PreemptionTimeAndPriorityInversion.
+
+    (* In this section we prove that the function max_length_of_priority_inversion 
+       indeed upper bounds the priority inversion length. *)
+    Section PreemprionTimeExists.
+
+      (* First we prove that if a job with higher-or-equal priority is scheduled at 
+         a quiet time t+1 then this is the first time when this job is scheduled. *)
+      Lemma hp_job_not_scheduled_before_quiet_time:
+        forall jhp t,
+          quiet_time job_arrival job_cost arr_seq sched higher_eq_priority j t.+1 ->
+          job_scheduled_at jhp t.+1 ->
+          higher_eq_priority jhp j ->
+          ~~ job_scheduled_at jhp t.
+      Proof.
+        intros jhp t QT SCHED1 HP.            
+        apply/negP; intros SCHED2.
+        specialize (QT jhp).
+        feed_n 3 QT; try done.
+        eapply H_jobs_come_from_arrival_sequence; eauto 1.
+        rewrite /arrived_before ltnS.
+        apply H_jobs_must_arrive_to_execute. by done.
+        apply completed_implies_not_scheduled in QT; last by done.
+          by move: QT => /negP NSCHED; apply: NSCHED.
+      Qed.
+      
+      (* Also, we show that lower-priority jobs that are scheduled inside the
+         busy-interval prefix [t1,t2) must have arrived before that interval. *)
+      Lemma low_priority_job_arrives_before_busy_interval_prefix:
+        forall jlp t,
+          t1 <= t < t2 ->
+          job_scheduled_at jlp t ->
+          ~~ higher_eq_priority jlp j ->
+          job_arrival jlp < t1.
+      Proof.
+        move => jlp t /andP [GE LT] SCHED LP.
+        move: (H_busy_interval_prefix) => [NEM [QT [NQT HPJ]]].
+        apply negbNE; apply/negP; intros ARR; rewrite -leqNgt in ARR.
+        have SCH:= scheduling_of_any_segment_starts_with_preemption_time _ _ SCHED.
+        move: SCH => [pt [/andP [NEQ1 NEQ2] [PT FA]]].
+        have NEQ: t1 <= pt < t2.
+        { apply/andP; split.
+          apply leq_trans with (job_arrival jlp); by done.
+          apply leq_ltn_trans with t; by done. }
+        have LL:= not_quiet_implies_exists_scheduled_hp_job_at_preemption_point pt.
+        feed_n 2 LL; try done.
+        move: LL => [jhp [ARRjhp [HP SCHEDhp]]].
+        feed (FA pt). apply/andP; split; by done.
+        have OOJ:= only_one_job_scheduled _ _ _ _ FA SCHEDhp; subst jhp.
+          by move: LP => /negP LP; apply: LP.
+      Qed.
+
+      (* Moreover, we show that lower-priority jobs that are scheduled inside the
+         busy-interval prefix [t1,t2) must be scheduled before that interval. *)
+      Lemma low_priority_job_scheduled_before_busy_interval_prefix:
+        forall jlp t,
+          t1 <= t < t2 ->
+          job_scheduled_at jlp t ->
+          ~~ higher_eq_priority jlp j ->
+          exists t', t' < t1 /\ job_scheduled_at jlp t'.
+      Proof.
+        move => jlp t NEQ SCHED LP.
+        have ARR := low_priority_job_arrives_before_busy_interval_prefix _ _ NEQ SCHED LP. 
+        move: NEQ => /andP [GE LT].
+        exists t1.-1.
+        split.
+        { rewrite prednK; first by done.
+            by apply leq_ltn_trans with (job_arrival jlp).
+        }
+        { move: (H_busy_interval_prefix) => [NEM [QT [NQT HPJ]]].
+          have SCHEDST := scheduling_of_any_segment_starts_with_preemption_time _ _ SCHED.
+          move: SCHEDST => [pt [NEQpt [PT SCHEDc]]].
+          have NEQ: pt < t1.
+          { rewrite ltnNge; apply/negP; intros CONTR.
+            have NQSCHED := not_quiet_implies_exists_scheduled_hp_job_at_preemption_point pt.
+            feed_n 2 NQSCHED; try done.
+            { apply/andP; split; first by done.
+                by apply leq_ltn_trans with t; move: NEQpt => /andP [_ T].
+            }
+            move: NQSCHED => [jhp [ARRhp [HPhp SCHEDhp]]].
+            specialize (SCHEDc pt).
+            feed SCHEDc.
+            { by apply/andP; split; last move: NEQpt => /andP [_ T]. }
+            have EQ:= only_one_job_scheduled sched jhp jlp pt.
+            feed_n 2 EQ; try done.
+            subst jhp.
+              by move: LP => /negP LP; apply: LP.
+          }
+          apply SCHEDc; apply/andP; split.
+          - rewrite -addn1 in NEQ.
+            apply subh3_ext in NEQ.
+              by rewrite subn1 in NEQ.
+          - apply leq_trans with t1. by apply leq_pred. by done.
+        }
+        Qed.
+      
+      (* Thus, there must be a preemption time in the interval [t1, t1 + max_priority_inversion t1]. 
+         That is, if a job with higher-or-equal priority is scheduled at time instant t1, then t1 is 
+         a preemprion time. Otherwise, if a job with lower priority is scheduled at time t1, 
+         then this jobs also should be scheduled before the beginning of the busy interval. So, the 
+         next preemption time will be no more than [max_priority_inversion t1] time units later. *)
+      Lemma preemption_time_exists: 
+        exists pr_t,
+          preemption_time pr_t /\
+          t1 <= pr_t <= t1 + max_length_of_priority_inversion j t1.
+      Proof.
+        set (service := service sched).
+        move: (H_correct_preemption_model) => CORR.
+        move: (H_busy_interval_prefix) => [NEM [QT1 [NQT HPJ]]].
+        case SCHED: (sched t1) => [s | ]; move: SCHED => /eqP SCHED; last first. 
+        { exists t1; split; last first.
+          apply/andP; split; [by done | by rewrite leq_addr].
+          move: SCHED => /eqP SCHED.
+          rewrite /preemption_time /LimitedPreemptionPlatform.preemption_time.
+            by rewrite SCHED.
+        }
+        { case PRIO: (higher_eq_priority s j).
+          { exists t1; split; last first.
+            apply/andP; split; [by done | by rewrite leq_addr].
+            destruct t1.
+            { eapply zero_is_pt; [eauto 2 | apply H_jobs_come_from_arrival_sequence]. }
+            eapply hp_job_not_scheduled_before_quiet_time in QT1; eauto 2.
+            eapply first_moment_is_pt with (j0 := s); eauto 2.
+          } 
+          { move: (SCHED) => ARRs; apply H_jobs_come_from_arrival_sequence in ARRs.
+            move: (H_model_with_bounded_nonpreemptive_segments s ARRs) => [_ [_ [_ EXPP]]].
+            move: (EXPP (service s t1)) => PP; clear EXPP.
+            feed PP. by apply/andP; split; [done | apply H_completed_jobs_dont_execute].                
+            have EX: exists pt,
+                ((service s t1) <= pt <= (service s t1) + (job_max_nps s - 1))
+                  && can_be_preempted s pt.
+            { move: PP => [pt [NEQ PP]].
+              exists pt; apply/andP; split; by done.
+            } clear PP. 
+            have MIN := ex_minnP EX.
+            move: MIN => [sm_pt /andP [NEQ PP] MIN]; clear EX.
+            have Fact: exists Δ, sm_pt = service s t1 + Δ.
+            { exists (sm_pt - service s t1).
+              apply/eqP; rewrite eq_sym; apply/eqP; rewrite subnKC //.
+                by move: NEQ => /andP [T _]. }
+            move: Fact => [Δ EQ]; subst sm_pt; rename Δ into sm_pt.
+            exists (t1 + sm_pt); split.
+            { have Fact1: 
+                forall prog, service s t1 <= prog < service s t1 + sm_pt ->
+                        ~~ can_be_preempted s prog. 
+              { move => prog /andP [GE LT].
+                apply/negP; intros PPJ.
+                feed (MIN prog); first (apply/andP; split); try done.
+                - apply/andP; split; first by done.
+                  apply leq_trans with (service s t1 + sm_pt).
+                  + by apply ltnW. 
+                  + by move: NEQ => /andP [_ K].
+                - by move: MIN; rewrite leqNgt; move => /negP NLT; apply: NLT.
+              } 
+              have Fact2: forall t', t1 <= t' < t1 + sm_pt -> job_scheduled_at s t'.
+              { 
+                move => t' /andP [GE LT]. 
+                have Fact: exists Δ, t' = t1 + Δ.
+                { by exists (t' - t1); apply/eqP; rewrite eq_sym; apply/eqP; rewrite subnKC.  }
+                move: Fact => [Δ EQ]; subst t'.
+                move: (Fact1 (service s (t1 + Δ)))(CORR s) => NPPJ T.
+                feed T; first by done. move: T => [T _ ].
+                apply: T; apply: NPPJ.
+                apply/andP; split.
+                { by apply Service.service_monotonic; rewrite leq_addr. }
+                rewrite /service /UniprocessorSchedule.service (@Service.service_during_cat _ _ _ t1).
+                { rewrite ltn_add2l; rewrite ltn_add2l in LT.
+                  apply leq_ltn_trans with Δ; last by done.
+                  rewrite -{2}(sum_of_ones t1 Δ).
+                  rewrite leq_sum //; clear; intros t _.
+                    by rewrite /service_at; destruct (scheduled_at sched s t). }
+                { by apply/andP; split; [done | rewrite leq_addr]. } 
+              }
+              rewrite /preemption_time /LimitedPreemptionPlatform.preemption_time.
+              case SCHEDspt: (sched (t1 + sm_pt)) => [s0 | ]; last by done.
+              move: SCHEDspt => /eqP SCHEDspt.
+              destruct (s == s0) eqn: EQ.
+              { move: EQ => /eqP EQ; subst s0.
+                rewrite /UniprocessorSchedule.service.
+                rewrite (@Service.service_during_cat _ _ _ t1); last first.
+                { by apply/andP; split; [ done | rewrite leq_addr]. }
+                have ALSCHED: service_during sched s t1 (t1 + sm_pt) = sm_pt.
+                { rewrite -{2}(sum_of_ones t1 sm_pt) /service_during.
+                  apply/eqP; rewrite eqn_leq //; apply/andP; split.
+                  { rewrite leq_sum //; clear; intros t _.
+                      by unfold service_at; destruct (scheduled_at sched s t). }
+                  { rewrite big_nat_cond [in X in _ <= X]big_nat_cond.
+                    rewrite leq_sum //.
+                    move => x /andP [HYP _].
+                    rewrite lt0b. 
+                      by apply Fact2.
+                  } 
+                } 
+                  by rewrite ALSCHED.
+              } 
+              destruct sm_pt.
+              { exfalso; move: EQ => /negP EQ; apply: EQ.
+                move: SCHED SCHEDspt => /eqP SCHED /eqP SCHEDspt.
+                rewrite addn0 in SCHEDspt; rewrite SCHEDspt in SCHED.
+                  by inversion SCHED. }
+              { rewrite addnS.
+                move: (H_correct_preemption_model s0) => T.
+                feed T; first by eauto 2. move: T => [_ T]; apply: T.
+                apply /negP; intros CONTR.
+                move: EQ => /negP EQ; apply: EQ.
+                move: (Fact2 (t1 + sm_pt)) => SCHEDs0.
+                feed SCHEDs0; first by apply/andP; split; [rewrite leq_addr | rewrite addnS].
+                apply/eqP; eapply only_one_job_scheduled; eauto 2.
+                  by rewrite -addnS.
+              } 
+            } 
+            move: NEQ => /andP [GE LE].
+            apply/andP; split; first by rewrite leq_addr.
+            rewrite leq_add2l.
+            unfold max_length_of_priority_inversion.
+            rewrite (big_rem s) //=.
+            { rewrite PRIO; simpl.
+              apply leq_trans with (job_max_nps s - ε); last by rewrite leq_maxl.
+                by rewrite leq_add2l in LE. }
+            eapply arrived_between_implies_in_arrivals; eauto 2.
+            apply/andP; split; first by done.
+            eapply low_priority_job_arrives_before_busy_interval_prefix with t1; eauto 2.
+              by rewrite PRIO.
+          }
+        }
+      Qed.
+
+    End PreemprionTimeExists.
+
+  End PriorityInversionIsBounded. 
+  
+End PriorityInversionIsBounded.
\ No newline at end of file

model/schedule/uni/limited/platform/util.v

+Require Import rt.util.all.
+
+From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
+
+(** * Non-decreasing sequence *)
+(** In this module we introduce the notion of a non-decreasing sequence
+     that will be used to describe preemption points in models with limited preemptions. *)
+Module NondecreasingSequence.
+
+  (* First, let's introduce the notion of the nth element of a sequence. *)
+  Notation "xs [| n |]" := (nth 0 xs n) (at level 30).
+  
+  (* In this section we provide the notion of a non-decreasing sequence. *)
+  Section Definitions. 
+    
+    (* We say that a sequence xs is non-decincreasing iff for any two indices n1 and n2 
+       such that [n1 <= n2 < size xs] the following condition holds: xs[n1] <= xs[n2]. *)
+    Definition nondecreasing_sequence (xs: seq nat) :=
+      forall n1 n2,
+        n1 <= n2 < size xs ->
+        nth 0 xs n1 <= nth 0 xs n2.
+
+    (* For a non-decreasing sequence we define the notion of 
+       distances between neighboring elements of the sequence. *)
+    (* Example:
+       Consider the following sequence of natural numbers: xs = [:: 1; 10; 10; 17; 20; 41]. 
+       Then [drop 1 xs] is equal to [:: 10; 10; 17; 20; 41].
+       Then [zip xs (drop 1 xs)] is equal to [:: (1,10); (10,10); (10,17); (17,20); (20,41)]
+       And after the mapping [map (fun '(x1, x2) => x2 - x1)] we end up with [:: 9; 0; 7; 3; 21]. *)
+    Definition distances (xs: seq nat) :=
+      map (fun '(x1, x2) => x2 - x1) (zip xs (drop 1 xs)).
+
+    (* Next, we define some common operations on lists. 
+       Namely max, first, and last. *)
+    Definition max := foldl maxn 0.
+    Definition first := head 0.
+    Definition last := last 0.
+
+  End Definitions.
+  
+  (* In this section, we prove a few basic lemmas about nondecreasing sequences. *)
+  Section Lemmas.
+ 
+    (* Next, we prove that no element can lie strictly between two 
+       neighboring elements and still belong to the list. *)
+    Lemma antidensity_of_nondecreasing_seq:
+      forall (xs: seq nat) (x: nat) (n: nat),
+        nondecreasing_sequence xs ->
+        xs [| n |] < x < xs [| n.+1 |] ->
+        ~~ (x \in xs).
+    Proof.
+      clear.
+      intros ? ? ? STR ?; apply/negP; intros ?. 
+      move: H0 => /nthP.  intros GG.
+      specialize (GG 0). 
+      move: GG => [ind LE HHH].
+      subst x; rename ind into x.                 
+      destruct (n.+1 < size xs) eqn:Bt; last first.
+      { move: Bt => /negP /negP; rewrite -leqNgt; move => Bt.
+        apply nth_default with (x0 := 0) in Bt. 
+        rewrite Bt in H; by move: H => /andP [_ T]. }
+      have B1: n.+1 < size xs; first by done. clear Bt.
+      have B2: n < size xs; first by apply leq_ltn_trans with n.+1.          
+      have GT: n < x.
+      { move: H => /andP [T _].
+        rewrite ltnNge; apply/negP; intros CONTR.
+        specialize (STR x n).
+        feed STR. by apply/andP; split.
+          by move: STR; rewrite leqNgt; move => /negP STR; apply: STR.
+      }
+      have LT: x < n.+1.
+      { clear GT.
+        move: H => /andP [_ T].
+        rewrite ltnNge; apply/negP; intros CONTR.
+        move: CONTR; rewrite leq_eqVlt; move => /orP [/eqP EQ | CONTR].
+        { by subst; rewrite ltnn in T. }
+        specialize (STR n.+1 x).
+        feed STR. by apply/andP; split; [ apply ltnW | done].
+          by move: STR; rewrite leqNgt; move => /negP STR; apply: STR.
+      }
+        by move: LT; rewrite ltnNge; move => /negP LT; apply: LT.
+    Qed. 
+
+    (* Alternatively, consider an arbitrary natural number x that is 
+       bounded by the first and the last element of a sequence xs. Then 
+       there is an index n such that xs[n] <= x < x[n+1]. *)
+    Lemma belonging_to_segment_of_seq_is_total:
+      forall (xs: seq nat) (x: nat), 
+        2 <= size xs -> 
+        first xs <= x < last xs ->
+        exists n,
+          n.+1 < size xs /\
+          xs[|n|] <= x < xs[|n.+1|].
+    Proof.
+      clear; intros ? ? SIZE LAST.
+      have EX: exists n, size xs <= n.
+      { by exists (size xs). } move: EX => [n LE].
+      destruct n.
+      { intros; destruct xs; by done. }
+      destruct n.
+      { intros.
+        destruct xs; first by done.
+          by destruct xs. 
+      }
+      generalize dependent xs.
+      induction n. 
+      { intros.
+        destruct xs; first by done.
+        destruct xs; first by done.
+        destruct xs; last by done.
+        clear LE SIZE.
+          by exists 0; unfold last in *; simpl in *.
+      }
+      { intros.
+        destruct xs; first by done.
+        destruct xs; first by done.
+        destruct xs.
+        { by exists 0; unfold last in *; simpl in *. }
+        destruct (x >= n1) eqn: NEQ.
+        { specialize (IHn [:: n1, n2 & xs]).
+          feed_n 3 IHn.
+          { by done. } 
+          { move: LAST => /andP [LAST1 LAST2].
+            apply/andP; split; first by done.
+            apply leq_trans with (last [:: n0, n1, n2 & xs]); first by done.
+              by rewrite /last !last_cons.
+          }
+          { by rewrite -(ltn_add2r 1) !addn1. }
+          move: IHn => [idx [SI /andP [G L]]].
+          exists idx.+1; split.
+          - by simpl in *; rewrite -addn1 -[in X in _ <= X]addn1 leq_add2r.
+          - by apply/andP; split.
+        }
+        { clear IHn SIZE LE; simpl in *.
+          exists 0; split; first by done.
+          move: NEQ => /negP /negP; rewrite -ltnNge; move => NEQ.
+          move: LAST => /andP [LAST _].
+            by apply/andP; split.
+        }
+      }
+    Qed.
+
+    (* We prove that the difference between any two neighboring elements is
+       bounded by the max element of the distances-sequence. *)
+    Lemma distance_between_neighboring_elements_le_max_distance_in_seq:
+      forall (xs: seq nat) (n: nat),
+        xs[|n.+1|] - xs[|n|] <= max (distances xs).
+    Proof.
+      clear; intros xs id.
+      apply leq_trans with (distances xs [| id |]).
+      rewrite leq_eqVlt; apply/orP; left; apply/eqP.
+      have EX: exists n, size xs <= n.
+      { by exists (size xs). } move: EX => [n LE].
+      generalize dependent xs; generalize dependent id.
+      induction n. 
+      { intros.
+        move: LE; rewrite leqn0 size_eq0; move => /eqP EQ; subst.
+          by rewrite !nth_default.
+      }
+      { intros. 
+        move: LE; rewrite leq_eqVlt; move => /orP [/eqP EQ|LT]; last first.
+        { by apply IHn; rewrite ltnS in LT. }
+        destruct xs; first by done.
+        destruct xs; first by destruct id; [simpl |rewrite !nth_default]. 
+        have Fact: distances [:: n0, n1 & xs] = (n1 - n0) :: distances [:: n1 & xs].
+        { by rewrite /distances; simpl; rewrite drop0. } 
+        rewrite Fact; clear Fact.
+        destruct id; first by done.
+        simpl.
+        rewrite -IHn. simpl. by done.
+          by move: EQ => /eqP; simpl; rewrite eqSS; move => /eqP EQ; rewrite -EQ.
+      }
+      { 
+        have Lem: forall x xs, x \in xs -> x <= max xs.
+        { clear; intros.
+          generalize dependent x.
+          induction xs.
+          { by done. }
+          { intros ? IN; rewrite /max seq_max_cons leq_max; apply/orP.
+            move: IN; rewrite in_cons; move => /orP [/eqP EQ| IN].
+            - by left; subst.
+            - by right; apply IHxs.
+          }
+        }
+        destruct (size (distances xs) <= id) eqn:SIZE.
+        { by rewrite nth_default. }
+        { apply Lem; rewrite mem_nth //.
+          move: SIZE => /negP /negP.
+            by rewrite ltnNge.
+        } 
+      }              
+    Qed.
+
+    (* As a corollary, the max distance between elements of any nontrivial sequence
+       (i.e. a sequence that contains at leas two distinct elements) is positive. *)
+    Corollary max_distance_in_nontrivial_seq_is_positive:
+      forall (xs: seq nat),
+        nondecreasing_sequence xs ->
+        (exists x y, x \in xs /\ y \in xs /\ x <> y) -> 
+        0 < max (distances xs).
+    Proof.
+      clear. 
+      intros xs SIZE SMI. 
+      move: SMI => [x [y [INx [INy NEQ]]]].
+      move: INx INy => /nthP INx /nthP INy.
+      specialize (INx 0); specialize (INy 0).
+      move: INx INy => [indx SIZEx EQx] [indy SIZEy EQy]. 
+      move: NEQ => /eqP; rewrite neq_ltn; move => /orP [LT|LT].
+      { have LTind: indx < indy. 
+        { rewrite ltnNge; apply/negP; intros CONTR.
+          specialize (SIZE indy indx).
+          feed SIZE; first by apply/andP; split.
+          subst x y.
+            by move: SIZE; rewrite leqNgt; move => /negP T; apply: T.
+        } 
+        have EQ: exists Δ, indy = indx + Δ.
+        { exists (indy - indx). by rewrite subnKC; last apply ltnW. }
+        move: EQ => [Δ EQ]; subst indy.
+        have F: exists ind, indx <= ind < indx + Δ /\ xs[|ind|] < xs[|ind.+1|].
+        { subst x y.
+          clear SIZEx SIZEy.
+          generalize dependent xs.
+          generalize dependent indx.
+          induction Δ.
+          { intros.
+            exfalso.
+              by move: LT; rewrite addn0 ltnn.
+          }
+          intros.
+          have ALT: Δ = 0 \/ Δ > 0.
+          { by destruct Δ; auto. }
+          move: ALT => [ZERO | POS].
+          { subst Δ.
+            exists indx; split; last by rewrite addn1 in LT.
+              by rewrite addn1; apply/andP; split.
+          }
+          have ALT: xs[|indx + Δ|] == xs[|indx + Δ.+1|] \/ xs[|indx + Δ|] < xs[|indx + Δ.+1|].
+          { rewrite addnS.
+            have NEQ: xs [|indx + Δ|] <= xs [|(indx + Δ).+1|].
+            apply SIZE; apply/andP; split; first by done.
+            rewrite ltnNge; apply/negP; intros CONTR.
+            move: LT; rewrite ltnNge; move => /negP LT; apply: LT.
+            have EQ: xs [|indx + Δ.+1|] = 0.
+            { by rewrite nth_default ?addnS. }
+              by rewrite EQ; clear EQ.
+              by apply/orP; rewrite -leq_eqVlt.
+          }                    
+          move: ALT => [/eqP EQ|LT'].
+          { specialize (IHΔ indx).
+            feed IHΔ; first by rewrite -addn1 leq_add2l.
+            rewrite -EQ in LT.
+            specialize (IHΔ xs SIZE LT).
+            move: IHΔ => [ind [/andP [B1 B2] UP]].
+            exists ind; split; last by done.
+            apply/andP; split; first by done.
+              by rewrite addnS ltnS ltnW. 
+          }
+          { exists (indx + Δ); split.
+            - apply/andP; split; first by rewrite leq_addr.
+                by rewrite addnS.
+            - by rewrite -addnS.
+          }
+        }
+        move: F => [ind [/andP [B1 B2] UP]].
+        apply leq_trans with (xs [|ind.+1|] - xs [|ind|]).
+        - by rewrite subn_gt0.
+        - by apply distance_between_neighboring_elements_le_max_distance_in_seq.
+      }
+      { have LTind: indy < indx. 
+        { rewrite ltnNge; apply/negP; intros CONTR.
+          specialize (SIZE indx indy).
+          feed SIZE; first by apply/andP; split.
+          subst x y.
+            by move: SIZE; rewrite leqNgt; move => /negP T; apply: T.
+        } 
+        have EQ: exists Δ, indx = indy + Δ.
+        { exists (indx - indy). by rewrite subnKC; last apply ltnW. }
+        move: EQ => [Δ EQ]; subst indx.
+        have F: exists ind, indy <= ind < indy + Δ /\ xs[|ind|] < xs[|ind.+1|].
+        { subst x y.
+          clear SIZEx SIZEy.
+          generalize dependent xs.
+          generalize dependent indy.
+          induction Δ.
+          { intros.
+            exfalso.
+              by move: LT; rewrite addn0 ltnn.
+          }
+          intros.
+          have ALT: Δ = 0 \/ Δ > 0.
+          { by destruct Δ; auto. }
+          move: ALT => [ZERO | POS].
+          { subst Δ.
+            exists indy; split; last by rewrite addn1 in LT.
+              by rewrite addn1; apply/andP; split.
+          }
+          have ALT: xs[|indy + Δ|] == xs[|indy + Δ.+1|] \/ xs[|indy + Δ|] < xs[|indy + Δ.+1|].
+          { rewrite addnS.
+            have NEQ: xs [|indy + Δ|] <= xs [|(indy + Δ).+1|].
+            apply SIZE; apply/andP; split; first by done.
+            rewrite ltnNge; apply/negP; intros CONTR.
+            move: LT; rewrite ltnNge; move => /negP LT; apply: LT.
+            have EQ: xs [|indy + Δ.+1|] = 0.
+            { by rewrite nth_default ?addnS. }
+              by rewrite EQ; clear EQ.
+              by apply/orP; rewrite -leq_eqVlt.
+          }
+          move: ALT => [/eqP EQ|LT'].
+          { specialize (IHΔ indy).
+            feed IHΔ; first by rewrite -addn1 leq_add2l.
+            rewrite -EQ in LT.
+            specialize (IHΔ xs SIZE LT).
+            move: IHΔ => [ind [/andP [B1 B2] UP]].
+            exists ind; split; last by done.
+            apply/andP; split; first by done.
+              by rewrite addnS ltnS ltnW. 
+          }
+          { exists (indy + Δ); split.
+            - apply/andP; split; first by rewrite leq_addr.
+                by rewrite addnS.
+            - by rewrite -addnS.
+          }
+        }
+        move: F => [ind [/andP [B1 B2] UP]].
+        apply leq_trans with (xs [|ind.+1|] - xs [|ind|]).
+        - by rewrite subn_gt0.
+        - by apply distance_between_neighboring_elements_le_max_distance_in_seq.
+      }
+    Qed.
+    
+    (* Note that the distances-function has the expected behavior indeed. I.e. an element 
+       on the n-th position of the distance-sequence is equal to the difference between
+       n+1-th and n-th elements. *)
+    Lemma function_of_distances_is_correct:
+      forall (xs: seq nat) (n: nat),
+        (distances xs)[|n|] = xs[|n.+1|] - xs[|n|].
+    Proof.
+      clear. 
+      intros xs.
+      have EX: exists len, size xs <= len.
+      { exists (size xs). by done. } 
+      move: EX => [len LE].
+      generalize dependent xs.
+      induction len.
+      { intros.
+        move: LE; rewrite leqn0 size_eq0; move => /eqP EQ; subst.
+        unfold distances. simpl.
+          by destruct n; simpl.
+      } 
+      intros.
+      move: LE; rewrite leq_eqVlt; move => /orP [/eqP EQ| LE]; last first.
+      { by apply IHlen. }
+      destruct xs as [ | x1 xs]. inversion EQ.
+      destruct xs as [ | x2 xs].
+      { clear EQ.
+        destruct n. by simpl.
+        destruct n; by simpl.
+      }
+      destruct n; first by done. 
+      have F: distances [:: x1, x2 & xs] [|n.+1|] = distances [::x2 & xs] [| n |].
+      { have EQ': distances [:: x1, x2 & xs] = (x2 - x1) :: distances [::x2 & xs].
+        { by unfold distances; simpl; rewrite drop0. } 
+          by rewrite EQ'.
+      }
+      have F2: [:: x1, x2 & xs] [|n.+2|] - [:: x1, x2 & xs] [|n.+1|] = [:: x2 & xs] [|n.+1|] - [:: x2 & xs] [|n|]; first by done.
+      rewrite F F2. 
+      apply IHlen.
+      move: EQ => /eqP; simpl; rewrite eqSS; move => /eqP EQ.
+        by rewrite -EQ. 
+    Qed.
+
+    (* We show that the size of a distances-sequence is one less 
+       than the size of the original sequence. *)
+    Lemma size_of_seq_of_distances:
+      forall (xs: seq nat),
+        2 <= size xs ->
+        size xs = size (distances xs) + 1.
+    Proof.
+      clear.
+      intros xs.
+      have EX: exists len, size xs <= len.
+      { exists (size xs). by done. } 
+      move: EX => [len LE].
+      generalize dependent xs.
+      induction len.
+      { intros.
+        move: LE; rewrite leqn0 size_eq0; move => /eqP EQ; subst.
+          by done.
+      }
+      intros ? ? SIZE.
+      move: LE; rewrite leq_eqVlt; move => /orP [/eqP EQ| LE]; last first.
+      { by apply IHlen. }
+      destruct xs as [ | x1 xs]; first by inversion EQ.
+      destruct xs as [ | x2 xs]; first by inversion SIZE.
+      destruct xs as [ | x3 xs]; first by done.
+      clear SIZE.
+      have F1: size [:: x1, x2, x3 & xs] = size [:: x2, x3 & xs] + 1.
+      { by rewrite addn1. } 
+      have F2: size (distances [:: x1, x2, x3 & xs]) = size (distances [:: x2, x3 & xs]) + 1.
+      { by rewrite addn1. }
+      rewrite F1 F2; clear F1 F2.
+      apply/eqP; rewrite eqn_add2r; apply/eqP.
+      apply IHlen.
+      { move: EQ => /eqP. simpl. rewrite eqSS; move => /eqP EQ.
+          by rewrite -EQ.
+      }
+        by done.
+    Qed. 
+
+    (* Note that the last element of a nondecreasing sequence is the max element. *)
+    Lemma last_is_max_in_nondecreasing_seq:
+      forall (xs: seq nat) (x: nat),
+        nondecreasing_sequence xs ->
+        (x \in xs) -> 
+        x <= last xs.
+    Proof.
+      clear; intros ? ? STR IN. 
+      have NEQ: forall x y, x = y \/ x != y.
+      { clear. intros.
+        destruct (x == y) eqn:EQ.
+        - by left; apply/eqP.
+        - by right.
+      }
+      move: (NEQ _ x (last xs)); clear NEQ; move => [EQ|NEQ].
+      { by subst x. }
+      move: IN => /nthP EX.
+      specialize (EX 0). 
+      move: EX => [id SIZE EQ].
+      rewrite /last -nth_last -EQ; subst x.      
+      rewrite -addn1 in SIZE.
+      apply STR; apply/andP.
+      have POS: 0 < size xs.
+      { by apply leq_trans with (id + 1); [rewrite addn1| done]. }
+      split.
+      - by rewrite -(leq_add2r 1) !addn1 prednK // -addn1.
+      - by rewrite prednK.
+    Qed.     
+
+    (* Given a nondecreasing sequence xs with length n, we show that the difference 
+       between the last element of xs and the last element of the distances-sequence 
+       of xs is equal to the (n-2)'th element of xs. *)
+    Lemma last_seq_minus_last_distance_seq:
+      forall (xs: seq nat),
+        nondecreasing_sequence xs ->
+        last xs - last (distances xs) = xs [| (size xs).-2 |].
+    Proof.
+      clear.
+      intros xs SIS.
+      destruct xs as [ | x1 xs]. unfold last, seq.last. simpl. by done.
+      destruct xs as [ | x2 xs]. unfold last, seq.last. simpl. by rewrite subn0.
+      rewrite {2}/last -[in X in _ - X]nth_last function_of_distances_is_correct prednK; last by done.
+      set [:: x1, x2 & xs] as X.
+      rewrite /last -nth_last.
+      rewrite size_of_seq_of_distances; last by done.
+      rewrite !addn1.
+      rewrite -pred_Sn.
+      rewrite subKn; first by done.
+      unfold X.
+      unfold nondecreasing_sequence in *.
+      apply SIS.
+      apply/andP; split.
+      simpl; by done.
+      rewrite [in X in _ < X]size_of_seq_of_distances; last by done.
+        by rewrite addn1.
+    Qed.          
+
+    (* Note that the last element is at most the max element. *)
+    Lemma last_of_seq_le_max_of_seq:
+      forall (xs: seq nat),
+        last xs <= max xs.
+    Proof.
+      clear.
+      intros xs.
+      have EX: exists len, size xs <= len.
+      { exists (size xs). by done. } 
+      move: EX => [len LE].
+      generalize dependent xs.
+      induction len.
+      { by intros; move: LE; rewrite leqn0 size_eq0; move => /eqP EQ; subst. }
+      intros ? SIZE.
+      move: SIZE; rewrite leq_eqVlt; move => /orP [/eqP EQ| LE]; last first.
+      { by apply IHlen. }
+      destruct xs as [ | x1 xs]; first by inversion EQ.
+      destruct xs as [ | x2 xs]. by rewrite /last /max leq_max; apply/orP; right.
+      have F1: last [:: x1, x2 & xs] = last [:: x2 & xs].
+      { by unfold last; simpl. }
+      rewrite F1 /max seq_max_cons; clear F1.
+      rewrite leq_max; apply/orP; right.
+      apply IHlen.
+      move: EQ => /eqP; simpl; rewrite eqSS; move => /eqP EQ.
+        by subst.
+    Qed.
+
+    (* If any n'th element of a sequence xs is less-than-or-equal-to n'th 
+       element of ys, then max of xs is less-than-or-equal-to max of ys. *)
+    Lemma max_of_dominating_seq:
+      forall (xs ys: seq nat),
+        (forall n, xs[|n|] <= ys[|n|]) ->
+        max xs <= max ys.
+    Proof.
+      clear.
+      intros xs ys.
+      have EX: exists len, size xs <= len /\ size ys <= len.
+      { exists (maxn (size xs) (size ys)).
+          by split; rewrite leq_max; apply/orP; [left | right].
+      }
+      move: EX => [len [LE1 LE2]].
+      generalize dependent xs.
+      generalize dependent ys.
+      induction len.
+      { intros. 
+        move: LE1 LE2; rewrite !leqn0 !size_eq0; move => /eqP E1 /eqP E2.
+        subst. by done.
+      }
+      {
+        intros. 
+        destruct xs, ys; try done.
+        { have L: forall xs, (forall n, xs [| n |] = 0) -> max xs = 0.
+          { clear. intros.
+            induction xs; first by done.
+            rewrite /max seq_max_cons.
+            apply/eqP; rewrite eqn_leq; apply/andP; split; last by done.
+            rewrite geq_max; apply/andP; split.
+            - by specialize (H 0); simpl in H; rewrite H.
+            - rewrite leqn0; apply/eqP; apply: IHxs.
+              intros.
+              specialize (H n.+1).
+                by simpl in *.
+          }
+          rewrite L; first by done. 
+          intros.
+          specialize (H n0).
+            by destruct n0; simpl in *; apply/eqP; rewrite -leqn0.
+        }
+        {  rewrite /max !seq_max_cons.
+           rewrite geq_max; apply/andP; split.
+           + rewrite leq_max; apply/orP; left.
+               by specialize (H 0); simpl in H.
+           + rewrite leq_max; apply/orP; right.
+             apply IHlen.
+             rewrite ltnS in LE2; by done.
+             rewrite ltnS in LE1; by done.
+             intros.
+             specialize (H n1.+1). 
+               by simpl in H.
+        }
+      }
+    Qed.
+
+    (* The max element of the distances-sequence of a sequence xs is bounded 
+       by the last element of xs. Note that all elements of xs are positive.
+       Thus they all lie within the interval [0, last xs]. *)
+    Lemma max_distance_in_seq_le_last_element_of_seq:
+      forall (xs: seq nat),
+        nondecreasing_sequence xs ->
+        max (distances xs) <= last xs. 
+    Proof. 
+      clear.
+      intros.
+      have SIZE: size xs < 2 \/ 2 <= size xs.
+      { destruct (size xs); auto.
+        destruct (n); auto.
+      }
+      move: SIZE => [LT | SIZE2].
+      { destruct xs.
+        rewrite /distances /last /max; simpl; by done.
+        destruct xs; last by done.
+          by unfold max, distances, last; simpl.
+      }
+      apply leq_trans with (last xs - first xs); last by apply leq_subr.
+      have F: forall xs c, (forall x, x \in xs -> x <= c) -> max xs <= c.
+      { clear; intros.
+        induction xs.
+        - by done.
+        - rewrite /max seq_max_cons geq_max; apply/andP; split.
+          + by apply H; rewrite in_cons; apply/orP; left.
+          + by apply IHxs; intros; apply H; rewrite in_cons; apply/orP; right.
+      }
+      apply F; clear F.
+      intros.
+      move: H0 => /nthP T; specialize (T 0).
+      move: T => [ind IN DIST].
+      rewrite function_of_distances_is_correct in DIST.
+      rewrite -DIST.
+      rewrite leq_sub //.
+      { destruct (xs [|ind.+1|] == last xs) eqn:EQ.
+        - by rewrite leq_eqVlt; apply/orP; left.
+        - rewrite /last -nth_last. apply H. 
+          rewrite -(ltn_add2r 1) addn1 -size_of_seq_of_distances in IN; last by done.
+          move: IN; rewrite leq_eqVlt; move => /orP [/eqP KK|KK].
+          move: EQ; rewrite /last -nth_last -{1}KK -[_.+2.-1]pred_Sn; move => /eqP; by done.
+          apply/andP; split; first rewrite -(ltn_add2r 1) !addn1 prednK //.
+          + by apply ltn_trans with ind.+2.
+          + by apply ltnW.
+          + by rewrite prednK //; apply ltn_trans with ind.+2.
+      }
+      { destruct (first xs == xs [|ind|]) eqn:EQ.
+        - by rewrite leq_eqVlt; apply/orP; left.
+        - rewrite /first -nth0. apply H.
+          rewrite -(ltn_add2r 1) addn1 -size_of_seq_of_distances in IN; last by done.
+          destruct ind; first by move: EQ; rewrite /first -nth0; move => /eqP.
+          apply/andP; split; first by done.
+            by apply ltn_trans with ind.+2.
+      }
+    Qed.
+
+    (* Consider two nondecreasing sequences xs and ys and assume that 
+       (1) first element of xs is at most the first element of ys and 
+       (2) distances-sequences of xs is dominated by distances-sequence of 
+       ys. Then xs is dominated by ys.  *)
+    Lemma domination_of_distances_implies_domination_of_seq:
+      forall (xs ys: seq nat),
+        first xs <= first ys ->
+        2 <= size xs ->
+        2 <= size ys ->
+        size xs = size ys -> 
+        nondecreasing_sequence xs ->
+        nondecreasing_sequence ys ->
+        (forall n, (distances xs)[|n|] <= (distances ys)[|n|]) ->
+        (forall n, xs[|n|] <= ys[|n|]).
+    Proof.
+      clear. 
+      intros xs ys.
+      have EX: exists len, size xs <= len /\ size ys <= len.
+      { exists (maxn (size xs) (size ys)).
+          by split; rewrite leq_max; apply/orP; [left | right].
+      }
+      move: EX => [len [LE1 LE2]]. 
+      generalize dependent xs.
+      generalize dependent ys. 
+      induction len.
+      { intros. 
+        move: LE1 LE2; rewrite !leqn0 !size_eq0; move => /eqP E1 /eqP E2.
+          by subst.
+      }
+      { intros ? LycSIZE ? LxSIZE FLE Sxs Sys SIZEEQ STRxs STRys LE n.
+        destruct xs as [ | x1 xs], ys as [ | y1 ys]; try by done.
+        destruct xs as [ | x2 xs], ys as [ | y2 ys]; try by done.
+        clear Sxs Sys.
+        have F: x2 <= y2.
+        { specialize (STRxs 0 1); simpl in STRxs; feed STRxs; first by done.
+          specialize (STRys 0 1); simpl in STRys; feed STRys; first by done.
+          specialize (LE 0); simpl in LE, FLE.
+          rewrite leqNgt; apply/negP; intros NEQ.
+          move: LE; rewrite leqNgt; move => /negP LE; apply: LE.
+          rewrite -(ltn_add2r x1).
+          rewrite subnK //.
+          rewrite subh1 //.
+          rewrite -(ltn_add2r y1).
+          rewrite subnK; last first.
+          apply leq_trans with y2; [by done | by rewrite leq_addr].
+          apply leq_ltn_trans with (y2 + y1).
+          - by rewrite leq_add2l.
+          - by rewrite ltn_add2r.
+        }
+        destruct xs as [ | x3 xs], ys as [ | y3 ys]; try by done. 
+        { destruct n; simpl; first by done.
+          destruct n; simpl; by done.
+        }
+        destruct n; first by simpl in *. 
+        simpl; apply IHlen; try done.
+        - by simpl in *; apply/eqP; rewrite -(eqn_add2r 1) !addn1; apply/eqP.
+        - move => m1 m2 /andP [B1 B2].
+          specialize (STRxs m1.+1 m2.+1).
+          feed STRxs.
+          apply/andP; split.
+          + by rewrite ltnS.
+          + by simpl in *; rewrite -(ltn_add2r 1) !addn1 in B2.
+              by done.
+        - move => m1 m2 /andP [B1 B2].
+          specialize (STRys m1.+1 m2.+1).
+          feed STRys.
+          apply/andP; split.
+          + by rewrite ltnS. 
+          + by simpl in *; rewrite -(ltn_add2r 1) !addn1 in B2.
+              by done.
+        - intros. specialize (LE n0.+1). simpl in LE.
+          unfold distances. simpl. by done.
+      }
+    Qed.
+
+  End Lemmas.
+
+End NondecreasingSequence.
\ No newline at end of file