diff --git a/analysis/abstract/busy_interval.v b/analysis/abstract/busy_interval.v
index c0be07fb30f98f200d8222afd4cc25bf327eac99..4173ac3063133ccad00f5adf0aedaa31686646ac 100644
--- a/analysis/abstract/busy_interval.v
+++ b/analysis/abstract/busy_interval.v
@@ -59,9 +59,9 @@ Section LemmasAboutAbstractBusyInterval.
   Lemma job_completes_within_busy_interval :
     completed_by sched j t2.
   Proof.
-    move: (H_busy_interval) => [[/andP [_ LT] [_ _]] [_ QT2]].
-    unfold pending, has_arrived in QT2.
-    move: QT2; rewrite  /pending negb_and; move => /orP [QT2|QT2].
+    move: (H_busy_interval) => [[/andP [_ LT] _] /andP [_ QT2]].
+    unfold quiet_time, pending_earlier_and_at, pending, has_arrived in QT2.
+    move: QT2; rewrite negb_and => /orP [QT2|QT2].
     { by move: QT2 => /negP QT2; exfalso; apply QT2, ltnW. }
     by rewrite Bool.negb_involutive in QT2.
   Qed.
diff --git a/analysis/abstract/definitions.v b/analysis/abstract/definitions.v
index 6b75cd00c7d740ddc46b1d2987f73d06859f2c84..03cd3f17d9cd34f9fd981aef9ab1c2b2c3acfbb4 100644
--- a/analysis/abstract/definitions.v
+++ b/analysis/abstract/definitions.v
@@ -106,8 +106,8 @@ Section AbstractRTADefinitions.
         now). The second condition ensures that the busy window
         captures the execution of job [j]. *)
     Definition quiet_time (j : Job) (t : instant) :=
-      cumulative_interference j 0 t = cumulative_interfering_workload j 0 t /\
-      ~~ pending_earlier_and_at sched j t.
+      (cumulative_interference j 0 t == cumulative_interfering_workload j 0 t)
+      && ~~ pending_earlier_and_at sched j t.
 
     (** Based on the definition of quiet time, we say that an interval
         <<[t1, t2)>> is a (potentially unbounded) busy-interval prefix
diff --git a/analysis/abstract/ideal/iw_instantiation.v b/analysis/abstract/ideal/iw_instantiation.v
index 81a03696675feb60acc13e9ae053c1f2de34ff21..a632f7bab19ee9f027dc453c73f715d476c62c59 100644
--- a/analysis/abstract/ideal/iw_instantiation.v
+++ b/analysis/abstract/ideal/iw_instantiation.v
@@ -694,10 +694,10 @@ Section JLFPInstantiation.
         clear H_JLFP_respects_sequential_tasks.
         have zero_is_quiet_time: forall j, quiet_time_cl j 0.
         { by move => jhp ARR HP AB; move: AB; rewrite /arrived_before ltn0. }
-        move=> t QT; split; last first.
+        move=> t QT; apply/andP; split; last first.
         { rewrite negb_and Bool.negb_involutive; apply/orP.
           by case ARR: (arrived_before j t); [right | left]; [apply QT | ]. }
-        { erewrite cumulative_interference_split, cumulative_interfering_workload_split; apply/eqP; rewrite eqn_add2l.
+        { erewrite cumulative_interference_split, cumulative_interfering_workload_split; rewrite eqn_add2l.
           rewrite cumulative_i_ohep_eq_service_of_ohep//.
           rewrite //= cumulative_iw_hep_eq_workload_of_ohep eq_sym; apply/eqP.
           apply all_jobs_have_completed_equiv_workload_eq_service => //.
@@ -716,7 +716,7 @@ Section JLFPInstantiation.
         clear H_JLFP_respects_sequential_tasks.
         have zero_is_quiet_time: forall j, quiet_time_cl j 0.
         { by move => jhp ARR HP AB; move: AB; rewrite /arrived_before ltn0. }
-        move => t [T0 T1] jhp ARR HP ARB.
+        move => t /andP [T0 T1] jhp ARR HP ARB.
         eapply all_jobs_have_completed_equiv_workload_eq_service with
           (P := fun jhp => hep_job jhp j) (t1 := 0) (t2 := t) => //.
         erewrite service_of_jobs_case_on_pred with (P2 := fun j' => j' != j).
@@ -732,7 +732,7 @@ Section JLFPInstantiation.
             by apply in_arrivals_implies_arrived_between in IN. }
           erewrite service_of_jobs_equiv_pred with (P2 := pred0) => [|//].
           erewrite workload_of_jobs_equiv_pred with (P' := pred0) => [|//].
-          move: T0; erewrite cumulative_interference_split, cumulative_interfering_workload_split => /eqP; rewrite eqn_add2l => /eqP EQ.
+          move: T0; erewrite cumulative_interference_split, cumulative_interfering_workload_split; rewrite eqn_add2l => /eqP EQ.
           rewrite EQ; clear EQ; apply/eqP; rewrite eqn_add2l.
           by erewrite workload_of_jobs_pred0, service_of_jobs_pred0.
         }
@@ -743,7 +743,7 @@ Section JLFPInstantiation.
             by move: EQ => /eqP EQ; rewrite Bool.andb_true_r; apply/eqP; rewrite eqb_id; subst. }
           erewrite service_of_jobs_equiv_pred with (P2 := eq_op j) => [|//].
           erewrite workload_of_jobs_equiv_pred with (P' := eq_op j) => [|//].
-          move: T0; erewrite cumulative_interference_split, cumulative_interfering_workload_split => /eqP; rewrite eqn_add2l => /eqP EQ.
+          move: T0; erewrite cumulative_interference_split, cumulative_interfering_workload_split; rewrite eqn_add2l => /eqP EQ.
           rewrite EQ; clear EQ; apply/eqP; rewrite eqn_add2l.
           apply/eqP; eapply all_jobs_have_completed_equiv_workload_eq_service with
             (P := eq_op j) (t1 := 0) (t2 := t) => //.