diff --git a/bertogna_fp_comp.v b/bertogna_fp_comp.v
index af10262c64ec71ce8317b22972de8b7ff356e7a4..5bc2f0ff63513baebf1278c463fe938a2f23aaa8 100644
--- a/bertogna_fp_comp.v
+++ b/bertogna_fp_comp.v
@@ -24,14 +24,14 @@ Module ResponseTimeIterationFP.
     Variable job_deadline: Job -> nat.
     Variable job_task: Job -> sporadic_task.
 
-    (* Consider a platform with num_cpus processors, ...*)
+    (* Consider a platform with num_cpus processors, ... *)
     Variable num_cpus: nat.
 
     (* ..., and priorities based on an FP policy. *)
     Variable higher_priority: fp_policy sporadic_task.
 
     (* Next we define the fixed-point iteration for computing
-       Bertogna's response-time bound for any task in ts. *)
+       Bertogna's response-time bound of a task set. *)
     
     (* First, given a sequence of pairs R_prev = <..., (tsk_hp, R_hp)> of
        response-time bounds for the higher-priority tasks, we define an
@@ -224,7 +224,7 @@ Module ResponseTimeIterationFP.
         }
       Qed.
 
-      (* fp_claimed_bounds contains a response-time bound for every tasks in the original task set. *)
+      (* The list contains a response-time bound for every task in the task set. *)
       Lemma fp_claimed_bounds_non_empty :
         forall ts' rt_bounds tsk,
           fp_claimed_bounds ts' = Some rt_bounds ->
diff --git a/interference_bound_edf.v b/interference_bound_edf.v
index 8e610c5102939be59ccd4e0f9c3e647203358b8e..19321f0df9bc0ad609d375ee90a119cace6eaba6 100644
--- a/interference_bound_edf.v
+++ b/interference_bound_edf.v
@@ -1009,7 +1009,7 @@ Module EDFSpecificBound.
               by rewrite big_const_nat iter_addn mul1n addn0.
             Qed.
             
-            (* ... which results in proving that (a_lst + D_k) - 1 <= a_fst.
+            (* ... which results in proving that (a_lst + D_k) - t1 <= D_i.
                This holds because high-priority jobs have earlier deadlines. Therefore,
                the interference caused by the first job is bounded by D_i %% p_k - (D_k - R_k). *)
             Lemma interference_bound_edf_interference_of_j_fst_limited_by_remainder_and_slack :