diff --git a/analysis/abstract/abstract_rta.v b/analysis/abstract/abstract_rta.v
index f3bfb0084c0cfa93c28c026ea6f6381b7e4071a8..dae453703881b1b2e2b61738f237ac6ac2963805 100644
--- a/analysis/abstract/abstract_rta.v
+++ b/analysis/abstract/abstract_rta.v
@@ -1,9 +1,9 @@
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
+
 Require Export prosa.analysis.definitions.schedulability.
 Require Export prosa.analysis.abstract.search_space.
 Require Export prosa.analysis.abstract.run_to_completion.
 
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
-
 (** * Abstract Response-Time Analysis *)
 (** In this module, we propose the general framework for response-time analysis (RTA) 
     of uni-processor scheduling of real-time tasks with arbitrary arrival models. *)
diff --git a/analysis/abstract/definitions.v b/analysis/abstract/definitions.v
index 461e4ef687a722f905c2a68d26d3c8a282276781..d37fabc7165ab06af28e26cd064ae9ac218c9f0e 100644
--- a/analysis/abstract/definitions.v
+++ b/analysis/abstract/definitions.v
@@ -1,5 +1,5 @@
-Require Export prosa.model.task.concept.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
+Require Export prosa.model.task.concept.
 
 (** Throughout this file, we assume ideal uni-processor schedules. *)
 Require Import prosa.model.processor.ideal.  
diff --git a/analysis/abstract/ideal_jlfp_rta.v b/analysis/abstract/ideal_jlfp_rta.v
index c27b606f69b2b0b223533f948a31b44c0f6b3281..ef56378c5a87b14de452f9f012ba2b1297f7ede0 100644
--- a/analysis/abstract/ideal_jlfp_rta.v
+++ b/analysis/abstract/ideal_jlfp_rta.v
@@ -1,6 +1,6 @@
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 Require Export prosa.analysis.definitions.priority_inversion.
 Require Export prosa.analysis.abstract.abstract_seq_rta.
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
 (** Throughout this file, we assume ideal uni-processor schedules. *)
 Require Import prosa.model.processor.ideal.
