diff --git a/analysis/facts/busy_interval/carry_in.v b/analysis/facts/busy_interval/carry_in.v
index 7e24459df6897ed944f34c3e00b4c744fdf2d473..c4ff57326eb6298667b6f16d720e4870b87a53e7 100644
--- a/analysis/facts/busy_interval/carry_in.v
+++ b/analysis/facts/busy_interval/carry_in.v
@@ -1,8 +1,8 @@
 Require Export prosa.analysis.facts.model.workload.
-Require Export prosa.analysis.definitions.carry_in.
-Require Export prosa.analysis.facts.busy_interval.busy_interval.
 Require Export prosa.analysis.facts.model.ideal.service_of_jobs.
-
+Require Export prosa.analysis.facts.busy_interval.quiet_time.
+Require Export prosa.analysis.definitions.work_bearing_readiness.
+Require Export prosa.model.schedule.work_conserving.
 
 (** * Existence of No Carry-In Instant *)
 
@@ -60,14 +60,6 @@ Section ExistsNoCarryIn.
   (** ... and assume that the schedule is work-conserving. *)
   Hypothesis H_work_conserving : work_conserving arr_seq sched.
 
-  (** The fact that there is no carry-in at time instant [t] trivially
-      implies that [t] is a quiet time. *)
-  Lemma no_carry_in_implies_quiet_time :
-    forall j t,
-      no_carry_in t ->
-      quiet_time j t.
-  Proof. by move=> j t + j_hp ARR HP BEF; apply. Qed.
-
   (** Conversely, the presence of a pending job implies that the processor isn't
       idle due to work-conservation. *)
   Lemma pending_job_implies_not_idle :
@@ -230,8 +222,7 @@ Section ExistsNoCarryIn.
             - eapply in_arrivals_implies_arrived_between in A; eauto 2.
           }
           apply/eqP; rewrite eqn_leq; apply/andP; split;
-            last by apply service_of_jobs_le_workload;
-            auto using ideal_proc_model_provides_unit_service.
+            last by apply service_of_jobs_le_workload.
           rewrite /total_workload (workload_of_jobs_cat arr_seq t); last first.
           apply/andP; split; [by done | by rewrite leq_addr].
           rewrite (service_of_jobs_cat_scheduling_interval _ _ _ _ _ _ _ t); try done; first last.
diff --git a/analysis/facts/busy_interval/busy_interval.v b/analysis/facts/busy_interval/ideal/busy_interval.v
similarity index 100%
rename from analysis/facts/busy_interval/busy_interval.v
rename to analysis/facts/busy_interval/ideal/busy_interval.v
diff --git a/analysis/facts/busy_interval/ideal/carry_in.v b/analysis/facts/busy_interval/ideal/carry_in.v
index a88fb6f270be24e4d6dcedf70cbef667f3846305..1bc826f8d41303bdf525f5db64a217862618e400 100644
--- a/analysis/facts/busy_interval/ideal/carry_in.v
+++ b/analysis/facts/busy_interval/ideal/carry_in.v
@@ -1,4 +1,5 @@
 Require Export prosa.analysis.facts.busy_interval.carry_in.
