diff --git a/README.md b/README.md
index fcf386b3ae911c2facdccc09f40f2e5602ffb17b..e1c750a572af8ad63ad68a67efddba8715adeae9 100644
--- a/README.md
+++ b/README.md
@@ -40,6 +40,16 @@ Furthermore, there are a couple of additional folders and modules.
 - [`util`](util/): A collection of miscellaneous "helper" lemmas and tactics. Used throughout the rest of Prosa.
 - [`scripts/`](scripts/): Scripts and supporting resources required for continuous integration and documentation generation.
 
+
+## Side-effects
+
+Importing Prosa changes the behavior of ssreflect's `done` tactic by adding basic lemmas about real-time systems.
+
+```
+Ltac done := solve [ ssreflect.done | eauto 4 with basic_rt_facts ].
+```
+
+
 ## Installation
 
 ### With the OCaml Package Manager (`opam`)
diff --git a/analysis/abstract/ideal/abstract_rta.v b/analysis/abstract/ideal/abstract_rta.v
index 50695a0e011a6fea9fffa097f07e975ed283d6fa..18d4ab502925814e7d23fae7ee92276605fbeb31 100644
--- a/analysis/abstract/ideal/abstract_rta.v
+++ b/analysis/abstract/ideal/abstract_rta.v
@@ -1,5 +1,3 @@
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
-
 Require Export prosa.analysis.facts.model.ideal.schedule.
 Require Export prosa.analysis.definitions.schedulability.
 Require Export prosa.analysis.abstract.search_space.
diff --git a/analysis/abstract/search_space.v b/analysis/abstract/search_space.v
index b52a3559c5fada4189b082d76c776137371f9fc6..6e3291a51fe62c3f4deb3c153a6a400a2c92b16d 100644
--- a/analysis/abstract/search_space.v
+++ b/analysis/abstract/search_space.v
@@ -1,4 +1,3 @@
-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.
diff --git a/analysis/definitions/carry_in.v b/analysis/definitions/carry_in.v
index dc49b2269504061f28ea10255e5bcf37b86df564..8196290f3d2483f83a68c232ea7819ffa4fec3a5 100644
--- a/analysis/definitions/carry_in.v
+++ b/analysis/definitions/carry_in.v
@@ -1,4 +1,3 @@
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
 Require Export prosa.model.priority.classes.
 
 (** * No Carry-In *)
diff --git a/analysis/definitions/completion_sequence.v b/analysis/definitions/completion_sequence.v
index c3a34a49e704d4fdc6ee56e75cb03e268dc4069d..5c86391f1c291854fac9968194ad919cbccc6528 100644
--- a/analysis/definitions/completion_sequence.v
+++ b/analysis/definitions/completion_sequence.v
@@ -1,4 +1,3 @@
-From mathcomp Require Export ssreflect seq ssrnat ssrbool eqtype.
 Require Import prosa.behavior.service.
 
 (** This module contains basic definitions and properties of job
diff --git a/analysis/definitions/hyperperiod.v b/analysis/definitions/hyperperiod.v
index a3754188b6a3ff23a9ed690c87e488aae273aa75..158ebeb5e29f56f1407fb839dab6ba65c7e526ea 100644
--- a/analysis/definitions/hyperperiod.v
+++ b/analysis/definitions/hyperperiod.v
@@ -1,4 +1,3 @@
-From mathcomp Require Import div.
 Require Export prosa.model.task.arrival.periodic.
 Require Export prosa.util.lcmseq.
 
diff --git a/analysis/facts/model/ideal/service_of_jobs.v b/analysis/facts/model/ideal/service_of_jobs.v
index 8fd510e37904fb3aa3c7cdfdb93b1c6a28c99b25..e2d9ff4ab71a631a11488afd1102fd62572b8ea6 100644
--- a/analysis/facts/model/ideal/service_of_jobs.v
+++ b/analysis/facts/model/ideal/service_of_jobs.v
@@ -1,5 +1,3 @@
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
-
 Require Export prosa.model.schedule.scheduled.
 Require Export prosa.model.aggregate.workload.
 Require Export prosa.model.aggregate.service_of_jobs.
diff --git a/analysis/facts/model/service_of_jobs.v b/analysis/facts/model/service_of_jobs.v
index 54256026c8de1c42de3e261748c828d903b67468..d59a9cb21a1beec1ab72067f8cfd20ab428b660a 100644
--- a/analysis/facts/model/service_of_jobs.v
+++ b/analysis/facts/model/service_of_jobs.v
@@ -1,5 +1,3 @@
-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.
@@ -270,7 +268,7 @@ Section UnitServiceModelLemmas.
           [by left |right]; apply negbT in EQU; rewrite leqNgt. }
       move: (F1 t_compl t1) => /orP [LT | GT].
       - rewrite /service_of_jobs /service_during in EQ.
