diff --git a/restructuring/model/priority/deadline_monotonic.v b/restructuring/model/priority/deadline_monotonic.v
index ff88a5370b85db8d8980a722afca27c2b38355ce..ff680b9dd5c5f7cfa6055a003cfe6312ced8faf0 100644
--- a/restructuring/model/priority/deadline_monotonic.v
+++ b/restructuring/model/priority/deadline_monotonic.v
@@ -29,11 +29,17 @@ Section Properties.
   Lemma DM_is_transitive : transitive_priorities.
   Proof. by intros t y x z; apply leq_trans. Qed.
 
+  (** DM is total. *)
+  Lemma DM_is_total : total_priorities.
+ Proof. by move=> t j1 j2; apply leq_total. Qed.
+
 End Properties.
 
 (** We add the above lemmas into a "Hint Database" basic_facts, so Coq
     will be able to apply them automatically. *)
 Hint Resolve
      DM_is_reflexive
-     DM_is_transitive: basic_facts.
+     DM_is_transitive
+     DM_is_total
+  : basic_facts.
 
diff --git a/restructuring/model/priority/edf.v b/restructuring/model/priority/edf.v
index aaa2db8a85ad3521e499a30dbb185fab7486a4c8..16f4709856516e22c14656c08e7f32788a36c111 100644
--- a/restructuring/model/priority/edf.v
+++ b/restructuring/model/priority/edf.v
@@ -28,11 +28,17 @@ Section PropertiesOfEDF.
   Lemma EDF_is_transitive : transitive_priorities.
   Proof. by intros t y x z; apply leq_trans. Qed.
 
+  (** EDF is total. *)
+  Lemma EDF_is_total : total_priorities.
+  Proof. by move=> t j1 j2; apply leq_total. Qed.
+
 End PropertiesOfEDF.
 
 (** We add the above lemmas into a "Hint Database" basic_facts, so Coq
     will be able to apply them automatically. *)
 Hint Resolve
      EDF_is_reflexive
-     EDF_is_transitive: basic_facts.
+     EDF_is_transitive
+     EDF_is_total
+  : basic_facts.
 
diff --git a/restructuring/model/priority/fifo.v b/restructuring/model/priority/fifo.v
index a8bf7af8bf7e2ff8aac40c65b96f66e6f85f8a66..2e16246e86612549ec7e4e2bb57d88ea74fd68f2 100644
--- a/restructuring/model/priority/fifo.v
+++ b/restructuring/model/priority/fifo.v
@@ -25,11 +25,17 @@ Section Properties.
   Lemma FIFO_is_transitive : transitive_priorities.
   Proof. by intros t y x z; apply leq_trans. Qed.
 
+  (** FIFO is total. *)
+  Lemma FIFO_is_total : total_priorities.
+  Proof. by move=> t j1 j2; apply leq_total. Qed.
+
 End Properties.
 
 (** We add the above lemmas into a "Hint Database" basic_facts, so Coq
     will be able to apply them automatically. *)
 Hint Resolve
      FIFO_is_reflexive
-     FIFO_is_transitive: basic_facts.
+     FIFO_is_transitive
+     FIFO_is_total
+  : basic_facts.
 
diff --git a/restructuring/model/priority/numeric_fixed_priority.v b/restructuring/model/priority/numeric_fixed_priority.v
index dd926cf88a5db7a96b81aa010bb8006e11c98b41..689f61b9844342b1f69a9bb58ce58bc56b897df3 100644
--- a/restructuring/model/priority/numeric_fixed_priority.v
+++ b/restructuring/model/priority/numeric_fixed_priority.v
@@ -41,11 +41,17 @@ Section Properties.
     by move=> PRIO_yx PRIO_zy; apply leq_trans with (n := task_priority (job_task y)).
   Qed.
 
+  (** The resulting priority policy is total. *)
+  Lemma NFP_is_total : total_priorities.
+  Proof. by move=> t j1 j2; apply leq_total. Qed.
+
 End Properties.
 
 (** We add the above lemmas into a "Hint Database" basic_facts, so Coq
     will be able to apply them automatically. *)
 Hint Resolve
      NFP_is_reflexive
-     NFP_is_transitive: basic_facts.
+     NFP_is_transitive
+     NFP_is_total
+  : basic_facts.
 
diff --git a/restructuring/model/priority/rate_monotonic.v b/restructuring/model/priority/rate_monotonic.v
index 4d3606e016423c3e6008801707d076158f9674f5..3ab5fa7f29152c3f0029f4e2c00880104ecff31d 100644
--- a/restructuring/model/priority/rate_monotonic.v
+++ b/restructuring/model/priority/rate_monotonic.v
@@ -31,11 +31,17 @@ Section Properties.
   Lemma RM_is_transitive : transitive_priorities.
   Proof. by intros t y x z; apply leq_trans. Qed.
 
+  (** RM is total. *)
+  Lemma RM_is_total : total_priorities.
+  Proof. by move=> t j1 j2; apply leq_total. Qed.
+
 End Properties.
 
 (** We add the above lemmas into a "Hint Database" basic_facts, so Coq
     will be able to apply them automatically. *)
 Hint Resolve
      RM_is_reflexive
-     RM_is_transitive: basic_facts.
+     RM_is_transitive
+     RM_is_total
+  : basic_facts.