+Require Export prosa.analysis.facts.busy_interval.ideal.busy_interval.
 
 (** The following lemma conceptually belongs in
     [prosa.analysis.facts.busy_interval.carry_in], but still has dependencies
diff --git a/analysis/facts/busy_interval/ideal/hep_job_scheduled.v b/analysis/facts/busy_interval/ideal/hep_job_scheduled.v
index 932556146fe79dba1ff803fbb3cd0122a6c89003..1d55f9e95ea256a88b8391b301db27193af2a11b 100644
--- a/analysis/facts/busy_interval/ideal/hep_job_scheduled.v
+++ b/analysis/facts/busy_interval/ideal/hep_job_scheduled.v
@@ -1,5 +1,5 @@
 Require Export prosa.model.schedule.priority_driven.
-Require Export prosa.analysis.facts.busy_interval.busy_interval.
+Require Export prosa.analysis.facts.busy_interval.ideal.busy_interval.
 
 (** Throughout this file, we assume ideal uni-processor schedules. *)
 Require Import prosa.model.processor.ideal.
diff --git a/analysis/facts/busy_interval/ideal/priority_inversion.v b/analysis/facts/busy_interval/ideal/priority_inversion.v
index 6409a84ba1eb310e9460ba53361ebc40280fea28..f08013b1a3406a33695fe5a4241fed4e01990d8a 100644
--- a/analysis/facts/busy_interval/ideal/priority_inversion.v
+++ b/analysis/facts/busy_interval/ideal/priority_inversion.v
@@ -1,4 +1,4 @@
-Require Export prosa.analysis.facts.busy_interval.priority_inversion.
+Require Export prosa.analysis.facts.priority.inversion.
 
 (** Throughout this file, we assume ideal uni-processor schedules. *)
 Require Import prosa.model.processor.ideal.
diff --git a/analysis/facts/busy_interval/quiet_time.v b/analysis/facts/busy_interval/quiet_time.v
index f2b6f5655ac534162f33d652a1bd8937f50c8b0a..400dc7733654f0e571b8537ac136a8de5607989a 100644
--- a/analysis/facts/busy_interval/quiet_time.v
+++ b/analysis/facts/busy_interval/quiet_time.v
@@ -1,5 +1,6 @@
 Require Export prosa.analysis.definitions.busy_interval.
-  
+Require Export prosa.analysis.definitions.carry_in.
+
 (** In this module we collect some basic facts about quiet times. *)
 
 Section Facts.
@@ -16,9 +17,16 @@ Section Facts.
   Variable arr_seq : arrival_sequence Job.
 
   (** We prove that 0 is always a quiet time. *)
-  Lemma zero_is_quiet_time (j : Job) : quiet_time arr_seq sched j 0.
-  Proof.
-    by intros jhp ARR HP AB; move: AB; rewrite /arrived_before ltn0.
-  Qed.
+  Lemma zero_is_quiet_time (j : Job) :
+    quiet_time arr_seq sched j 0.
+  Proof. by move=> jhp ARR HP; rewrite /arrived_before ltn0. Qed.
+
+  (** The fact that there is no carry-in at time instant [t] trivially
+      implies that [t] is a quiet time. *)
+  Lemma no_carry_in_implies_quiet_time :
+    forall j t,
+      no_carry_in arr_seq sched t ->
+      quiet_time arr_seq sched j t.
+  Proof. by move=> j t + j_hp ARR HP BEF; apply. Qed.
 
 End Facts.
diff --git a/analysis/facts/priority/edf.v b/analysis/facts/priority/edf.v
index 2c1b624c5673ed95727454653ef8a2e2a7766a39..29ba567267507dd0a611a4f5ced28569ec7cba6a 100644
--- a/analysis/facts/priority/edf.v
+++ b/analysis/facts/priority/edf.v
@@ -35,7 +35,7 @@ Global Hint Resolve EDF_respects_sequential_tasks : basic_rt_facts.
 
 
 Require Export prosa.model.task.sequentiality.
-Require Export prosa.analysis.facts.busy_interval.priority_inversion.
+Require Export prosa.analysis.facts.priority.inversion.
 Require Export prosa.analysis.facts.priority.sequential.
 
 (** In this section, we prove that the EDF priority policy implies that tasks
diff --git a/analysis/facts/busy_interval/priority_inversion.v b/analysis/facts/priority/inversion.v
similarity index 100%
rename from analysis/facts/busy_interval/priority_inversion.v
rename to analysis/facts/priority/inversion.v
diff --git a/results/fixed_priority/rta/bounded_pi.v b/results/fixed_priority/rta/bounded_pi.v
index 37e456c40dbb45014d0f20b699ccfa27adf5c947..436090ab3350cfa3b286e5adc86a6a7db0af0b0e 100644
--- a/results/fixed_priority/rta/bounded_pi.v
+++ b/results/fixed_priority/rta/bounded_pi.v
@@ -1,6 +1,6 @@
 Require Export prosa.model.schedule.priority_driven.
 Require Export prosa.analysis.abstract.ideal.iw_instantiation.
-Require Export prosa.analysis.facts.busy_interval.busy_interval.
+Require Export prosa.analysis.facts.busy_interval.ideal.busy_interval.
 
 (** * Abstract RTA for FP-schedulers with Bounded Priority Inversion *)
 (** In this module we instantiate the Abstract Response-Time analysis