diff --git a/implementation/definitions/maximal_arrival_sequence.v b/implementation/definitions/maximal_arrival_sequence.v
index 77f235f36de4bdedf3094d520b2a00612b504655..38e1382955613770e432e9b04631e4bf8df7721a 100644
--- a/implementation/definitions/maximal_arrival_sequence.v
+++ b/implementation/definitions/maximal_arrival_sequence.v
@@ -50,12 +50,12 @@ Section MaximalArrivalSequence.
         
         The high-level idea is as follows. Let us assume that the length of
         the arrival prefix is [Δ]. To preserve the sub-additive property, one
-        needs to go through all suffixes of the arrival prefix an pick
+        needs to go through all suffixes of the arrival prefix and pick
         the minimum. *)
     Definition jobs_remaining (arr_prefix : seq nat) :=
       supremum leq [seq (max_arrivals tsk Δ.+1 - suffix_sum arr_prefix Δ) | Δ <- iota 0 (size arr_prefix).+1].
     
-    (** Further, We define function [next_max_arrival] to handle a special
+    (** Further, We define the function [next_max_arrival] to handle a special
         case: when the arrival prefix is empty, the function returns the value
         of the arrival curve with a window length of [1]. Otherwise, it
         returns the number the number of jobs that can additionally be
diff --git a/implementation/facts/maximal_arrival_sequence.v b/implementation/facts/maximal_arrival_sequence.v
index 328a60bc64e5fc46ba09e51b6d985fa9ff6fac18..6389a10aacca7cf0ba7cd5efc7829b2d97c2ea2f 100644
--- a/implementation/facts/maximal_arrival_sequence.v
+++ b/implementation/facts/maximal_arrival_sequence.v
@@ -51,7 +51,7 @@ Section MaximalArrivalSequence.
       /\ job_arrival j = t
       /\ job_cost j <= task_cost tsk.
 
-  (** Finally, we assume that all job generated by [generate_jobs_at] are unique. *) 
+  (** Finally, we assume that all jobs generated by [generate_jobs_at] are unique. *) 
   Hypothesis H_jobs_unique:
     forall (t1 t2 : instant),
       uniq (arrivals_between (concrete_arrival_sequence generate_jobs_at ts) t1 t2).