diff --git a/analysis/facts/model/ideal_uni_exceed.v b/analysis/facts/model/ideal_uni_exceed.v
index b30a00b3caf65513bbff293bd9d6790111942b07..b1268dfded9e5b3f051d9da0affde9b1f25f13f5 100644
--- a/analysis/facts/model/ideal_uni_exceed.v
+++ b/analysis/facts/model/ideal_uni_exceed.v
@@ -24,9 +24,9 @@ Section ExceedanceProcStateProperties.
   (** A job [j] is said to be [scheduled_at] some time [t] if and only if the
       processor state at that time is [NominalExecution j] or
       [ExceedanceExecution j]. *)
-   Lemma scheduled_at_procstate (sched : schedule (exceedance_proc_state Job)) j t:
-    scheduled_at sched j t <->
-      sched t = NominalExecution j \/ sched t = ExceedanceExecution j.
+   Lemma scheduled_at_procstate (sched : schedule (exceedance_proc_state Job)) j t :
+     scheduled_at sched j t <->
+       sched t = NominalExecution j \/ sched t = ExceedanceExecution j.
   Proof.
     split.
     -  move => SCHED.
@@ -46,7 +46,7 @@ Section ExceedanceProcStateProperties.
 
 
   (** Next we prove that the processor model under consideration is a uniprocessor
-      model i.e., only one job can be scheduled at any time instant. *)
+      model, i.e., only one job can be scheduled at any time instant. *)
   Lemma eps_is_uniproc : uniprocessor_model (exceedance_proc_state Job).
   Proof.
     rewrite /uniprocessor_model.
@@ -63,7 +63,7 @@ Section ExceedanceProcStateProperties.
   Qed.
 
   (** Next, we prove that the processor model under consideration is fully
-      consuming i.e., all the supply offered is consumed by the scheduled job. *)
+      consuming, i.e., all the supply offered is consumed by the scheduled job. *)
   Lemma eps_is_fully_consuming :
     fully_consuming_proc_model (exceedance_proc_state Job).
   Proof.
@@ -81,7 +81,7 @@ Section ExceedanceProcStateProperties.
   Qed.
 
   (** Finally we prove that the processor model under consideration is unit
-      service i.e., it provides at most one unit of service at any time instant. *)
+      service, i.e., it provides at most one unit of service at any time instant. *)
   Lemma eps_is_unit_service : unit_service_proc_model (exceedance_proc_state Job).
   Proof.
     rewrite /unit_service_proc_model.
@@ -97,7 +97,7 @@ End ExceedanceProcStateProperties.
     ideal uniprocessor with exceedance processor state. *)
 Section ExceedanceProcStateProperties1.
 
-  (** In this section we consider any type of jobs. *)
+  (** In this section, we consider any type of jobs. *)
   Context `{Job : JobType}.
 
   (** First let us define the notion of exceedance execution. A processor state
@@ -105,8 +105,8 @@ Section ExceedanceProcStateProperties1.
       [ExceedanceExecution j] for some [j]. *)
   Definition is_exceedance_exec (pstate : (exceedance_proc_state Job)) :=
     match pstate with
-    |ExceedanceExecution _ => true
-    |_ => false
+    | ExceedanceExecution _ => true
+    | _ => false
     end.
   Local Transparent scheduled_in scheduled_on service_on.