diff --git a/analysis/facts/behavior/supply.v b/analysis/facts/behavior/supply.v
index 7884e0f748c224b7720e7cf3507d0b09e3ea6d75..5fe44544f09d6a5b25cbebe4091d407bcab436a7 100644
--- a/analysis/facts/behavior/supply.v
+++ b/analysis/facts/behavior/supply.v
@@ -72,15 +72,25 @@ Section UnitService.
     by rewrite /is_blackout /has_supply /supply_at; case: supply_in => [|[]].
   Qed.
 
-  (** We show that supply during an interval <<[t, t + δ)>> is bounded
-      by [δ]. *)
-  Lemma supply_at_le_1 :
+  (** We note that supply is bounded at all times by [1] ... *)
+  Remark supply_at_le_1 :
     forall t,
       supply_at sched t <= 1.
   Proof. by move=> t; apply H_unit_supply_proc_model. Qed.
 
-  (** We show that supply during an interval <<[t, t + δ)>> is bounded
-      by [δ]. *)
+  (** ... and as a trivial consequence, we show that the service of
+      any job is either [0] or [1]. *)
+  Corollary unit_supply_proc_service_case :
+    forall j t,
+      service_at sched j t = 0 \/ service_at sched j t = 1.
+  Proof.
+    move=> j t.
+    have SER := service_at_le_supply_at sched j t.
+    have SUP := supply_at_le_1 t.
+    by lia.
+  Qed.
+
+  (** We show that supply during an interval <<[t, t + δ)>> is bounded by [δ]. *)
   Lemma supply_during_bound :
     forall t δ,
       supply_during sched t (t + δ) <= δ.
diff --git a/util/list.v b/util/list.v
index e3073f6d7473563f74a538d8ef9e551783218aba..5859b16d6e9d09e155a782c664d8f24c378e162f 100644
--- a/util/list.v
+++ b/util/list.v
@@ -292,6 +292,32 @@ End RemList.
 (** Additional lemmas about sequences. *)
 Section AdditionalLemmas.
 
+  (** First, we show that a sequence [xs] contains the same elements
+      as a sequence [undup xs]. *)
+  Lemma in_seq_equiv_undup :
+    forall {X : eqType} (xs : seq X) (x : X),
+      (x \in undup xs) = (x \in xs).
+  Proof.
+    move=> X xs; induction xs as [ | x0 xs IHxs]; first by done.
+    move=> x; rewrite in_cons //=; case IN: (x0 \in xs).
+    - case EQ: (x == x0).
+      + by move: EQ => /eqP EQ; subst; rewrite orTb IHxs.
+      + by rewrite orFb; apply IHxs.
+    - by rewrite in_cons IHxs.
+  Qed.
+
+  (** We prove that [x::xs = ys] is a sufficient condition for [x] to
+      be in [ys]. *)
+  Lemma mem_head_impl :
+    forall {X : eqType} (x : X) (xs ys : seq X),
+      x::xs = ys ->
+      x \in ys.
+  Proof.
+    intros X x xs [ |y ys] EQ; first by done.
+    move: EQ => /eqP; rewrite eqseq_cons => /andP [/eqP EQ _].
+    by subst y; rewrite in_cons; apply/orP; left.
+  Qed.
+
   (** We show that if [n > 0], then [nth (x::xs) n = nth xs (n-1)]. *)
   Lemma nth0_cons :
     forall x xs n,
diff --git a/util/minmax.v b/util/minmax.v
index cef2860f20f9a211523a1423be77559d95ee5fd1..de5924316f4a3b8cf9d8f4123559eb07dfce99fa 100644
--- a/util/minmax.v
+++ b/util/minmax.v
@@ -1,5 +1,5 @@
 From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.
-Require Export prosa.util.notation prosa.util.nat prosa.util.list.
+Require Export prosa.util.notation prosa.util.nat prosa.util.list prosa.util.setoid.
 
 (** Additional lemmas about [BigMax]. *)
 Section ExtraLemmas.
@@ -12,6 +12,19 @@ Section ExtraLemmas.
       x \in xs -> P x -> F x <= \max_(i <- xs | P i) F i.
   Proof. by move=> X F P xs x IN Px; rewrite (big_rem x) //= Px leq_maxl. Qed.
 
+  (** Similarly, we show that for a constant [n] to be bounded by [max
+      { F i | ∀ i ∈ xs, P i}], it is sufficient to find an element [x
+      ∈ xs] such that [P x] and [n <= F x]. *)
+  Corollary leq_bigmax_sup :
+    forall {X : eqType} (P : pred X) (F : X -> nat) (xs : seq X) (n : nat),
+      (exists x, x \in xs /\ P x /\ n <= F x) ->
+      n <= \max_(x <- xs | P x) F x.
+  Proof.
+    move=> X P F xs n [x [IN [Px LE]]].
+    apply: leq_trans; first by exact: LE.
+    by apply leq_bigmax_cond_seq.
+  Qed.
+
   (** Next, we show that the fact [max { F i | ∀ i ∈ xs, P i} <= m] for
       some [m] is equivalent to the fact that [∀ x ∈ xs, P x -> F x <= m]. *)
   Lemma bigmax_leq_seqP : 
diff --git a/util/sum.v b/util/sum.v
index 3dc26cefe023302b48a3326aa2c3a560bba5c5ae..c027f9f2bd47e0d9e615dc27f7d3bdb0e13bb1dc 100644
--- a/util/sum.v
+++ b/util/sum.v
@@ -96,6 +96,20 @@ Section SumsOverSequences.
       by rewrite (leq_trans (max_leq_add m1 m2)) ?leq_add.
     Qed.
 
+    (** We show that if [r1] is a subsequence of [r2], then the sum of
+        function [F] over elements satisfying predicate [P] in [r1] is
+        less than or equal to the sum over elements satisfying [P] in [r2].  *)
+    Lemma sum_le_subseq :
+      forall r1 r2,
+        subseq r1 r2 ->
+        \sum_(x <- r1 | P x) F x <= \sum_(x <- r2 | P x) F x.
+    Proof.
+      move => r1 r2 SUB.
+      apply: sub_le_big_seq => //= [x y|]; first exact: leq_addr.
+      rewrite count_subseqP.
+      by exists r1.
+    Qed.
+
   End SumOfOneFunction.
 
   (** In this section, we show some properties of the sum performed over two different functions. *)