diff --git a/_CoqProject b/_CoqProject
index b6b0fd8c9de79a374a807b97210510936ef8cbad..b7dffe558244fa77fc7224eb62c333aa98227c00 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -16,5 +16,6 @@ static_priority.v
 examples/case_study/arbitrary_flows.v
 #examples/case_study/case.v  # needs minerve to compile
 link/clock.v
+link/flow_cc_of_arrival_sequence.v
 
 COQDOCFLAGS = "-g -interpolate -utf8 --external https://math-comp.github.io/htmldoc/ mathcomp -R . NCCoq"
diff --git a/link/clock.v b/link/clock.v
index 30cf503ca33336b3d64ce47f210955331b65bce9..729ce2cdf4cdaf411da48ad9ac6624eea4c248d0 100644
--- a/link/clock.v
+++ b/link/clock.v
@@ -88,6 +88,20 @@ Lemma uclock_lt_next_tick (c : uclock) (t : universal_time) :
   forall n, (n < next_tick c t)%nat -> (c n)%:nngnum < t%:nngnum.
 Proof. by rewrite /next_tick; case: next_tick_ex => ? []. Qed.
 
+Lemma next_tick_eq (c : uclock) (t : universal_time) n :
+  t%:nngnum <= (c n)%:nngnum ->
+  (forall n' : nat, (n' < n)%N -> (c n')%:nngnum < t%:nngnum) ->
+  next_tick c t = n.
+Proof.
+move=> tlecn cltn.
+apply/anti_leq/andP; split.
+{ rewrite leqNgt; apply/negP => nltnt; move: tlecn; apply/negP; rewrite -ltNge.
+  exact: uclock_lt_next_tick. }
+rewrite leqNgt; apply/negP => ntltn.
+move: (cltn _ ntltn); apply/negP; rewrite -leNgt.
+exact: uclock_next_tick_gt.
+Qed.
+
 Lemma uclock_le (c : uclock) (x y : instant) :
   (x <= y)%nat -> (c x)%:nngnum <= (c y)%:nngnum.
 Proof.
@@ -122,6 +136,17 @@ Qed.
 Lemma next_tick_0 (c : uclock) : next_tick c 0%:nng = 0%nat.
 Proof. by rewrite -(uclock_0 c) uclockK. Qed.
 
+Lemma next_tick_gt0 c t : (0 < next_tick c t)%nat = (0 < t%:nngnum).
+Proof.
+apply/idP/idP => [ntgt0 | tgt0].
+{ rewrite ltNge; apply/negP => tle0; move: ntgt0; apply/negP; rewrite -leqNgt.
+  rewrite (_ : t = 0%:nng) ?next_tick_0//.
+  by apply/le_anti; rewrite !leEsub tle0 /=. }
+rewrite ltnNge leqn0; apply/negP => /eqP nt0.
+move: tgt0; apply/negP; rewrite -leNgt.
+by apply: (le_trans (uclock_next_tick_gt c t)); rewrite nt0 uclock_0.
+Qed.
+
 (** ** A few specific clocks *)
 
 (** Periodic clocks are a simple example of clock *)
diff --git a/link/flow_cc_of_arrival_sequence.v b/link/flow_cc_of_arrival_sequence.v
new file mode 100644
index 0000000000000000000000000000000000000000..fd7b44506cea444a7ef2b676f5270bbce7e5b281
--- /dev/null
+++ b/link/flow_cc_of_arrival_sequence.v
@@ -0,0 +1,82 @@
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype order ssrnat ssrint.
+From mathcomp Require Import choice seq path bigop ssralg ssrnum rat.
+From mathcomp Require Import fintype finfun.
+From mathcomp.analysis Require Import reals ereal nngnum posnum boolp classical_sets.
+Require Import prosa.util.nat prosa.util.bigcat prosa.util.sum.
+Require Import prosa.model.task.concept prosa.behavior.arrival_sequence.
+Require Import RminStruct cumulative_curves.
+Require Import clock.
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+Unset Printing Implicit Defensive.
+
+Local Open Scope classical_set_scope.
+Local Open Scope ring_scope.
+
+Import Order.Theory GRing.Theory Num.Theory.
+
+Section Flow_cc_of_arrival_sequence.
+
+Context {Task : TaskType}.
+Context {Job : JobType}.
+Context `{JobTask Job Task}.
+Context `{JobCost Job}.
+
+Let arrivals_of_tsk (arr_seq : arrival_sequence Job) tsk t1 t2 :=
+  [seq j <- arrivals_between arr_seq t1 t2 | job_task j == tsk].
+
+(** Build a network calculus flow cumulative curve (c.f. flow_cc in
+    ../cumulative_curves.v) corresponding to an
+    arrival sequence (c.f. prosa.behavior.arrival_sequence) on
+    a given clock (c.f. clock.v). *)
+Program Definition flow_cc_of_arrival_sequence
+        (s : arrival_sequence Job) (c : uclock) (tsk : Task) :=
+  Build_flow_cc'
+    (Build_Fup
+       (Build_Fplus
+          (fun t => (\sum_(j <- arrivals_of_tsk s tsk O (next_tick c t)) job_cost j)%:R%:E)
+          _)
+       _)
+    _.
+Next Obligation. by apply/leFP => t; rewrite lee_fin. Qed.
+Next Obligation.
+apply/asboolP => x y xley /=; rewrite lee_fin ler_nat.
+rewrite /arrivals_of_tsk /arrivals_between !big_filter.
+rewrite (@big_cat_nat _ _ _ (next_tick c x) _ (next_tick c y)) /=;
+  [|by []|by apply next_tick_leq].
+rewrite big_cat /=.
+exact: leq_addr.
+Qed.
+Next Obligation.
+apply/andP; split; last by exact/asboolP.
+apply/leFP => t.
+have: (0 <= t%:nngnum); [by []|].
+rewrite le_eqVlt => /orP[/eqP t0|tgt0].
+{ rewrite (_ : t = 0%:nng); [|exact/val_inj].
+  rewrite left_cont_closure0 next_tick_0.
+  by rewrite /arrivals_of_tsk /arrivals_between !big_nil. }
+set f := fun _ : {nonneg R} => _.
+have fp : f \is a nonNegativeF; [by apply/leFP => t'; rewrite lee_fin|].
+rewrite -[f]/(Fplus_val (Build_Fplus f fp)) left_cont_closure_ereal_sup//.
+move: tgt0; rewrite -(next_tick_gt0 c).
+case nE: next_tick => [//|n] _.
+pose t' := (((c n)%:nngnum + t%:nngnum) / 2)%:nng.
+have t'ltt : t'%:nngnum < t%:nngnum.
+{ rewrite ltr_pdivr_mulr// mulrDr mulr1 ltr_add2r.
+  by apply: uclock_lt_next_tick; rewrite nE. }
+apply: ereal_sup_ub; exists t' => [//|].
+rewrite /= /f (_ : next_tick c t' = n.+1)//.
+apply: next_tick_eq.
+{ apply/ltW/(lt_le_trans t'ltt).
+  rewrite -nE; exact: uclock_next_tick_gt. }
+move=> n'; rewrite ltnS => n'len.
+apply: (le_lt_trans (uclock_le _ n'len)).
+rewrite /= ltr_pdivl_mulr// mulrDr mulr1 ltr_add2l.
+by apply: uclock_lt_next_tick; rewrite nE.
+Qed.
+
+Definition related_arrival_flow_cc c tsk arr f :=
+  f = flow_cc_of_arrival_sequence arr c tsk.
+
+End Flow_cc_of_arrival_sequence.