diff --git a/backlogged_period.v b/backlogged_period.v
index 5c06c87338b347e5755096bcfe96c20e482c5cbb..011a9a9246b94ab8dee942af2223a0158c013588 100644
--- a/backlogged_period.v
+++ b/backlogged_period.v
@@ -12,7 +12,7 @@
 (******************************************************************************)
 
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype order ssrnat.
-From mathcomp Require Import choice seq fintype finfun bigop ssralg ssrnum rat.
+From mathcomp Require Import choice seq fintype finfun bigop ssralg ssrnum rat interval.
 From mathcomp.analysis Require Import reals ereal nngnum posnum boolp classical_sets.
 From mathcomp.dioid Require Import HB_wrappers dioid.
 From mathcomp.dioid Require Import complete_lattice complete_dioid.
@@ -24,12 +24,13 @@ Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
 Local Open Scope classical_set_scope.
+Local Open Scope order_scope.
 Local Open Scope ring_scope.
 
 Import Order.Theory GRing.Theory Num.Theory DualAddTheory.
 
-Definition backlogged_period (A D : F) (u v : R) :=
-  u <= v /\ forall x : {nonneg R}, u < x%:nngnum <= v -> (D x < A x)%E.
+Definition backlogged_period (A D : F) (I : interval {nonneg R}) :=
+  forall x, x \in I -> (D x < A x)%E.
 
 Lemma start_proof (A D : F) (t : {nonneg R}) :
   { y : {nonneg R} | y%:nngnum%:E
@@ -55,7 +56,8 @@ have Hy : [set (u)%:nngnum%:E | u in s] (y)%:nngnum%:E; [by exists y|].
 by exfalso; move: E => /ereal_sup_ninfty /(_ y%:nngnum%:E Hy).
 Qed.
 
-Definition start (A D : F) (t : {nonneg R}) : {nonneg R} := proj1_sig (start_proof A D t).
+Definition start (A D : F) (t : {nonneg R}) : {nonneg R} :=
+  proj1_sig (start_proof A D t).
 
 Lemma start_non_decr (A D : flow_cc) : {homo (start A D) : x y / x <= y }.
 Proof.
@@ -76,7 +78,7 @@ apply: ub_ereal_sup => _ [z' [Hz' H'z'] <-].
 by apply: ereal_sup_ub; exists z' => //; split=> //; move: Hxy; apply: le_trans.
 Qed.
 
-Lemma start_eq (A D : flow_cc) (t : {nonneg R}) : A (start A D t) = D (start A D t).
+Lemma start_eq (A D : flow_cc) t : A (start A D t) = D (start A D t).
 Proof.
 set s := start _ _ _.
 case (@eqP _ s 0%:nng) => [-> | /eqP Hs]; [by rewrite !flow_cc0|].
@@ -144,32 +146,29 @@ by rewrite lee_fin -leEsub.
 Qed.
 
 Lemma start_t_is_a_backlogged_period (S : partial_server) (A D : flow_cc) t :
