diff --git a/analysis/facts/preemption/rtc_threshold/job_preemptable.v b/analysis/facts/preemption/rtc_threshold/job_preemptable.v
index 269cf64775ea3f12598e76fb240d915525d24320..8dba9cc61fa51bcf998daa6696c875db9746d56c 100644
--- a/analysis/facts/preemption/rtc_threshold/job_preemptable.v
+++ b/analysis/facts/preemption/rtc_threshold/job_preemptable.v
@@ -71,7 +71,7 @@ Section RunToCompletionThreshold.
     Proof.
       intros POS.
       unfold job_preemption_points, range, index_iota; rewrite subn0 -addn1.
-      rewrite iota_add add0n filter_cat mem_cat.
+      rewrite iotaD add0n filter_cat mem_cat.
       apply/orP; right; simpl.
       destruct (H_valid_preemption_model j) as [A1 [A2 [A3 A4]]]; auto.
       unfold job_cannot_be_nonpreemptive_after_completion in *.
@@ -111,9 +111,9 @@ Section RunToCompletionThreshold.
       erewrite last0_filter.
       + by apply/eqP; apply eq_refl.
       + unfold range, index_iota; rewrite subn0 -addn1.
-          by rewrite iota_add; destruct (iota 0 (job_cost j)). 
+          by rewrite iotaD; destruct (iota 0 (job_cost j)). 
       + unfold range, index_iota; rewrite subn0 -addn1.
-          by rewrite iota_add last0_cat //. 
+          by rewrite iotaD last0_cat //. 
       + by apply A2.
     Qed.
     
diff --git a/util/nondecreasing.v b/util/nondecreasing.v
index 1462134ca7448f7e8cd88ca6e17321a89554f74a..2a890adf4bc1bdcd1014f1b38568fe1982d92d09 100644
--- a/util/nondecreasing.v
+++ b/util/nondecreasing.v
@@ -583,20 +583,19 @@ Section NondecreasingSequence.
     Qed.
 
     (** We prove that [index_iota 0 n] produces a sequence of numbers
-        which are always one unit apart each other. *)
+        which are always one unit apart from each other. *)
     Lemma distances_of_iota_ε:
       forall n x, x \in distances (index_iota 0 n) -> x = ε.
     Proof.
       intros n x IN; induction n.
       - by unfold index_iota, distances in IN.
       - destruct n; first by unfold distances, index_iota in IN. 
-        rewrite -addn1 /index_iota subn0 iota_add in IN.
-        rewrite add0n in IN. 
-        rewrite distances_unfold_1app_last in IN; last by rewrite size_iota. 
-        move: IN; rewrite mem_cat; move => /orP [IN|IN].
+        move: IN; rewrite -addn1 /index_iota subn0 iotaD add0n.
+        rewrite distances_unfold_1app_last; last by rewrite size_iota. 
+        rewrite mem_cat => /orP [IN|IN].
         + by apply IHn; rewrite /index_iota subn0; simpl.
         + by move: IN;
-            rewrite -addn1 iota_add /last0 last_cat add0n addn1 // subSnn in_cons;
+            rewrite -addn1 iotaD /last0 last_cat add0n addn1 // subSnn in_cons;
             move => /orP [/eqP EQ|F]; subst.
     Qed.