typos

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

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).