diff --git a/analysis/facts/model/task_cost.v b/analysis/facts/model/task_cost.v
index f4fe14238b599340c51e4fff940061de9d6fdb29..746e1b214e7f1cfeacd170abc00ca3bf52a8f235 100644
--- a/analysis/facts/model/task_cost.v
+++ b/analysis/facts/model/task_cost.v
@@ -28,6 +28,36 @@ Section TaskCost.
 
 End TaskCost.
 
+(** Next, we prove a simple lemma that extends the notion of [valid_job_cost]
+    from a single job to multiple jobs. *)
+Section JointWCETCompliance.
+
+  (** Consider any type of tasks and their jobs described by a WCET bound. *)
+  Context {Task : TaskType} `{TaskCost Task}.
+  Context {Job : JobType} `{JobCost Job} `{JobTask Job Task}.
+
+  (** Consider a given task [tsk] ... *)
+  Variable tsk : Task.
+
+  (** ... and any sequence of jobs of task [tsk] (in any order) with job costs
+      compliant with the task's WCET bound. *)
+  Variable js : seq Job.
+  Hypothesis H_valid_jobs : {in js, forall j, job_of_task tsk j && valid_job_cost j}.
+
+  (** Then it is the case that the sum of the costs of the jobs in the sequence
+      is upper-bounded by their joint WCET. *)
+  Lemma sum_job_costs_bounded :
+    \sum_(j <- js) job_cost j <= task_cost tsk * size js.
+  Proof.
+      rewrite -sum1_size big_distrr /=.
+      rewrite [leqLHS]big_seq_cond [leqRHS]big_seq_cond.
+      apply: leq_sum => j /andP[IN _] /[! muln1].
+      move: (H_valid_jobs _ IN) => /andP[/eqP <- COST].
+      by apply: COST.
+    Qed.
+
+End JointWCETCompliance.
+
 (** We add the above lemma to the global hints database. *)
 Global Hint Resolve
   job_cost_positive_implies_task_cost_positive :