diff --git a/restructuring/model/task/preemption/floating_nonpreemptive.v b/restructuring/model/task/preemption/floating_nonpreemptive.v
index 3c801eabcf14a5554a5f2b57905cf651ac38f51e..26b57305b526e0768dfb9879e43758c248f0b4f2 100644
--- a/restructuring/model/task/preemption/floating_nonpreemptive.v
+++ b/restructuring/model/task/preemption/floating_nonpreemptive.v
@@ -1,8 +1,6 @@
 Require Import rt.restructuring.model.preemption.limited_preemptive.
 Require Export rt.restructuring.model.task.preemption.parameters.
 
-From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
-
 (** * Platform for Models with Floating Non-Preemptive Regions *)
 (** In this section, we introduce a set of requirements for function
     [task_max_nonpr_segment], so it is coherent with model with
diff --git a/restructuring/model/task/preemption/fully_nonpreemptive.v b/restructuring/model/task/preemption/fully_nonpreemptive.v
index 297fca8b1dfe0e5ce366f7bdbb797d5a0ebd8af5..becff2100e463b82286559b6cecc6b5d5b5e6c7f 100644
--- a/restructuring/model/task/preemption/fully_nonpreemptive.v
+++ b/restructuring/model/task/preemption/fully_nonpreemptive.v
@@ -1,7 +1,5 @@
 Require Export rt.restructuring.model.task.preemption.parameters.
 
-From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
-
 (** * Platform for Fully Non-Preemptive Model *)
 (** In this section, we instantiate function
    [task_max_nonpreemptive_segment] for the fully non-preemptive
@@ -22,9 +20,6 @@ Section FullyNonPreemptiveModel.
                                                      
 End FullyNonPreemptiveModel.
 
-
-From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop.
-
 (** * Task's Run to Completion Threshold *)
 (** In this section, we instantiate function [task run to completion
     threshold] for the fully non-preemptive model. *)
diff --git a/restructuring/model/task/preemption/fully_preemptive.v b/restructuring/model/task/preemption/fully_preemptive.v
index 654a2068151f5c023c76782ad3c42dee37f9fad0..8f658cb8a6a14986aae2655be1bab8236c80892f 100644
--- a/restructuring/model/task/preemption/fully_preemptive.v
+++ b/restructuring/model/task/preemption/fully_preemptive.v
@@ -17,8 +17,6 @@ Section FullyPreemptiveModel.
   
 End FullyPreemptiveModel.
 
-Require Export rt.restructuring.model.task.preemption.parameters.
-
 (** * Task's Run to Completion Threshold *)
 (** In this section, we instantiate function [task run to completion
    threshold] for the fully preemptive model. *)
diff --git a/restructuring/model/task/preemption/limited_preemptive.v b/restructuring/model/task/preemption/limited_preemptive.v
index 1dc1094fcc99377c07d905d914fed86fb6f89b0c..3458aa5bd9b15f07bc4d395eb1c71738186edbb3 100644
--- a/restructuring/model/task/preemption/limited_preemptive.v
+++ b/restructuring/model/task/preemption/limited_preemptive.v
@@ -1,6 +1,5 @@
 Require Export rt.restructuring.model.task.preemption.parameters.
 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