diff --git a/analysis/abstract/search_space.v b/analysis/abstract/search_space.v
index 40b3d352ededaaaa3a06f85faaa1446827816d51..ae74e993f8c9c0ff62efbc066fcf6e6ad4eab719 100644
--- a/analysis/abstract/search_space.v
+++ b/analysis/abstract/search_space.v
@@ -1,7 +1,7 @@
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 Require Import prosa.util.epsilon.
 Require Import prosa.util.tactics.
 Require Import prosa.model.task.concept.
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
 (** * Reduction of the search space for Abstract RTA *)
 (** In this file, we prove that in order to calculate the worst-case response time 
diff --git a/analysis/definitions/carry_in.v b/analysis/definitions/carry_in.v
index f657e5bc283fd9286f297a2fa75be9dee6476a09..b83bf9798e08c5427bfcc7dd26318ff6dcdfc95c 100644
--- a/analysis/definitions/carry_in.v
+++ b/analysis/definitions/carry_in.v
@@ -1,5 +1,5 @@
-Require Export prosa.model.priority.classes.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
+Require Export prosa.model.priority.classes.
 
 (** * No Carry-In *)
 (** In this module, we define the notion of a time without any carry-in work. *)
diff --git a/analysis/definitions/hyperperiod.v b/analysis/definitions/hyperperiod.v
index 0d7bad8f6a86a52ed19fe582e946445b1d04abd5..a3754188b6a3ff23a9ed690c87e488aae273aa75 100644
--- a/analysis/definitions/hyperperiod.v
+++ b/analysis/definitions/hyperperiod.v
@@ -1,6 +1,6 @@
+From mathcomp Require Import div.
 Require Export prosa.model.task.arrival.periodic.
 Require Export prosa.util.lcmseq.
-From mathcomp Require Import div.
 
 (** In this file we define the notion of a hyperperiod for periodic tasks. *)
 Section Hyperperiod.
diff --git a/analysis/facts/model/service_of_jobs.v b/analysis/facts/model/service_of_jobs.v
index 5670cd93d31196549dd6d15b7b7452ff586518c6..5680f812ea4be0c4680c060537742069258f68af 100644
--- a/analysis/facts/model/service_of_jobs.v
+++ b/analysis/facts/model/service_of_jobs.v
@@ -1,11 +1,11 @@
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
+
 Require Export prosa.model.aggregate.workload.
 Require Export prosa.model.aggregate.service_of_jobs.
 Require Export prosa.analysis.facts.behavior.completion.
 Require Export prosa.analysis.facts.model.ideal_schedule.
 Require Import prosa.model.processor.ideal.
 
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
-
 (** * Lemmas about Service Received by Sets of Jobs *)
 (** In this file, we establish basic facts about the service received by _sets_ of jobs. *)
 
diff --git a/analysis/facts/tdma.v b/analysis/facts/tdma.v
index a94adcd6a9df2d9d417f8ca43ddbfb23ed52dfa7..aca8b5cc0ee81813407bb27ecc3af2cd5b8d72a6 100644
--- a/analysis/facts/tdma.v
+++ b/analysis/facts/tdma.v
@@ -1,6 +1,6 @@
+From mathcomp Require Import div.
 Require Export prosa.model.schedule.tdma.
 Require Import prosa.util.all.
-From mathcomp Require Import div.
 
 (** In this section, we define the properties of TDMA and prove some basic lemmas. *)
 Section TDMAFacts.
diff --git a/analysis/facts/transform/wc_correctness.v b/analysis/facts/transform/wc_correctness.v
index 2042cb138ca649a6fe44b44a5ea258440859b31c..c9cdd027b97b2e7c013e3a951d7291a3978cc7ff 100644
--- a/analysis/facts/transform/wc_correctness.v
+++ b/analysis/facts/transform/wc_correctness.v
@@ -1,3 +1,5 @@
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
+
 Require Export prosa.model.schedule.work_conserving.
 Require Export prosa.analysis.facts.model.ideal_schedule.
 Require Export prosa.analysis.transform.wc_trans.
@@ -5,8 +7,6 @@ Require Export prosa.analysis.facts.transform.swaps.
 Require Export prosa.analysis.definitions.schedulability.
 Require Export prosa.util.list.
 
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
-
 (** * Correctness of the work-conservation transformation *)
 (** This file contains the main argument of the work-conservation proof,
     starting with an analysis of the individual functions that drive
diff --git a/behavior/job.v b/behavior/job.v
index e5d17882bc724b8300cdc4b44367a758525a7443..d008c821976426421f3e4d6a019c9d6a39ea5e85 100644
--- a/behavior/job.v
+++ b/behavior/job.v
@@ -1,5 +1,5 @@
-Require Export prosa.behavior.time.
 From mathcomp Require Export eqtype ssrnat.
+Require Export prosa.behavior.time.
 
 (** * Notion of a Job Type *)
 
diff --git a/model/priority/classes.v b/model/priority/classes.v
index 8646455a9a48bdbee894f3a1f7f1021e224c1f97..ac48795dcf47317f38c2209a0e6a11dc74d9e513 100644
--- a/model/priority/classes.v
+++ b/model/priority/classes.v
@@ -1,9 +1,9 @@
+From mathcomp Require Export seq.
+
 Require Export prosa.model.task.concept.
 Require Export prosa.util.rel.
 Require Export prosa.util.list.
 
-From mathcomp Require Export seq.
-
 (** * The FP, JLFP, and JLDP Priority Classes *)
 
 (** In this module, we define the three well-known classes of priority
diff --git a/model/schedule/tdma.v b/model/schedule/tdma.v
index 47a79907c1065bed2d2f6b6e4b13ed1631f7ab0c..68f5fd46fb134da15c25c89e8d3aed296272261c 100644
--- a/model/schedule/tdma.v
+++ b/model/schedule/tdma.v
@@ -1,7 +1,7 @@
+From mathcomp Require Import div.
 Require Export prosa.model.task.concept.
 Require Export prosa.util.seqset.
 Require Export prosa.util.rel.
-From mathcomp Require Import div.
 
 (** Throughout this file, we assume ideal uniprocessor schedules. *)
 Require prosa.model.processor.ideal.
diff --git a/results/edf/rta/bounded_pi.v b/results/edf/rta/bounded_pi.v
index bf82c7bf621befe8f445e1507670d27913ca0419..88113de4f67f5c022446faa477b269c410f60d82 100644
--- a/results/edf/rta/bounded_pi.v
+++ b/results/edf/rta/bounded_pi.v
@@ -1,3 +1,5 @@
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
+
 Require Export prosa.analysis.facts.priority.edf.
 Require Export prosa.analysis.definitions.schedulability.
 Require Import prosa.model.priority.edf.
@@ -6,8 +8,6 @@ Require Import prosa.analysis.abstract.ideal_jlfp_rta.
 Require Import prosa.analysis.facts.busy_interval.carry_in.
 Require Import prosa.analysis.facts.readiness.basic.
 
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
-
 (** Throughout this file, we assume ideal uni-processor schedules ... *)
 Require Import prosa.model.processor.ideal.
 
diff --git a/results/edf/rta/floating_nonpreemptive.v b/results/edf/rta/floating_nonpreemptive.v
index c6f3cde84b486a84680d69a3ecd76500e5788591..9859fc710ed493faac7227bec5afc6f46a79db70 100644
--- a/results/edf/rta/floating_nonpreemptive.v
+++ b/results/edf/rta/floating_nonpreemptive.v
@@ -1,9 +1,9 @@
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
+
 Require Export prosa.results.edf.rta.bounded_nps.
 Require Export prosa.analysis.facts.preemption.rtc_threshold.floating.
 Require Export prosa.analysis.facts.readiness.sequential.
 
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
-
 (** * RTA for EDF with Floating Non-Preemptive Regions *)
 (** In this module we prove the RTA theorem for floating non-preemptive regions EDF model. *)
 
diff --git a/results/edf/rta/fully_nonpreemptive.v b/results/edf/rta/fully_nonpreemptive.v
index 4034a3e6e1c68e34331b9afaceb532694811a0e9..8f9fbe80d5f65adc27aeb4f28b88a61f329138c3 100644
--- a/results/edf/rta/fully_nonpreemptive.v
+++ b/results/edf/rta/fully_nonpreemptive.v
@@ -1,10 +1,10 @@
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
+
 Require Export prosa.results.edf.rta.bounded_nps.
 Require Export prosa.analysis.facts.preemption.task.nonpreemptive.
 Require Export prosa.analysis.facts.preemption.rtc_threshold.nonpreemptive.
 Require Export prosa.analysis.facts.readiness.basic.
 
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
-
 
 (** * RTA for Fully Non-Preemptive EDF *)
 (** In this module we prove the RTA theorem for the fully non-preemptive EDF model. *)
diff --git a/results/edf/rta/fully_preemptive.v b/results/edf/rta/fully_preemptive.v
index 5ca06a9c032eece661467b2e9934df0b2fdab92b..e3a3395845c9e254872adcf0cea0860224218437 100644
--- a/results/edf/rta/fully_preemptive.v
+++ b/results/edf/rta/fully_preemptive.v
@@ -1,10 +1,10 @@
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
+
 Require Import prosa.results.edf.rta.bounded_nps.
 Require Export prosa.analysis.facts.preemption.task.preemptive.
 Require Export prosa.analysis.facts.preemption.rtc_threshold.preemptive.
 Require Export prosa.analysis.facts.readiness.basic.
 
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
-
 (** * RTA for Fully Preemptive EDF *)
 (** In this section we prove the RTA theorem for the fully preemptive EDF model *)
 
diff --git a/results/edf/rta/limited_preemptive.v b/results/edf/rta/limited_preemptive.v
index cbfced66a1da95def3810fe172b6b9809cecd964..309dfbeff90dce07872796f18de6565e2662593f 100644
--- a/results/edf/rta/limited_preemptive.v
+++ b/results/edf/rta/limited_preemptive.v
@@ -1,9 +1,9 @@
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
+
 Require Export prosa.results.edf.rta.bounded_nps.
 Require Export prosa.analysis.facts.preemption.rtc_threshold.limited.
 Require Export prosa.analysis.facts.readiness.basic.
 
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
-
 (** * RTA for EDF with Fixed Preemption Points *)
 (** In this module we prove the RTA theorem for EDF-schedulers with
     fixed preemption points. *)
diff --git a/results/fifo/rta.v b/results/fifo/rta.v
index 1a2f653be75c669644226b60b2b68d8ee4260813..f0d99bc85c2f54b5992896e35cfc0b254305f2ac 100644
--- a/results/fifo/rta.v
+++ b/results/fifo/rta.v
@@ -1,10 +1,10 @@
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
+
 Require Import prosa.analysis.facts.priority.fifo. 
 Require Import prosa.model.priority.fifo.
 Require Import prosa.analysis.abstract.ideal_jlfp_rta.
 Require Export prosa.analysis.facts.busy_interval.carry_in.
 
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
-
 (** Throughout this file, we assume ideal uni-processor schedules ... *)
 Require Import prosa.model.processor.ideal.
 
diff --git a/results/fixed_priority/rta/floating_nonpreemptive.v b/results/fixed_priority/rta/floating_nonpreemptive.v
index f7d9c99f0d10a163447b9e4856f5e998ab849ba2..4699544090733a1cdf67f50bf8b6ea37a9a1ebcc 100644
--- a/results/fixed_priority/rta/floating_nonpreemptive.v
+++ b/results/fixed_priority/rta/floating_nonpreemptive.v
@@ -1,9 +1,9 @@
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
+
 Require Export prosa.results.fixed_priority.rta.bounded_nps.
 Require Export prosa.analysis.facts.preemption.rtc_threshold.floating.
 Require Export prosa.analysis.facts.readiness.sequential.
 
-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/results/fixed_priority/rta/fully_nonpreemptive.v b/results/fixed_priority/rta/fully_nonpreemptive.v
index 5de85eaf48524cd10d95a89aebe406274309a6e4..3191a4e00c20891da08d61e606535458d2857f3c 100644
--- a/results/fixed_priority/rta/fully_nonpreemptive.v
+++ b/results/fixed_priority/rta/fully_nonpreemptive.v
@@ -1,10 +1,10 @@
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
+
 Require Export prosa.results.fixed_priority.rta.bounded_nps.
 Require Export prosa.analysis.facts.preemption.task.nonpreemptive.
 Require Export prosa.analysis.facts.preemption.rtc_threshold.nonpreemptive.
 Require Export prosa.analysis.facts.readiness.sequential.
 
-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. *)
diff --git a/results/fixed_priority/rta/fully_preemptive.v b/results/fixed_priority/rta/fully_preemptive.v
index 7e2b4800aacc8a90ecdb2f5e203c93c665ba1321..28ceef67f90438fcac8de2897cd2cdcc6425ceea 100644
--- a/results/fixed_priority/rta/fully_preemptive.v
+++ b/results/fixed_priority/rta/fully_preemptive.v
@@ -1,10 +1,10 @@
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
+
 Require Export prosa.results.fixed_priority.rta.bounded_nps.
 Require Export prosa.analysis.facts.preemption.task.preemptive.
 Require Export prosa.analysis.facts.preemption.rtc_threshold.preemptive.
 Require Export prosa.analysis.facts.readiness.sequential.
 
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
-
 
 (** * RTA for Fully Preemptive FP Model *)
 (** In this section we prove the RTA theorem for the fully preemptive FP model *)
diff --git a/results/fixed_priority/rta/limited_preemptive.v b/results/fixed_priority/rta/limited_preemptive.v
index 14de81fb1117f3196536fdc9df42dca0ae68249f..ff425f254b03dbb01f8338661c9efd74f9f3be4f 100644
--- a/results/fixed_priority/rta/limited_preemptive.v
+++ b/results/fixed_priority/rta/limited_preemptive.v
@@ -1,9 +1,9 @@
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
+
 Require Export prosa.results.fixed_priority.rta.bounded_nps.
 Require Export prosa.analysis.facts.preemption.rtc_threshold.limited.
 Require Export prosa.analysis.facts.readiness.sequential.
 
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
-
 
 (** * RTA for FP-schedulers with Fixed Preemption Points *)
 (** In this module we prove the RTA theorem for FP-schedulers with
diff --git a/util/div_mod.v b/util/div_mod.v
index e82386c7cc8686b6ea4448928397a9ccd412d68a..eed01ed2ba33b2296b68843ed3eada4bcb3e9d27 100644
--- a/util/div_mod.v
+++ b/util/div_mod.v
@@ -1,5 +1,5 @@
-Require Export prosa.util.nat prosa.util.subadditivity.
 From mathcomp Require Export ssreflect ssrbool eqtype ssrnat seq fintype bigop div ssrfun.
+Require Export prosa.util.nat prosa.util.subadditivity.
 
 (** Additional lemmas about [divn] and [modn]. *)
 Section DivMod.
diff --git a/util/list.v b/util/list.v
index 006559beb0b55c34ee7a8391bc70c5ae5acf0031..ebceb3a85e7a8d782e9a5079aa60c89733568cff 100644
--- a/util/list.v
+++ b/util/list.v
@@ -1,6 +1,6 @@
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 Require Import prosa.util.ssrlia prosa.util.tactics.
 Require Export prosa.util.supremum.
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
 
 (** We define a few simple operations on lists that return zero for
     empty lists: [max0], [first0], and [last0]. *)
diff --git a/util/minmax.v b/util/minmax.v
index 736d5cdc5568121bd1057ea29ff292b118057e8d..be2ad47adfa0d27839340c58f876814dc7876e69 100644
--- a/util/minmax.v
+++ b/util/minmax.v
@@ -1,5 +1,5 @@
-Require Export prosa.util.notation prosa.util.nat prosa.util.list.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
+Require Export prosa.util.notation prosa.util.nat prosa.util.list.
 
 (** Additional lemmas about [BigMax]. *)
 Section ExtraLemmas.
diff --git a/util/nat.v b/util/nat.v
index 9bf128120d0ec82d0c81921df2b179d60c2911a0..f327993445821de17b82b0e79c4f7311a9a5e5d1 100644
--- a/util/nat.v
+++ b/util/nat.v
@@ -1,5 +1,5 @@
-Require Export prosa.util.tactics prosa.util.ssrlia.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop div.
+Require Export prosa.util.tactics prosa.util.ssrlia.
 
 (** Additional lemmas about natural numbers. *)
 Section NatLemmas.
diff --git a/util/nondecreasing.v b/util/nondecreasing.v
index 2a890adf4bc1bdcd1014f1b38568fe1982d92d09..f55b3c7b82aa7badd7e1aae899328b3cb8b6701c 100644
--- a/util/nondecreasing.v
+++ b/util/nondecreasing.v
@@ -1,7 +1,7 @@
+From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
 Require Export prosa.util.epsilon.
 Require Export prosa.util.nat.
 Require Export prosa.util.list.
-From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
 
 (** * Non-Decreasing Sequence and Distances *)
 (** In this file we introduce the notion of a non-decreasing sequence. *)
diff --git a/util/sum.v b/util/sum.v
index 47a3209eeeeeecda74da6f560ef76d95fc9c5ce3..febadac56b77143f068469f784681530c4834df7 100644
--- a/util/sum.v
+++ b/util/sum.v
@@ -1,8 +1,8 @@
+From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop path.
+
 Require Export prosa.util.notation.
 Require Export prosa.util.nat.
 
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop path.
-
 Section SumsOverSequences.
 
   (** Consider any type [I] with a decidable equality ... *)
diff --git a/util/unit_growth.v b/util/unit_growth.v
index d29f82ac1736340d4a389da7efd7cbd1f9b37cba..cb75e30f42b951036783ae7dc7d50e2b1ab210db 100644
--- a/util/unit_growth.v
+++ b/util/unit_growth.v
@@ -1,5 +1,5 @@
-Require Import prosa.util.tactics prosa.util.notation.
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat.
+Require Import prosa.util.tactics prosa.util.notation.
 
 (** We say that a function [f] is a unit growth function iff for any
     time instant [t] it holds that [f (t + 1) <= f t + 1]. *)