diff --git a/model/task/arrival/periodic_as_sporadic.v b/model/task/arrival/periodic_as_sporadic.v
index 3fb575218ce7ebe5a5c0de8239088b6a7059e6e3..e249a0f429d33fdf800f62e3726de386292aa7cb 100644
--- a/model/task/arrival/periodic_as_sporadic.v
+++ b/model/task/arrival/periodic_as_sporadic.v
@@ -67,13 +67,13 @@ Section PeriodicTasksAsSporadicTasks.
 
   (** First, we show that all tasks in a task set with valid periods
       also have valid min inter-arrival times. *)
-  Remark valid_periods_are_valid_inter_arrival_times:
+  Remark valid_periods_are_valid_inter_arrival_times :
     forall ts, valid_periods ts -> valid_taskset_inter_arrival_times ts.
   Proof. trivial. Qed.
 
   (** Second, we show that each task in a periodic task set respects
       the sporadic task model. *)
-  Remark periodic_task_sets_respect_sporadic_task_model:
+  Remark periodic_task_sets_respect_sporadic_task_model :
     forall ts,
       valid_periods ts ->
       taskset_respects_periodic_task_model arr_seq ts ->
@@ -87,6 +87,11 @@ Section PeriodicTasksAsSporadicTasks.
   
 End PeriodicTasksAsSporadicTasks.
 
-(** We add the [periodic_task_respects_sporadic_task_model] lemma into a "Hint Database" basic_rt_facts,
-    so Coq will be able to apply it automatically. *)
-Global Hint Extern 1 => apply periodic_task_respects_sporadic_task_model : basic_rt_facts.
+(** We add the lemmas into the "Hint Database" basic_rt_facts so that
+    they become available for proof automation. *)
+Global Hint Resolve
+  periodic_task_respects_sporadic_task_model
+  valid_period_is_valid_inter_arrival_time
+  valid_periods_are_valid_inter_arrival_times
+  periodic_task_sets_respect_sporadic_task_model
+  : basic_rt_facts.
diff --git a/model/task/arrival/sporadic_as_curve.v b/model/task/arrival/sporadic_as_curve.v
index 4051d343c064af21419e0cd5a0c2fbca5a0d7257..bc9e45287849d7afd3892505ba4319e78eb2381f 100644
--- a/model/task/arrival/sporadic_as_curve.v
+++ b/model/task/arrival/sporadic_as_curve.v
@@ -27,6 +27,13 @@ Section SporadicArrivalCurve.
     exact: div_ceil_monotone1.
   Qed.
 
+  (** For convenience, we lift the preceding observation to the level
+      of entire task sets. *)
+  Remark sporadic_task_sets_arrival_curve_valid :
+    forall ts,
+      valid_taskset_arrival_curve ts max_arrivals.
+  Proof. move=> ? ? ?; exact: sporadic_arrival_curve_valid. Qed.
+
    (** Next, we note that it is indeed an arrival bound. To this end,
        consider any type of jobs stemming from these tasks ... *)
   Context {Job : JobType} `{JobTask Job Task} `{JobArrival Job}.
@@ -36,16 +43,43 @@ Section SporadicArrivalCurve.
   Hypothesis H_consistent_arrivals: consistent_arrival_times arr_seq.
   Hypothesis H_uniq_arr_seq: arrival_sequence_uniq arr_seq.
 
-  (** Let [tsk] denote any valid sporadic task to be analyzed. *)
-  Variable tsk : Task.
-  Hypothesis H_sporadic_model: respects_sporadic_task_model arr_seq tsk.
-  Hypothesis H_valid_inter_min_arrival: valid_task_min_inter_arrival_time tsk.
+  (** We establish the validity of the defined curve. *)
+  Section Validity.
+
+    (** Let [tsk] denote any valid sporadic task to be analyzed. *)
+    Variable tsk : Task.
+    Hypothesis H_sporadic_model: respects_sporadic_task_model arr_seq tsk.
+    Hypothesis H_valid_inter_min_arrival: valid_task_min_inter_arrival_time tsk.
+
+    (** We observe that [max_sporadic_arrivals] is indeed an upper bound
+        on the maximum number of arrivals. *)
+    Lemma sporadic_arrival_curve_respects_max_arrivals :
+      respects_max_arrivals arr_seq tsk (max_sporadic_arrivals tsk).
+    Proof. move=> t1 t2 LEQ. exact: sporadic_task_arrivals_bound. Qed.
 
-  (** We observe that [max_sporadic_arrivals] is indeed an upper bound
-      on the maximum number of arrivals. *)
-  Lemma sporadic_arrival_curve_respects_max_arrivals :
-    respects_max_arrivals arr_seq tsk (max_sporadic_arrivals tsk).
-  Proof. move=> t1 t2 LEQ. exact: sporadic_task_arrivals_bound. Qed.
+  End Validity.
+
+  (** For convenience, we lift the preceding observation to the level
+      of entire task sets. *)
+  Remark sporadic_task_sets_respects_max_arrivals :
+    forall ts,
+      valid_taskset_inter_arrival_times ts ->
+      taskset_respects_sporadic_task_model ts arr_seq ->
+      taskset_respects_max_arrivals arr_seq ts.
+  Proof.
+    move=> ts VAL SPO tsk IN.
+    apply: sporadic_arrival_curve_respects_max_arrivals.
+    - by apply: SPO.
+    - by apply: VAL.
+  Qed.
 
 End SporadicArrivalCurve.
 
+(** We add the lemmas into the "Hint Database" basic_rt_facts so that
+    they become available for proof automation. *)
+Global Hint Resolve
+  sporadic_arrival_curve_valid
+  sporadic_task_sets_arrival_curve_valid
+  sporadic_arrival_curve_respects_max_arrivals
+  sporadic_task_sets_respects_max_arrivals
+  : basic_rt_facts.