note that common priority policies are total

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.
 

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.
 

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.
 

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.
 

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.