-  S A D -> backlogged_period A D (start A D t)%:nngnum t%:nngnum.
+  S A D -> backlogged_period A D `]start A D t, t].
 Proof.
-move=> HAD; split=> [| u /andP[Hsu Hut]]; [exact: start_le|].
+move=> HAD u uI.
 rewrite lt_def; move: (server_le HAD) => /leFP /(_ u) ->; rewrite andbT.
-apply/eqP => H; move: Hsu; apply/negP; rewrite -leNgt.
-rewrite -lee_fin /start; case: start_proof => _ ->.
-by rewrite le_maxr; apply/orP; right; apply: ereal_sup_ub; exists u.
+apply/eqP => H.
+have: start A D t < u by rewrite (itvP uI).
+apply/negP; rewrite -leNgt.
+rewrite leEsub /= -lee_fin /start; case: start_proof => _ ->.
+rewrite le_maxr; apply/orP; right.
+by apply: ereal_sup_ub; exists u; rewrite //= (itvP uI) H.
 Qed.
 
-Lemma backlogged_period_sub_interval u v u' v' A D :
-  u <= u' -> v' <= v -> u' <= v' ->
-  backlogged_period A D u v -> backlogged_period A D u' v'.
-Proof.
-move=> Huu' Hvv' Hu'v' [_ Huv]; split=> // t /andP[Hu't Htv'].
-apply/Huv/andP; split.
-{ by move: Hu't; apply: le_lt_trans. }
-by move: Hvv'; apply: le_trans.
-Qed.
+Lemma backlogged_period_sub_interval I I' A D : (I' <= I)%O ->
+  backlogged_period A D I -> backlogged_period A D I'.
+Proof. by move=> /subitvP I'subI blI + /I'subI. Qed.
 
-Lemma backlogged_period_weaken_cond n (S : n.-server) A D (HS : S A D) u v
+Lemma backlogged_period_weaken_cond n (S : n.-server) A D (HS : S A D) I
       (P P' : pred 'I_n) :
   (forall i, P i -> P' i) ->
-  backlogged_period (\sum_(i | P i) A i)%C (\sum_(i | P i) D i)%C u v
-  -> backlogged_period (\sum_(i | P' i) A i)%C (\sum_(i | P' i) D i)%C u v.
+  backlogged_period (\sum_(i | P i) A i)%C (\sum_(i | P i) D i)%C I
+  -> backlogged_period (\sum_(i | P' i) A i)%C (\sum_(i | P' i) D i)%C I.
 Proof.
-move=> HPP' [Huv HuvP]; split=> // t Ht.
+move=> HPP' blP t tinI.
 rewrite !flow_cc_sumE.
 under eq_bigr => i _ do rewrite -fin_flow_ccE.
 under [X in (_ < X)%E]eq_bigr => i _ do rewrite -fin_flow_ccE.
@@ -184,7 +183,7 @@ apply: lte_le_dadd => //.
   under eq_bigr => i _ do rewrite fin_flow_ccE.
   under [X in (_ < X)%E]eq_bigr => i _ do rewrite fin_flow_ccE.
   rewrite -!flow_cc_sumE.
-  exact: HuvP. }
+  exact: blP. }
 rewrite -!dsumEFin; apply: lee_dsum => i _; rewrite !fin_flow_ccE.
 by move: (nserver_le HS i) => /leFP.
 Qed.
diff --git a/services.v b/services.v
index 2c5a32bc353c7f1cea82fb2ea4caa6527aad78e7..ed0ded14e3186e4a8a06d73b381886d55c094093 100644
--- a/services.v
+++ b/services.v
@@ -13,7 +13,7 @@
 (******************************************************************************)
 
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype order ssrnat.
-From mathcomp Require Import choice seq fintype finfun bigop ssralg ssrnum rat.
+From mathcomp Require Import choice seq fintype finfun bigop ssralg ssrnum rat interval.
 From mathcomp.analysis Require Import reals ereal nngnum posnum boolp classical_sets.
 From mathcomp.dioid Require Import HB_wrappers dioid.
 From mathcomp.dioid Require Import complete_lattice complete_dioid.
@@ -45,8 +45,9 @@ Definition is_min_service S beta := forall A, is_min_service_for S beta A.
 (* Final : def 5.5 p108 *)
 Definition is_strict_min_service (S : flow_cc -> flow_cc -> Prop) (beta : F) :=
   forall A D, S A D ->
-         forall u v : {nonneg R}, backlogged_period A D u%:nngnum v%:nngnum ->
-                (beta (insubd 0%:nng (v%:nngnum - u%:nngnum))%R <= D v - D u)%dE.
+    forall u v : {nonneg R}, (u%:nngnum <= v%:nngnum)%R ->
+      backlogged_period A D `]u, v] ->
+      (beta (insubd 0%:nng (v%:nngnum - u%:nngnum))%R <= D v - D u)%dE.
 
 (** Max service *)
 (* def p132 *)