-        rewrite exchange_big big_geq //= in EQ; last by rewrite ltnW.
+        rewrite exchange_big big_geq //= in EQ.
         rewrite /workload_of_jobs in EQ.
         rewrite (big_rem j) ?Pj //= in EQ.
         move: EQ => /eqP; rewrite addn_eq0; move => /andP [CZ _].
diff --git a/analysis/facts/tdma.v b/analysis/facts/tdma.v
index b10aa7954a8af72a5b7dabdb781999a4d6cd011c..6df95f339a0458cfa468ea8482d1a76e5ba205f3 100644
--- a/analysis/facts/tdma.v
+++ b/analysis/facts/tdma.v
@@ -1,4 +1,3 @@
-From mathcomp Require Import div.
 Require Export prosa.model.schedule.tdma.
 Require Import prosa.util.all.
 
diff --git a/analysis/facts/transform/edf_opt.v b/analysis/facts/transform/edf_opt.v
index 5c21cd52fe8d26dead7ba8ca14a0048650ff8ada..688aefebe72b3d04ef7f1108818733ff99ebb23b 100644
--- a/analysis/facts/transform/edf_opt.v
+++ b/analysis/facts/transform/edf_opt.v
@@ -1,4 +1,3 @@
-From mathcomp Require Import ssrnat ssrbool fintype.
 Require Import prosa.model.readiness.basic.
 Require Export prosa.model.schedule.edf.
 Require Export prosa.analysis.definitions.schedulability.
diff --git a/analysis/facts/transform/wc_correctness.v b/analysis/facts/transform/wc_correctness.v
index 9c667011040bb70fd98570a47be980d33dbd6ebf..2eee23eb7652db12c17e21df290f6a42285fbc50 100644
--- a/analysis/facts/transform/wc_correctness.v
+++ b/analysis/facts/transform/wc_correctness.v
@@ -1,5 +1,3 @@
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
-
 Require Export prosa.model.schedule.work_conserving.
 Require Import prosa.model.readiness.basic.
 Require Export prosa.analysis.facts.model.ideal.schedule.
