diff git a/restructuring/analysis/facts/priority_inversion_is_bounded.v b/restructuring/analysis/facts/priority_inversion_is_bounded.v
index 6fbe1590ccd8591675a6b9eaff95f007a2c8398d..9e7880b5648255ffe036ca2d29d4f9a9042a5483 100644
 a/restructuring/analysis/facts/priority_inversion_is_bounded.v
+++ b/restructuring/analysis/facts/priority_inversion_is_bounded.v
@@ 18,6 +18,72 @@ From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bi
pending jobs are always ready. *)
Require Import rt.restructuring.model.readiness.basic.
+(** In preparation of the derivation of the priority inversion bound, we
+ establish two basic facts on preemption times. *)
+Section PreemptionTimes.
+
+ (** Consider any type of tasks ... *)
+ Context {Task : TaskType}.
+ Context `{TaskCost Task}.
+ Context `{TaskMaxNonpreemptiveSegment Task}.
+
+ (** ... and any type of jobs associated with these tasks. *)
+ Context {Job : JobType}.
+ Context `{JobTask Job Task}.
+ Context `{JobArrival Job}.
+ Context `{JobCost Job}.
+
+ (** In addition, we assume the existence of a function mapping a
+ task to its maximal nonpreemptive segment ... *)
+ Context `{TaskMaxNonpreemptiveSegment Task}.
+
+ (** ... and the existence of a function mapping a job and
+ its progress to a boolean value saying whether this job is
+ preemptable at its current point of execution. *)
+ Context `{JobPreemptable Job}.
+
+ (** Consider any arrival sequence with consistent arrivals. *)
+ Variable arr_seq : arrival_sequence Job.
+ Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
+
+ (** Next, consider any ideal uniprocessor schedule of this arrival sequence ... *)
+ Variable sched : schedule (ideal.processor_state Job).
+ Hypothesis H_jobs_come_from_arrival_sequence:
+ jobs_come_from_arrival_sequence sched arr_seq.
+
+ (** Consider a valid model with bounded nonpreemptive segments. *)
+ Hypothesis H_model_with_bounded_nonpreemptive_segments:
+ valid_model_with_bounded_nonpreemptive_segments arr_seq sched.
+
+ (** Then, we show that time 0 is a preemption time. *)
+ Lemma zero_is_pt: preemption_time sched 0.
+ Proof.
+ unfold preemption_time.
+ case SCHED: (sched 0) => [j  ]; last by done.
+ move: (SCHED) => /eqP; rewrite scheduled_at_def; move => ARR.
+ apply H_jobs_come_from_arrival_sequence in ARR.
+ rewrite /service /service_during big_geq; last by done.
+ destruct H_model_with_bounded_nonpreemptive_segments as [T1 T2].
+ by move: (T1 j ARR) => [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 >
+ ~~ scheduled_at sched j prt >
+ scheduled_at sched j prt.+1 >
+ preemption_time sched prt.+1.
+ Proof.
+ intros s pt ARR NSCHED SCHED.
+ unfold preemption_time.
+ move: (SCHED); rewrite scheduled_at_def; move => /eqP SCHED2; rewrite SCHED2; clear SCHED2.
+ destruct H_model_with_bounded_nonpreemptive_segments as [T1 T2].
+ by move: (T1 s ARR) => [_ [_ [_ P]]]; apply P.
+ Qed.
+
+End PreemptionTimes.
+
(** * 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
diff git a/restructuring/model/preemption/preemption_time.v b/restructuring/model/preemption/preemption_time.v
index 37bf755904ecd8b9fc47c52eda9c08cb994d996d..dfe6e24e18a6346428a2061bd37280fc03620dfb 100644
 a/restructuring/model/preemption/preemption_time.v
+++ b/restructuring/model/preemption/preemption_time.v
@@ 1,6 +1,5 @@
Require Import rt.util.all.
Require Import rt.restructuring.behavior.all.
Require Import rt.restructuring.analysis.basic_facts.ideal_schedule.
Require Import rt.restructuring.model.job.
Require Import rt.restructuring.model.task.
Require Import rt.restructuring.model.processor.ideal.
@@ 50,41 +49,5 @@ Section PreemptionTime.
if sched t is Some j then
job_preemptable j (service sched j t)
else true.

 (** In this section we prove a few basic properties of the preemption_time predicate. *)
 Section Lemmas.

 (** Consider a valid model with bounded nonpreemptive segments. *)
 Hypothesis H_model_with_bounded_nonpreemptive_segments:
 valid_model_with_bounded_nonpreemptive_segments arr_seq sched.

 (** Then, we 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; rewrite scheduled_at_def; move => ARR.
 apply H_jobs_come_from_arrival_sequence in ARR.
 rewrite /service /service_during big_geq; last by done.
 destruct H_model_with_bounded_nonpreemptive_segments as [T1 T2].
 by move: (T1 j ARR) => [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 >
 ~~ scheduled_at sched j prt >
 scheduled_at sched j prt.+1 >
 preemption_time prt.+1.
 Proof.
 intros s pt ARR NSCHED SCHED.
 unfold preemption_time.
 move: (SCHED); rewrite scheduled_at_def; move => /eqP SCHED2; rewrite SCHED2; clear SCHED2.
 destruct H_model_with_bounded_nonpreemptive_segments as [T1 T2].
 by move: (T1 s ARR) => [_ [_ [_ P]]]; apply P.
 Qed.

 End Lemmas.
End PreemptionTime.