diff --git a/static_priority.v b/static_priority.v
index f38687224a6631f9529eaa11704194e9632c6ca6..c287211c4fe3381de2593275072187ce69ed60c1 100644
--- a/static_priority.v
+++ b/static_priority.v
@@ -12,7 +12,7 @@
 (******************************************************************************)
 
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype order ssrnat.
-From mathcomp Require Import choice seq fintype finfun bigop ssralg ssrnum rat.
+From mathcomp Require Import choice seq fintype finfun bigop ssralg ssrnum rat interval.
 From mathcomp.analysis Require Import reals ereal nngnum posnum boolp classical_sets.
 From mathcomp.dioid Require Import HB_wrappers dioid.
 From mathcomp.dioid Require Import complete_lattice complete_dioid.
@@ -74,23 +74,22 @@ by rewrite (sum_flow_cc_equiv_at_t HS) H.
 Qed.
 
 (* Lemma 25 page 175 *)
-Lemma backlogged_period_server_cond n (S : (n.+1).-server) A D (s t : R)
+Lemma backlogged_period_server_cond n (S : (n.+1).-server) A D I
       (P : pred 'I_n.+1):
   S A D ->
-  (s <= t
-   /\ forall u : {nonneg R}, s < u%:nngnum <= t -> exists i, P i /\ ((D i) u < (A i) u)%E)
-  <-> backlogged_period (\sum_(i | P i) A i)%C (\sum_(i | P i) D i)%C s t.
+  (forall u : {nonneg R}, u \in I -> exists i, P i /\ ((D i) u < (A i) u)%E)
+  <-> backlogged_period (\sum_(i | P i) A i)%C (\sum_(i | P i) D i)%C I.
 Proof.
 move=> Hs; split.
 { rewrite /backlogged_period.
-  move=> [Hst H]; split=> // u Hu.
+  move=> H u Hu.
   move: (H _ Hu) => [i [Hi HAD]].
   rewrite lt_def; apply/andP; split.
   { apply/negP => /eqP /(proj2 (sum_flow_cc_equiv_cond P Hs u)) /(_ _ Hi) /eqP.
     by apply/negP; move: HAD; rewrite lt_def => /andP[]. }
   rewrite !flow_cc_sumE; apply: lee_dsum => j _.
   exact/leFP/(nserver_le Hs). }
-move=> [Hst H]; split=> // u Hu.
+move=> H u Hu.
 move: (H _ Hu); rewrite lt_def => /andP[H_u _].
 rewrite not_existsP => Hf.
 move: H_u => /eqP; apply.
@@ -102,32 +101,28 @@ by rewrite -leNgt.
 Qed.
 
 (* Lemma 25 page 175 without condition *)
-Lemma backlogged_period_eqv n (S : (n.+1).-server) A D (s t : R) :
+Lemma backlogged_period_eqv n (S : (n.+1).-server) A D I :
   S A D ->
-  (s <= t /\ forall u : {nonneg R}, s < u%:nngnum <= t -> exists i, ((D i) u < (A i) u)%E)
-  <-> backlogged_period (\sum_i A i)%C (\sum_i D i)%C s t.
+  (forall u : {nonneg R}, u \in I -> exists i, ((D i) u < (A i) u)%E)
+  <-> backlogged_period (\sum_i A i)%C (\sum_i D i)%C I.
 Proof.
 move=> HS; split.
-{ move=> [Hst H].
-  rewrite -(backlogged_period_server_cond _ _ _ HS).
-  split=> // u Hu.
+{ move=> H.
+  rewrite -(backlogged_period_server_cond _ _ HS) => u Hu.
   move: (H _ Hu) => [i HAD].
   by exists i. }
-move=> [Hst H]; split=> // u Hu.
-move: (conj Hst H) => {H}.
-rewrite -/(backlogged_period _ _ s t).
-rewrite -(backlogged_period_server_cond _ _ _ HS) => [[_ /(_ _ Hu)[i [_ H]]]].
+move=> H u Hu.
+move: H; rewrite -(backlogged_period_server_cond _ _ HS) => /(_ _ Hu)[i [_ H]].
 by exists i.
 Qed.
 
-Lemma backlogged_period_aggregate  n (S : (n.+1).-server) s t A D :
+Lemma backlogged_period_aggregate  n (S : (n.+1).-server) A D I :
   S A D ->
-  forall i, backlogged_period (A i) (D i) s t ->
-            backlogged_period (\sum_i A i)%C (\sum_i D i)%C s t.
+  forall i, backlogged_period (A i) (D i) I ->
+       backlogged_period (\sum_i A i)%C (\sum_i D i)%C I.
 Proof.
-move=> Hs i [Hst H].
-rewrite -(backlogged_period_eqv s t Hs).
-split=> // u Hu.
+move=> Hs i H.
+rewrite -(backlogged_period_eqv I Hs) => u Hu.
 by exists i; apply H.
 Qed.
 
@@ -135,11 +130,11 @@ Qed.
 Definition preemptive_SP n (S : (n.+1).-server) (prior : 'I_n.+1 -> nat) :=
   forall A D,
     S A D ->
-    forall i, forall s t : {nonneg R},
+    forall i, forall s t : {nonneg R}, s%:nngnum <= t%:nngnum ->
         backlogged_period
           (\sum_(j < n.+1 | (prior j < prior i)%nat) A j)%C
           (\sum_(j < n.+1 | (prior j < prior i)%nat) D j)%C
-          s%:nngnum t%:nngnum ->
+          `]s, t] ->
         (D i) s = (D i) t.
 
 (* Theorem 7.6 p170 *)
@@ -156,10 +151,10 @@ Theorem SP_residual_service_curve n (S : (n.+1).-server)
          (fun t => Order.max 0%:E
             (beta t - (\sum_(j < n.+1 | (prior j < prior i)%nat) (alpha j))%F t))%dE).
 Proof.
-move=> Hbeta alpha i _ _ [A [D [HAD [-> [-> Halpha]]]]] u v Huv.
+move=> Hbeta alpha i _ _ [A [D [HAD [-> [-> Halpha]]]]] u v Huv bluv.
 move: (Hbeta (\sum_i A i)%C (\sum_i D i)%C (aggregate_server_prop HAD) u v).
-move=> /(_ (@backlogged_period_aggregate _ _ _ _ _ _ HAD i _)).
-move=> /(_ Huv) => Hbeta_sum.
+move=> /(_ Huv (@backlogged_period_aggregate _ _ _ _ _ HAD i _)).
+move=> Hbeta_sum.
 pose sum_A_higher_i := (\sum_(j | (prior j < prior i)%nat) A j)%C.
 pose sum_D_higher_i := (\sum_(j | (prior j < prior i)%nat) D j)%C.
 pose sum_alpha_higher_i := (\sum_(j | (prior j < prior i)%nat) alpha j)%F.
@@ -177,12 +172,12 @@ suff: forall w : {nonneg R}, p <= w <= v ->
   rewrite le_maxl; apply/andP; split.
   { rewrite -!fin_flow_ccE -NEFin -daddEFin lee_fin subr_ge0.
     rewrite -lee_fin !fin_flow_ccE.
-    by apply/ndFP; move: Huv => -[]. }
+    exact/ndFP. }
   have <- : D i p = D i u; [exact: (HS _ _ HAD)|].
   pose w := (t%:nngnum + p%:nngnum)%:nng.
   have Hw_pv : p <= w <= v.
   { rewrite !leEsub /= ler_addr; apply/andP; split=> //.
-    move: Huv Ht => -[Huv _].
+    move: Ht.
     rewrite leEsub insubdK /=; [|by rewrite /in_mem /= subr_ge0].
     by rewrite ler_subr_addl -ler_subr_addr -ler_subr_addl; apply: le_trans. }
   rewrite (_ : t = insubd 0%:nng (w%:nngnum - p%:nngnum)); last first.
@@ -228,20 +223,20 @@ have -> :
   rewrite ltn_neqAle /= andbC.
   apply/f_equal2/negb_inj => //=.
   rewrite !negbK; exact: inj_eq. }
-have Hpw_backl : backlogged_period (\sum_i A i)%C (\sum_i D i)%C p%:nngnum w%:nngnum.
-{ split=> // x /andP[Hpx Hxw].
+have Hpw_backl : backlogged_period (\sum_i A i)%C (\sum_i D i)%C `]p, w].
+{ move=> x xinpw.
   case: (leP x u) => Hwu.
   { move: (backlogged_period_weaken_cond
-             HAD (fun _ _ => eq_refl true) Hpu_backl) => -[_].
-    by apply; apply/andP; split. }
-  move: Huv.
+             HAD (fun _ _ => eq_refl true) Hpu_backl).
+    by apply; rewrite in_itv /= (itvP xinpw). }
+  move: bluv.
   rewrite (_ : A i = (\sum_(j | j == i) A j)%C); [|by rewrite big_pred1_eq].
   rewrite (_ : D i = (\sum_(j | j == i) D j)%C); [|by rewrite big_pred1_eq].
   move=> H'.
