diff --git a/analysis/facts/periodic/arrival_times.v b/analysis/facts/periodic/arrival_times.v
index 164cf83f3145f77ef36b0b7f0200fa4a0c3a38f8..15a7501986b72f12916e1d7fa4a6f9d15ddb1032 100644
--- a/analysis/facts/periodic/arrival_times.v
+++ b/analysis/facts/periodic/arrival_times.v
@@ -84,7 +84,7 @@ Section PeriodicArrivalTimes.
         apply first_job_arrival with (tsk0 := tsk) in EQ => //.
         now rewrite EQ in ARR; ssrlia.
       }
-      move : H_task_respects_periodic_model => [j' [ARR' [IND' [TSK' [ARRIVAL']]]]].
+      move : H_task_respects_periodic_model => [j' [ARR' [IND' [TSK' ARRIVAL']]]].
       specialize (IHn j'); feed_n 3 IHn => //; first by rewrite ARR in ARRIVAL'; ssrlia.
       rewrite IHn in IND'.
       destruct (PeanoNat.Nat.zero_or_succ (job_index arr_seq j)) as [Z | [m SUCC]]; last by ssrlia.