diff --git a/analysis/transform/prefix.v b/analysis/transform/prefix.v
index 82f976f515bbd90decf13968ee8885672ac907e4..08f5e27383d0521911cae023ddbad8b216723cc3 100644
--- a/analysis/transform/prefix.v
+++ b/analysis/transform/prefix.v
@@ -1,4 +1,3 @@
-From mathcomp Require Import ssrnat ssrbool fintype.
 Require Export prosa.analysis.facts.behavior.all.
 
 (** This file provides an operation that transforms a finite prefix of
diff --git a/behavior/arrival_sequence.v b/behavior/arrival_sequence.v
index 4e9fde5ada178e8ea2b4dc8fbcc7c5ef17dc80b0..c10efb3230a294c45269f7676e36627a51509494 100644
--- a/behavior/arrival_sequence.v
+++ b/behavior/arrival_sequence.v
@@ -1,4 +1,3 @@
-From mathcomp Require Export ssreflect seq ssrnat ssrbool bigop eqtype ssrfun.
 Require Export prosa.behavior.job.
 Require Export prosa.util.notation.
 
diff --git a/behavior/job.v b/behavior/job.v
index d008c821976426421f3e4d6a019c9d6a39ea5e85..d9355ee3ea55c954349e837a2a5c3243b6a3a089 100644
--- a/behavior/job.v
+++ b/behavior/job.v
@@ -1,4 +1,4 @@
-From mathcomp Require Export eqtype ssrnat.
+Require Export prosa.util.all.
 Require Export prosa.behavior.time.
 
 (** * Notion of a Job Type *)
diff --git a/behavior/ready.v b/behavior/ready.v
index d41858ae42da5e6334e122b9c7c76d436a4d7652..bc759ae88dd5dd56afb34eb19cffe6d63c694971 100644
--- a/behavior/ready.v
+++ b/behavior/ready.v
@@ -1,4 +1,3 @@
-From mathcomp Require Export ssreflect ssrnat ssrbool eqtype fintype bigop.
 Require Export prosa.behavior.service.
 
 (** * Readiness of a Job *)
diff --git a/behavior/schedule.v b/behavior/schedule.v
index 5b8fcc5a495d51096f6d15a4bef3ce5998cba8ba..9cb5b819ede1eccdf60ea82471bf2f9f5a812f43 100644
--- a/behavior/schedule.v
+++ b/behavior/schedule.v
@@ -1,4 +1,3 @@
-From mathcomp Require Export ssreflect ssrnat ssrbool eqtype fintype bigop.
 Require Export prosa.behavior.arrival_sequence.
 
 (** * Generic Processor State Interface *)
diff --git a/doc/guidelines.md b/doc/guidelines.md
index 52e3cb331507bf707f35a3a3d894ee405bb9265a..0505a0284756740af1824122d2b5fdbd486e95bb 100644
--- a/doc/guidelines.md
+++ b/doc/guidelines.md
@@ -96,7 +96,7 @@ Exception to this rule: ssreflect and other standard library imports.
 3. As an important exception to the prior rule, do not re-export modules that contain type class instance definitions. Prosa uses type class instances to express key modeling choices; such assumptions should be made explicitly.
 4. Always require external libraries first, i.e., *before* stating any Prosa-internal dependencies. This way, an addition in external libraries
 cannot shadow a definition in Prosa. For example, require `mathcomp` modules before any modules in the `prosa` namespace.
-
+5. Do not import `mathcomp` modules outside of  the `util/all.v` file. The file `util/tactics.v` redefined the behavior of the `done` tactic; hence, it must be imported after the `mathcomp` modules.
 
 ## Stating Lemmas and Theorems
 
diff --git a/implementation/definitions/extrapolated_arrival_curve.v b/implementation/definitions/extrapolated_arrival_curve.v
index 3cfa60b367fd4321e7b3184b389c8898b6ed07bf..91e7c7ddf8f743bec9ca1c67e75891374a124ad2 100644
--- a/implementation/definitions/extrapolated_arrival_curve.v
+++ b/implementation/definitions/extrapolated_arrival_curve.v
@@ -1,4 +1,3 @@
-From mathcomp Require Export ssreflect ssrbool eqtype ssrnat div seq path fintype bigop.
 Require Export prosa.behavior.time.
 Require Export prosa.util.all.
 
diff --git a/implementation/facts/extrapolated_arrival_curve.v b/implementation/facts/extrapolated_arrival_curve.v
index 1f77ace05e535c48caa33f5d4976b5bd1a5e0bac..97e120f0e3e77763f23a9212e7fe82f8742e68b3 100644
--- a/implementation/facts/extrapolated_arrival_curve.v
+++ b/implementation/facts/extrapolated_arrival_curve.v
@@ -1,4 +1,3 @@
-From mathcomp Require Export ssreflect ssrbool eqtype ssrnat div seq path fintype bigop.
 Require Export prosa.behavior.time.
 Require Export prosa.util.all.
 Require Export prosa.implementation.definitions.extrapolated_arrival_curve.
diff --git a/implementation/facts/generic_schedule.v b/implementation/facts/generic_schedule.v
index 6de5e8de08a19f2b9997bbbedf928c3542a8b1b6..8b368c3e138361707cbec4bda1d2fd3a2de15343 100644
--- a/implementation/facts/generic_schedule.v
+++ b/implementation/facts/generic_schedule.v
@@ -1,4 +1,3 @@
-From mathcomp Require Export ssreflect ssrnat ssrbool eqtype fintype bigop.
 Require Export prosa.implementation.definitions.generic_scheduler.
 Require Export prosa.analysis.facts.transform.replace_at.
 
diff --git a/model/priority/definitions.v b/model/priority/definitions.v
index 92f63fa1de5859aeb64ead6d42790a9602335499..c35939f6caa8123a6bc41efd893c03c2fd53f07b 100644
--- a/model/priority/definitions.v
+++ b/model/priority/definitions.v
@@ -1,5 +1,3 @@
-From mathcomp Require Export seq.
-
 Require Export prosa.model.task.concept.
 Require Export prosa.util.rel.
 Require Export prosa.util.list.
diff --git a/model/processor/ideal.v b/model/processor/ideal.v
index 5f76b4afc474c47d2c4122f7565439fc3ed857d8..c9576e1754ddb8cad759611df1bdab0ba7cc9137 100644
--- a/model/processor/ideal.v
+++ b/model/processor/ideal.v
@@ -1,4 +1,3 @@
-From mathcomp Require Import all_ssreflect.
 Require Export prosa.behavior.all.
 
 (** * The Ideal Uniprocessor Model *)
diff --git a/model/processor/multiprocessor.v b/model/processor/multiprocessor.v
index abe5efbab1b6551ecbc68ab52b980b09ce2fa864..a0faaa1ccd61d0c024f7542f8b88b85462dacae4 100644
--- a/model/processor/multiprocessor.v
+++ b/model/processor/multiprocessor.v
@@ -1,4 +1,3 @@
-From mathcomp Require Export fintype.
 Require Export prosa.behavior.all.
 Require Import prosa.analysis.facts.behavior.service.
 
diff --git a/model/processor/spin.v b/model/processor/spin.v
index ec68bf12c9229dfb3a0d17cf89723225374e537d..9cce1357f93f9095ac21ca6a3a68a20df67cc969 100644
--- a/model/processor/spin.v
+++ b/model/processor/spin.v
@@ -1,4 +1,3 @@
-From mathcomp Require Import all_ssreflect.
 Require Export prosa.behavior.all.
 
 (** In the following, we define a processor state that includes the possibility
diff --git a/model/processor/varspeed.v b/model/processor/varspeed.v
index 817fdaa8834d0fb7e9b2e39b58784cb061ba995f..87393a987985db74f6a58275e0c373d2a743bf6a 100644
--- a/model/processor/varspeed.v
+++ b/model/processor/varspeed.v
@@ -1,4 +1,3 @@
-From mathcomp Require Import all_ssreflect.
 Require Export prosa.behavior.all.
 
 (** In the following, we define a model of processors with variable execution
diff --git a/model/readiness/jitter.v b/model/readiness/jitter.v
index 816cf6cb19e043ad0b31bcef9db0b26399132bee..ee35fef54a0468b7bbe77a318e23a9c199625949 100644
--- a/model/readiness/jitter.v
+++ b/model/readiness/jitter.v
@@ -1,5 +1,3 @@
-From mathcomp Require Export ssreflect ssrnat ssrbool eqtype fintype bigop.
-
 Require Export prosa.behavior.all.
 Require Import prosa.util.nat.
 
diff --git a/model/schedule/edf.v b/model/schedule/edf.v
index 947d79c584395708fb75858d0bb3ec53637ded26..dcfcf7193f39adfbe91e7fc2d72c86372a676da0 100644
--- a/model/schedule/edf.v
+++ b/model/schedule/edf.v
@@ -1,4 +1,3 @@
-From mathcomp Require Import ssrnat ssrbool fintype.
 Require Export prosa.behavior.all.
 
 (** * Fully-Preemptive EDF Schedules *)
diff --git a/model/schedule/tdma.v b/model/schedule/tdma.v
index 2441b1e7e6be3c0072191cdeb513c6471ac5cf30..c2d4a485be4a2c494359f21c1419faf53f7ca486 100644
--- a/model/schedule/tdma.v
+++ b/model/schedule/tdma.v
@@ -1,4 +1,3 @@
-From mathcomp Require Import div.
 Require Export prosa.model.task.concept.
 Require Export prosa.util.seqset.
 Require Export prosa.util.rel.
diff --git a/results/edf/rta/bounded_pi.v b/results/edf/rta/bounded_pi.v
index 9b0bc644da65c2a9812fe079fd01edde4cf7d5ad..c3be107a74c2fb195850aea0da256a2ec6e6f883 100644
--- a/results/edf/rta/bounded_pi.v
+++ b/results/edf/rta/bounded_pi.v
@@ -1,5 +1,3 @@
-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.readiness.basic.
diff --git a/results/edf/rta/floating_nonpreemptive.v b/results/edf/rta/floating_nonpreemptive.v
index 61e215582d1fdc736c35e3c96cd38c7e5845b6f1..15f0d40904fbe5e6e74ec7f400d6c7ef4efb2159 100644
--- a/results/edf/rta/floating_nonpreemptive.v
+++ b/results/edf/rta/floating_nonpreemptive.v
@@ -1,5 +1,3 @@
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
-
 Require Import prosa.model.readiness.basic.
 Require Export prosa.results.edf.rta.bounded_nps.
 Require Export prosa.analysis.facts.preemption.rtc_threshold.floating.
diff --git a/results/edf/rta/fully_nonpreemptive.v b/results/edf/rta/fully_nonpreemptive.v
index 03912bdb24e65bfbecaa508e5a702c8d27d689c4..b8fecdff0f8b2ec5ca4d95e60c5b61da90b7c1f5 100644
--- a/results/edf/rta/fully_nonpreemptive.v
+++ b/results/edf/rta/fully_nonpreemptive.v
@@ -1,5 +1,3 @@
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
-
 Require Import prosa.model.readiness.basic.
 Require Export prosa.results.edf.rta.bounded_nps.
 Require Export prosa.analysis.facts.preemption.task.nonpreemptive.
diff --git a/results/edf/rta/fully_preemptive.v b/results/edf/rta/fully_preemptive.v
index c3942cf47e74049f54a052eaab6939afd7a58d23..06ac3de45e208f43313088f0005f3f3fe7df93e6 100644
--- a/results/edf/rta/fully_preemptive.v
+++ b/results/edf/rta/fully_preemptive.v
@@ -1,5 +1,3 @@
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
-
 Require Import prosa.model.readiness.basic.
 Require Import prosa.results.edf.rta.bounded_nps.
 Require Export prosa.analysis.facts.preemption.task.preemptive.
diff --git a/results/edf/rta/limited_preemptive.v b/results/edf/rta/limited_preemptive.v
index f70c1b064c82865d2313b3b2998a7a67c00ce43f..2d96af80caa0eb7c0e2843933704adf3293e5caf 100644
--- a/results/edf/rta/limited_preemptive.v
+++ b/results/edf/rta/limited_preemptive.v
@@ -1,5 +1,3 @@
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
-
 Require Export prosa.model.readiness.basic.
 Require Export prosa.results.edf.rta.bounded_nps.
 Require Export prosa.analysis.facts.preemption.rtc_threshold.limited.
diff --git a/results/elf/generality.v b/results/elf/generality.v
index c9d31d347f6d90a54c32f811267dea2e57d56892..4185cd03a3c493b59f6051e833075018b8d45f05 100644
--- a/results/elf/generality.v
+++ b/results/elf/generality.v
@@ -1,4 +1,3 @@
-From mathcomp Require Import eqtype ssrnat seq path fintype bigop.
 Require Export prosa.util.int.
 Require Export prosa.model.schedule.priority_driven.
 Require Export prosa.model.priority.elf.
diff --git a/results/elf/rta/bounded_pi.v b/results/elf/rta/bounded_pi.v
index 805e7b7e5c4fd59a9cccf2e9c76b33f57941f8ff..c72931a4764b0bfd2e4357e73babeca3e3da868f 100644
--- a/results/elf/rta/bounded_pi.v
+++ b/results/elf/rta/bounded_pi.v
@@ -1,5 +1,3 @@
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop ssrZ.
-
 Require Import prosa.util.int.
 Require Export prosa.analysis.abstract.ideal.cumulative_bounds.
 Require Export prosa.analysis.facts.priority.elf.
diff --git a/results/fifo/rta.v b/results/fifo/rta.v
index b1f8744658dc63573d8be9b4c596bb4fa5c8731d..acf80934bb73cb8d1e65ccea4767ec9d337e0ad0 100644
--- a/results/fifo/rta.v
+++ b/results/fifo/rta.v
@@ -1,5 +1,3 @@
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
-
 Require Import prosa.model.readiness.basic.
 Require Import prosa.model.priority.fifo.
 Require Import prosa.analysis.facts.priority.fifo.
diff --git a/results/fixed_priority/rta/comp/fully_preemptive.v b/results/fixed_priority/rta/comp/fully_preemptive.v
index ca6dc82b03f30bce35641e34cd2804319480d217..e8f17ffe485ae338b618d65540dc00c3dc3d20be 100644
--- a/results/fixed_priority/rta/comp/fully_preemptive.v
+++ b/results/fixed_priority/rta/comp/fully_preemptive.v
@@ -1,5 +1,3 @@
-From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq path fintype bigop.
-
 Require Export prosa.util.fixpoint.
 Require Export prosa.results.fixed_priority.rta.fully_preemptive.
 
diff --git a/results/fixed_priority/rta/floating_nonpreemptive.v b/results/fixed_priority/rta/floating_nonpreemptive.v
index 431649a01f32d2722ee6eeb3ffb27bb6e6775f7d..862e36446a610e8802347ff4b9c7195d8783d058 100644
--- a/results/fixed_priority/rta/floating_nonpreemptive.v
+++ b/results/fixed_priority/rta/floating_nonpreemptive.v
@@ -1,5 +1,3 @@
-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.
diff --git a/results/fixed_priority/rta/fully_nonpreemptive.v b/results/fixed_priority/rta/fully_nonpreemptive.v
index f9557ec2ac21ab1b864d45bf9ef1a83819bb12f9..9d71593e22e75151de3d22549fdece7880038d52 100644
--- a/results/fixed_priority/rta/fully_nonpreemptive.v
+++ b/results/fixed_priority/rta/fully_nonpreemptive.v
@@ -1,5 +1,3 @@
-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.
diff --git a/results/fixed_priority/rta/fully_preemptive.v b/results/fixed_priority/rta/fully_preemptive.v
index f32f854902355253297fed09e9af6d3d3a3e09a1..50300c5c21fa83c975e64d705974b4f1d0e84eb3 100644
--- a/results/fixed_priority/rta/fully_preemptive.v
+++ b/results/fixed_priority/rta/fully_preemptive.v
@@ -1,5 +1,3 @@
-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.
diff --git a/results/fixed_priority/rta/limited_preemptive.v b/results/fixed_priority/rta/limited_preemptive.v
index e7ee5be84e5669fe33d74bcfbfa2d9a2b8298d75..e99c04f086b4e145274d1c87e8048a95b64050f8 100644
--- a/results/fixed_priority/rta/limited_preemptive.v
+++ b/results/fixed_priority/rta/limited_preemptive.v
@@ -1,5 +1,3 @@
-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.
diff --git a/results/gel/generality.v b/results/gel/generality.v
index 4427c84c8bc38883ab19d436873728a1d89302db..fdee5d13e313568a48d8011c04dc069ad9c9704b 100644
--- a/results/gel/generality.v
+++ b/results/gel/generality.v
@@ -1,4 +1,3 @@
-From mathcomp Require Import eqtype ssrnat seq path fintype bigop.
 Require Export prosa.util.int.
 Require Export prosa.model.schedule.priority_driven.
 Require Export prosa.model.priority.gel.
diff --git a/results/gel/rta/bounded_pi.v b/results/gel/rta/bounded_pi.v
index 81366f9e28685630e7363fdb9fb9073501c17f7a..55ce7a7d5384ea1f28625fe1d186b0c060584b50 100644
--- a/results/gel/rta/bounded_pi.v
+++ b/results/gel/rta/bounded_pi.v
@@ -1,4 +1,3 @@
-From mathcomp Require Import eqtype ssrnat seq path fintype bigop.
 Require Import prosa.util.int.
 Require Import prosa.model.readiness.basic.
 Require Import prosa.analysis.abstract.ideal.cumulative_bounds.
diff --git a/util/all.v b/util/all.v
index ca17d35f789556b7d9020055c01caa96c222569a..41809cc80eb7c83cb75f37edbb6e8dbb74019618 100644
--- a/util/all.v
+++ b/util/all.v
@@ -1,5 +1,6 @@
+From mathcomp Require Export ssreflect ssrnat ssrbool eqtype fintype bigop.
+
 Require Export mathcomp.zify.zify.
-Require Export prosa.util.tactics.
 Require Export prosa.util.notation.
 Require Export prosa.util.bigcat.
 Require Export prosa.util.div_mod.
@@ -15,3 +16,4 @@ Require Export prosa.util.minmax.
 Require Export prosa.util.supremum.
 Require Export prosa.util.nondecreasing.
 Require Export prosa.util.setoid.
+Require Export prosa.util.tactics.