-  move: (backlogged_period_weaken_cond HAD (fun _ _ => eq_refl true) H') => -[_].
-  apply; rewrite -ltEsub Hwu /=.
-  by move: Hwv; rewrite leEsub /=; apply: le_trans. }
-move: (Hbeta _ _ (aggregate_server_prop HAD) _ _ Hpw_backl) => H.
+  move: (backlogged_period_weaken_cond HAD (fun _ _ => eq_refl true) H').
+  apply; rewrite in_itv /= Hwu /=.
+  by apply: le_trans Hwv; rewrite (itvP xinpw). }
+move: (Hbeta _ _ (aggregate_server_prop HAD) _ _ Hpw Hpw_backl) => H.
 apply: (le_trans H).
 rewrite -!fin_flow_cc_sumE -!NEFin -!daddEFin.
 rewrite (bigID (fun j0 => (prior j0 <= prior i)%nat)) /=.
@@ -261,7 +256,7 @@ have H_D_after_i :
   { by move=> j0 Hj0; move: Hj; apply ltn_trans. }
   rewrite -/sum_A_higher_i -/sum_D_higher_i.
   move: Hpu_backl.
-  exact: backlogged_period_sub_interval. }
+  exact/backlogged_period_sub_interval/andP. }
 case: (leP w u) => Hwu.
 { rewrite !(daddEFin, NEFin) !fin_flow_cc_sumE.
   rewrite -H_D_after_i; [|by apply/andP; split].
@@ -273,14 +268,13 @@ have H_D_after_i_u_w :
   (\sum_(j | (prior i < prior j)%nat) D j)%C u =
   (\sum_(j | (prior i < prior j)%nat) D j)%C w.
 { rewrite !flow_cc_sumE; apply: eq_bigr => j' Hj'.
-  apply: (HS _ _ HAD).
+  apply: (HS _ _ HAD); [exact: ltW|].
   apply: (backlogged_period_weaken_cond HAD (P:=(fun k=> prior k == prior i))).
   { by move=> k /eqP ->. }
-  split=> [| x]; [exact: ltW|].
+  move=> x.
   rewrite -d_i_sum_i -a_i_sum_i.
-  move: Huv x.
-  apply backlogged_period_sub_interval => //.
-  exact: ltW. }
+  apply: backlogged_period_sub_interval bluv x.
+  exact/andP. }
 rewrite !(daddEFin, NEFin) !fin_flow_cc_sumE.
 rewrite -H_D_after_i_u_w -H_D_after_i.
 rewrite -!fin_flow_cc_sumE -!(daddEFin, NEFin).