diff --git a/behavior/facts/all.v b/behavior/facts/all.v
index 534cdb2a7245fda833d2c40cf3ca8ccd7b7d130d..d455c2ba54894d3300b1e75627c6c354f597373e 100644
--- a/behavior/facts/all.v
+++ b/behavior/facts/all.v
@@ -1,3 +1,4 @@
 Require Export rt.behavior.facts.service.
 Require Export rt.behavior.facts.completion.
 Require Export rt.behavior.facts.ideal_schedule.
+Require Export rt.behavior.facts.sequential.
diff --git a/behavior/facts/sequential.v b/behavior/facts/sequential.v
new file mode 100644
index 0000000000000000000000000000000000000000..27cad7cf8864c39e012ea247fde71d0c563cac15
--- /dev/null
+++ b/behavior/facts/sequential.v
@@ -0,0 +1,42 @@
+From rt.behavior Require Export sequential.
+
+Section ExecutionOrder.
+  (* Consider any type of job associated with any type of tasks... *)
+  Context {Job: JobType}.
+  Context {Task: TaskType}.
+  Context `{JobTask Job Task}.
+
+  (* ... with arrival times and costs ... *)
+  Context `{JobArrival Job}.
+  Context `{JobCost Job}.
+
+  (* ... and any kind of processor state model. *)
+  Context {PState: Type}.
+  Context `{ProcessorState Job PState}.
+
+  (* Assume a schedule ... *)
+  Variable sched: schedule PState.
+
+  (* in which the sequential jobs hypothesis holds. *)
+  Hypothesis H_sequential_jobs: sequential_jobs sched.
+
+
+  (* A simple corollary of this hypothesis is that the scheduler
+     executes a job with the earliest arrival time. *)
+  Corollary scheduler_executes_job_with_earliest_arrival:
+    forall j1 j2 t,
+      same_task j1 j2 ->
+      ~~ completed_by sched j2 t ->
+      scheduled_at sched j1 t ->
+      job_arrival j1 <= job_arrival j2.
+  Proof.
+    intros ? ? t TSK NCOMPL SCHED.
+    rewrite /same_task eq_sym in TSK.
+    have SEQ := H_sequential_jobs j2 j1 t TSK.
+    rewrite leqNgt; apply/negP; intros ARR.
+    move: NCOMPL => /negP NCOMPL; apply: NCOMPL.
+      by apply SEQ.
+  Qed.
+
+End ExecutionOrder.
+
diff --git a/behavior/sequential.v b/behavior/sequential.v
new file mode 100644
index 0000000000000000000000000000000000000000..974e6719a67f74269048d0d5ecb67a883583c775
--- /dev/null
+++ b/behavior/sequential.v
@@ -0,0 +1,29 @@
+From rt.behavior Require Export schedule task.
+
+Section PropertyOfSequentiality.
+  (* Consider any type of job associated with any type of tasks... *)
+  Context {Job: JobType}.
+  Context {Task: TaskType}.
+  Context `{JobTask Job Task}.
+
+  (* ... with arrival times and costs ... *)
+  Context `{JobArrival Job}.
+  Context `{JobCost Job}.
+
+  (* ... and any kind of processor state model. *)
+  Context {PState: Type}.
+  Context `{ProcessorState Job PState}.
+
+  (* Given a schedule ... *)
+  Variable sched: schedule PState.
+
+  (* ...we say that jobs (or, rather, tasks) are sequential if each task's jobs
+     are executed in the order they arrived. *)
+  Definition sequential_jobs :=
+    forall (j1 j2: Job) (t: instant),
+      same_task j1 j2 ->
+      job_arrival j1 < job_arrival j2 ->
+      scheduled_at sched j2 t ->
+      completed_by sched j1 t.
+
+End PropertyOfSequentiality.
diff --git a/behavior/task.v b/behavior/task.v
index 2759d28a6d5ca45eaf8d3c41f995b1488fe3706e..600edb5d16714470d85ce582ede79f780bade256 100644
--- a/behavior/task.v
+++ b/behavior/task.v
@@ -1,3 +1,4 @@
+From mathcomp Require Export ssrbool.
 From rt.behavior Require Export job.
 
 (* Throughout the library we assume that jobs have decidable equality *)
@@ -6,4 +7,17 @@ Definition TaskType := eqType.
 
 (* Definition of a generic type of parameter relating jobs to tasks *)
 
-Class JobTask (T : TaskType) (J : JobType) := job_task : J -> T.
\ No newline at end of file
+Class JobTask (J : JobType) (T : TaskType) := job_task : J -> T.
+
+
+Section SameTask.
+  (* For any type of job associated with any type of tasks... *)
+  Context {Job: JobType}.
+  Context {Task: TaskType}.
+  Context `{JobTask Job Task}.
+
+  (* ... we say that two jobs j1 and j2 are from the same task iff job_task j1
+     is equal to job_task j2. *)
+  Definition same_task j1 j2 := job_task j1 == job_task j2.
+
+End SameTask.