diff --git a/restructuring/analysis/abstract/core/definitions.v b/restructuring/analysis/abstract/core/definitions.v
index e0341070e4ddea954b1fc7216407a895ca02203b..59fe51b6e3952473e69937e258d1d292371ddff6 100644
--- a/restructuring/analysis/abstract/core/definitions.v
+++ b/restructuring/analysis/abstract/core/definitions.v
@@ -1,9 +1,8 @@
 Require Export rt.restructuring.model.task.concept.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
 (** Throughout this file, we assume ideal uniprocessor schedules. *)
-Require Import rt.restructuring.model.processor.ideal.
-  
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
+Require Import rt.restructuring.model.processor.ideal.  
 
 (** * Definitions for Abstract Response-Time Analysis *)
 (** In this module, we propose a set of definitions for the general framework for response-time analysis (RTA) 
diff --git a/restructuring/analysis/definitions/busy_interval.v b/restructuring/analysis/definitions/busy_interval.v
index 5a2edb38fd9a8e7731f6a75c827836fea65da315..bb1fff380744394263ee947200a1ea5b747358e3 100644
--- a/restructuring/analysis/definitions/busy_interval.v
+++ b/restructuring/analysis/definitions/busy_interval.v
@@ -1,11 +1,10 @@
 Require Export rt.restructuring.model.priority.classes.
 Require Export rt.restructuring.analysis.basic_facts.completion.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
 (** Throughout this file, we assume ideal uniprocessor schedules. *)
 Require Import rt.restructuring.model.processor.ideal.
 
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
-
 (** * Busy Interval for JLFP-models *)
 (** In this file we define the notion of busy intervals for uniprocessor for JLFP schedulers. *)
 Section BusyIntervalJLFP.
diff --git a/restructuring/analysis/definitions/no_carry_in.v b/restructuring/analysis/definitions/no_carry_in.v
index f30d12ba15eec51560986479b284e7fc86c35b5e..252ab2794425bc10f5fa19d84bc8ef931ec1b81d 100644
--- a/restructuring/analysis/definitions/no_carry_in.v
+++ b/restructuring/analysis/definitions/no_carry_in.v
@@ -1,10 +1,9 @@
 Require Export rt.restructuring.model.priority.classes.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
 (** Throughout this file, we assume ideal uniprocessor schedules. *)
 Require Import rt.restructuring.model.processor.ideal.
 
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
-
 (** * No Carry-In *)
 (** In this module we define the notion of no carry-in time for uniprocessor schedulers. *)
 Section NoCarryIn.
diff --git a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/floating.v b/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/floating.v
index 0fd62e5c47e77750ffc69332bc01b29e7f890a97..693cb2e7ee765af3df85fcd1a994994a0ec8d157 100644
--- a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/floating.v
+++ b/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/floating.v
@@ -1,14 +1,18 @@
 Require Export rt.restructuring.analysis.edf.rta.nonpr_reg.response_time_bound.
 Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.floating.
 Require Import rt.restructuring.model.priority.edf.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
+(** Throughout this file, we assume ideal uniprocessor schedules. *)
 Require Import rt.restructuring.model.processor.ideal.
+
+(** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
 Require Import rt.restructuring.model.readiness.basic.
+
+(** Throughout this file, we assume the task model with floating non-preemptive regions. *)
 Require Import rt.restructuring.model.preemption.limited_preemptive.
 Require Import rt.restructuring.model.task.preemption.floating_nonpreemptive.
 
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
-
 (** * RTA for Model with Floating Non-Preemptive Regions *)
 (** In this module we prove the RTA theorem for floating non-preemptive regions EDF model. *)
 Section RTAforModelWithFloatingNonpreemptiveRegionsWithArrivalCurves.
diff --git a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/limited.v b/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/limited.v
index b7550071d82f68e1b7a3a7d724729da9373a0395..1b646474b50bce71dfed74a705e765b093694709 100644
--- a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/limited.v
+++ b/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/limited.v
@@ -1,14 +1,18 @@
 Require Export rt.restructuring.analysis.edf.rta.nonpr_reg.response_time_bound.
 Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.limited.
 Require Import rt.restructuring.model.priority.edf.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
+(** Throughout this file, we assume ideal uniprocessor schedules. *)
 Require Import rt.restructuring.model.processor.ideal.
+
+(** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
 Require Import rt.restructuring.model.readiness.basic.
+
+(** Throughout this file, we assume the task model with fixed preemption points. *)
 Require Import rt.restructuring.model.preemption.limited_preemptive.
 Require Import rt.restructuring.model.task.preemption.limited_preemptive.
 
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
-
 (** * RTA for EDF-schedulers with Fixed Premption Points *)
 (** In this module we prove the RTA theorem for EDF-schedulers with fixed preemption points. *)
 Section RTAforFixedPreemptionPointsModelwithArrivalCurves.
diff --git a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/nonpreemptive.v b/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/nonpreemptive.v
index 725cc69ac9be2209d886a07f272c2ef1b042299b..e72bc1c60c338062d5518e771d657de3b88e9506 100644
--- a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/nonpreemptive.v
+++ b/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/nonpreemptive.v
@@ -1,15 +1,17 @@
-Require Import rt.restructuring.model.processor.ideal.
-Require Import rt.restructuring.model.readiness.basic.
-
 Require Export rt.restructuring.analysis.edf.rta.nonpr_reg.response_time_bound.
 Require Export rt.restructuring.analysis.basic_facts.preemption.task.nonpreemptive.
 Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.nonpreemptive.
 Require Import rt.restructuring.model.priority.edf.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
-(** Assume we have a fully non-preemptive model. *)
-Require Import rt.restructuring.model.task.preemption.fully_nonpreemptive.
+(** Throughout this file, we assume ideal uniprocessor schedules. *)
+Require Import rt.restructuring.model.processor.ideal.
 
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
+(** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
+Require Import rt.restructuring.model.readiness.basic.
+
+(** Throughout this file, we assume the fully non-preemptive task model. *)
+Require Import rt.restructuring.model.task.preemption.fully_nonpreemptive.
 
 (** * RTA for Fully Non-Preemptive FP Model *)
 (** In this module we prove the RTA theorem for the fully non-preemptive EDF model. *)
diff --git a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/preemptive.v b/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/preemptive.v
index 6197685dcf250271b45c992264871f77f3170a8f..07c5ebf84182b63b0806682dcac005c78458d321 100644
--- a/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/preemptive.v
+++ b/restructuring/analysis/edf/rta/nonpr_reg/concrete_models/preemptive.v
@@ -1,15 +1,17 @@
-Require Import rt.restructuring.model.processor.ideal.
-Require Import rt.restructuring.model.readiness.basic.
-
 Require Import rt.restructuring.analysis.edf.rta.nonpr_reg.response_time_bound.
 Require Export rt.restructuring.analysis.basic_facts.preemption.task.preemptive.
 Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.preemptive.
 Require Import rt.restructuring.model.priority.edf.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
-(** Assume we have a fully preemptive model. *)
-Require Import rt.restructuring.model.task.preemption.fully_preemptive.
+(** Throughout this file, we assume ideal uniprocessor schedules. *)
+Require Import rt.restructuring.model.processor.ideal.
 
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
+(** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
+Require Import rt.restructuring.model.readiness.basic.
+
+(** Throughout this file, we assume the fully preemptive task model. *)
+Require Import rt.restructuring.model.task.preemption.fully_preemptive.
 
 (** * RTA for Fully Preemptive EDF Model *)
 (** In this section we prove the RTA theorem for the fully preemptive EDF model *)
diff --git a/restructuring/analysis/edf/rta/nonpr_reg/response_time_bound.v b/restructuring/analysis/edf/rta/nonpr_reg/response_time_bound.v
index 885eb5881013611b6f3b2456f0f00dd2da098939..6c59465f208da3fc317590b11ccfbb4827daecea 100644
--- a/restructuring/analysis/edf/rta/nonpr_reg/response_time_bound.v
+++ b/restructuring/analysis/edf/rta/nonpr_reg/response_time_bound.v
@@ -2,11 +2,13 @@ Require Export rt.restructuring.analysis.facts.priority_inversion_is_bounded.
 Require Export rt.restructuring.analysis.edf.rta.response_time_bound.
 Require Export rt.restructuring.analysis.arrival.rbf.
 Require Import rt.restructuring.model.priority.edf.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
+(** Throughout this file, we assume ideal uniprocessor schedules. *)
 Require Import rt.restructuring.model.processor.ideal.
-Require Import rt.restructuring.model.readiness.basic.
 
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
+(** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
+Require Import rt.restructuring.model.readiness.basic.
 
 (** * RTA for EDF-schedulers with Bounded Non-Preemprive Segments *)
 
diff --git a/restructuring/analysis/edf/rta/response_time_bound.v b/restructuring/analysis/edf/rta/response_time_bound.v
index 982e050af1353483598a267d7b72a9370b1ac911..fda9c51b8b3bec439b442c0ad580f62cc2e921c4 100644
--- a/restructuring/analysis/edf/rta/response_time_bound.v
+++ b/restructuring/analysis/edf/rta/response_time_bound.v
@@ -4,12 +4,15 @@ Require Export rt.restructuring.analysis.facts.no_carry_in_exists.
 Require Export rt.restructuring.analysis.schedulability.
 Require Import rt.restructuring.model.priority.edf.
 Require Import rt.restructuring.model.task.absolute_deadline.
+Require Import rt.restructuring.analysis.abstract.instantiations.ideal_processor.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
+(** Throughout this file, we assume ideal uniprocessor schedules. *)
 Require Import rt.restructuring.model.processor.ideal.
+
+(** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
 Require Import rt.restructuring.model.readiness.basic.
-Require Import rt.restructuring.analysis.abstract.instantiations.ideal_processor.
 
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
 (** * Abstract RTA for EDF-schedulers with Bounded Priority Inversion *)
 (** In this module we instantiate the Abstract Response-Time analysis
diff --git a/restructuring/analysis/facts/busy_interval_exists.v b/restructuring/analysis/facts/busy_interval_exists.v
index 3e08644788e015e9e3fec68c294c16856f982b3a..d97ca3841ebd13e3fc86871f17f53103fabfefae 100644
--- a/restructuring/analysis/facts/busy_interval_exists.v
+++ b/restructuring/analysis/facts/busy_interval_exists.v
@@ -2,6 +2,7 @@ Require Export rt.restructuring.analysis.definitions.job_properties.
 Require Export rt.restructuring.model.schedule.work_conserving.
 Require Export rt.restructuring.analysis.definitions.priority_inversion.
 Require Export rt.restructuring.analysis.basic_facts.all.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
 (** Throughout this file, we assume ideal uniprocessor schedules. *)
 Require Import rt.restructuring.model.processor.ideal.
@@ -9,8 +10,6 @@ Require Import rt.restructuring.model.processor.ideal.
 (** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
 Require Import rt.restructuring.model.readiness.basic.
 
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
-
 (** * Existence of Busy Interval for JLFP-models *)
 (** In this module we derive a sufficient condition for existence of
     busy intervals for uniprocessor for JLFP schedulers. *)
diff --git a/restructuring/analysis/facts/no_carry_in_exists.v b/restructuring/analysis/facts/no_carry_in_exists.v
index 1e9b85e351606b76463bd27d495a4e6364719454..26c4bdaf9381a9ca63792212226a7d6e0b67b426 100644
--- a/restructuring/analysis/facts/no_carry_in_exists.v
+++ b/restructuring/analysis/facts/no_carry_in_exists.v
@@ -1,5 +1,6 @@
 Require Export rt.restructuring.analysis.definitions.no_carry_in.
 Require Export rt.restructuring.analysis.facts.busy_interval_exists.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 
 (** Throughout this file, we assume ideal uniprocessor schedules. *)
 Require Import rt.restructuring.model.processor.ideal.
@@ -7,8 +8,6 @@ Require Import rt.restructuring.model.processor.ideal.
 (** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
 Require Import rt.restructuring.model.readiness.basic.
 
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
-
 (** * Existence of No Carry-In Instant *)
 
 (** In this section, we derive an alternative condition for the existence of 
diff --git a/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/floating.v b/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/floating.v
index 18e002d13381c7177f5818ee4b124eb11709c12d..6b9a836ac0dc30f258051e174906a3d5be9a35fa 100644
--- a/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/floating.v
+++ b/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/floating.v
@@ -1,5 +1,6 @@
 Require Export rt.restructuring.analysis.fixed_priority.rta.nonpr_reg.response_time_bound.
 Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.floating.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
 (** Throughout this file, we assume ideal uniprocessor schedules. *)
 Require Import rt.restructuring.model.processor.ideal.
@@ -7,11 +8,10 @@ Require Import rt.restructuring.model.processor.ideal.
 (** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
 Require Import rt.restructuring.model.readiness.basic.
 
+(** Throughout this file, we assume the task model with floating non-preemptive regions. *)
 Require Import rt.restructuring.model.preemption.limited_preemptive.
 Require Import rt.restructuring.model.task.preemption.floating_nonpreemptive.
 
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
-
 (** * RTA for Model with Floating Non-Preemptive Regions *)
 (** In this module we prove the RTA theorem for floating
     non-preemptive regions FP model. *)
diff --git a/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/limited.v b/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/limited.v
index 099c7bf599a2130c874f879ddf38c84e215e508a..7ce643664c90421f168addf7e1d36b8e07677061 100644
--- a/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/limited.v
+++ b/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/limited.v
@@ -1,5 +1,6 @@
 Require Export rt.restructuring.analysis.fixed_priority.rta.nonpr_reg.response_time_bound.
 Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.limited.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
 (** Throughout this file, we assume ideal uniprocessor schedules. *)
 Require Import rt.restructuring.model.processor.ideal.
@@ -7,10 +8,10 @@ Require Import rt.restructuring.model.processor.ideal.
 (** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
 Require Import rt.restructuring.model.readiness.basic.
 
+(** Throughout this file, we assume the task model with fixed preemption points. *)
 Require Import rt.restructuring.model.preemption.limited_preemptive.
 Require Import rt.restructuring.model.task.preemption.limited_preemptive.
 
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
 (** * RTA for FP-schedulers with Fixed Premption Points *)
 (** In this module we prove the RTA theorem for FP-schedulers with fixed preemption points. *)
diff --git a/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/nonpreemptive.v b/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/nonpreemptive.v
index f78d709f25139362cbb012c8bb3c9e21f9d6d01f..853e69903d2ba46a098e375020187f92eca56842 100644
--- a/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/nonpreemptive.v
+++ b/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/nonpreemptive.v
@@ -1,6 +1,7 @@
 Require Export rt.restructuring.analysis.fixed_priority.rta.nonpr_reg.response_time_bound.
 Require Export rt.restructuring.analysis.basic_facts.preemption.task.nonpreemptive.
 Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.nonpreemptive.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
 (** Throughout this file, we assume ideal uniprocessor schedules. *)
 Require Import rt.restructuring.model.processor.ideal.
@@ -8,10 +9,9 @@ Require Import rt.restructuring.model.processor.ideal.
 (** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
 Require Import rt.restructuring.model.readiness.basic.
 
+(** Throughout this file, we assume the fully non-preemptive task model. *)
 Require Import rt.restructuring.model.task.preemption.fully_nonpreemptive.
 
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
-
 (** * RTA for Fully Non-Preemptive FP Model *)
 (** In this module we prove the RTA theorem for the fully non-preemptive FP model. *)
 Section RTAforFullyNonPreemptiveFPModelwithArrivalCurves.
diff --git a/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/preemptive.v b/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/preemptive.v
index c411242a27515dbe47b516096b592ca6362c353f..b67faa581ec39bdafb6e1ec353185b6d7f637004 100644
--- a/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/preemptive.v
+++ b/restructuring/analysis/fixed_priority/rta/nonpr_reg/concrete_models/preemptive.v
@@ -1,13 +1,16 @@
 Require Export rt.restructuring.analysis.fixed_priority.rta.nonpr_reg.response_time_bound.
 Require Export rt.restructuring.analysis.basic_facts.preemption.task.preemptive.
 Require Export rt.restructuring.analysis.basic_facts.preemption.rtc_threshold.preemptive.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
-(** Assume we have a fully preemptive model. *)
+(** Throughout this file, we assume ideal uniprocessor schedules. *)
 Require Import rt.restructuring.model.processor.ideal.
+
+(** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
 Require Import rt.restructuring.model.readiness.basic.
-Require Import rt.restructuring.model.task.preemption.fully_preemptive.
 
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
+(** Throughout this file, we assume the fully preemptive task model. *)
+Require Import rt.restructuring.model.task.preemption.fully_preemptive.
 
 (** * RTA for Fully Preemptive FP Model *)
 (** In this module we prove the RTA theorem for fully preemptive FP model. *)
diff --git a/restructuring/analysis/fixed_priority/rta/nonpr_reg/response_time_bound.v b/restructuring/analysis/fixed_priority/rta/nonpr_reg/response_time_bound.v
index 88825b64be14fc0bbc89fc2da5b439953183a2f1..6f39f334dadf53fcdf410435d29227d5014ca2d7 100644
--- a/restructuring/analysis/fixed_priority/rta/nonpr_reg/response_time_bound.v
+++ b/restructuring/analysis/fixed_priority/rta/nonpr_reg/response_time_bound.v
@@ -2,6 +2,7 @@ Require Export rt.restructuring.analysis.schedulability.
 Require Export rt.restructuring.analysis.arrival.workload_bound.
 Require Export rt.restructuring.analysis.fixed_priority.rta.response_time_bound.
 Require Export rt.restructuring.analysis.facts.priority_inversion_is_bounded.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
 (** Throughout this file, we assume ideal uniprocessor schedules. *)
 Require Import rt.restructuring.model.processor.ideal.
@@ -9,8 +10,6 @@ Require Import rt.restructuring.model.processor.ideal.
 (** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
 Require Import rt.restructuring.model.readiness.basic.
 
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
-
 (** * RTA for FP-schedulers with Bounded Non-Preemprive Segments *)
 
 (** In this section we instantiate the Abstract RTA for FP-schedulers
diff --git a/restructuring/analysis/fixed_priority/rta/response_time_bound.v b/restructuring/analysis/fixed_priority/rta/response_time_bound.v
index 8662ed9f271d9e3018439ab73bfb8945ddde079b..3d2122480a364ee8d48d143d6db53e91d0e67c4a 100644
--- a/restructuring/analysis/fixed_priority/rta/response_time_bound.v
+++ b/restructuring/analysis/fixed_priority/rta/response_time_bound.v
@@ -1,6 +1,7 @@
 Require Export rt.restructuring.model.schedule.priority_driven.
 Require Export rt.restructuring.analysis.facts.busy_interval_exists.
 Require Import rt.restructuring.analysis.abstract.instantiations.ideal_processor.
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
 (** Throughout this file, we assume ideal uniprocessor schedules. *)
 Require Import rt.restructuring.model.processor.ideal.
@@ -8,8 +9,6 @@ Require Import rt.restructuring.model.processor.ideal.
 (** Throughout this file, we assume the basic (i.e., Liu & Layland) readiness model. *)
 Require Import rt.restructuring.model.readiness.basic.
 
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
-
 (** * Abstract RTA for FP-schedulers with Bounded Priority Inversion *)
 (** In this module we instantiate the Abstract Response-Time analysis
     (aRTA) to FP-schedulers for ideal uni-processor model of
diff --git a/restructuring/model/task/preemption/limited_preemptive.v b/restructuring/model/task/preemption/limited_preemptive.v
index 5b6b7f687457ea382e8cb9ad9f4d58b3e0c66b44..1dc1094fcc99377c07d905d914fed86fb6f89b0c 100644
--- a/restructuring/model/task/preemption/limited_preemptive.v
+++ b/restructuring/model/task/preemption/limited_preemptive.v
@@ -1,7 +1,6 @@
 Require Export rt.restructuring.model.task.preemption.parameters.
-From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
-
 Require Import rt.restructuring.model.preemption.limited_preemptive.
+From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
 
 (** * Platform for Models with Limited Preemptions *)
 (** In this section, we introduce a set of requirements for function