Bump MathComp lower bound to >= 1.16.0 and Coq to >= 8.16.

Currently a draft as I need to update the OPAM package first. (https://github.com/coq/opam-coq-archive/pull/2516 merged)

I also don't know how to update the Docker image bbbrandenburg/alectryon-ci:1.14.0-coq-8.15.0 to some bbbrandenburg/alectryon-ci:1.16.0-coq-8.16.0

Fixes: #85 (closed)

analysis/facts/transform/edf_opt.v

@@ -255,7 +255,6 @@ Section MakeEDFAtFacts.
         now apply scheduled_job_in_sched_has_later_deadline.
       - have EX: (exists t', scheduled_at sched j t').
         {
-          try ( apply swap_job_scheduled with (t1 := t_edf) (t2 := find_swap_candidate sched t_edf j_orig) (t0 := t) ) ||
           apply swap_job_scheduled with (t1 := t_edf) (t2 := find_swap_candidate sched t_edf j_orig) (t := t).
           now move: SCHED; rewrite /sched' /make_edf_at SCHED_orig.
         }
@@ -418,7 +417,6 @@ Section MakeEDFAtFacts.
       + by rewrite -EQ; apply fsc_range1.
     - case (boolP(t_edf == t)) => [/eqP EQ'| /eqP NEQ'].
       + move=> SCHED_j.
-        try ( have ARR_j: job_arrival j <= t_edf by apply fsc_found_job_arrival with (sched0 := sched) (j1 := j_orig) => //; rewrite scheduled_at_def ) ||
         have ARR_j: job_arrival j <= t_edf by apply fsc_found_job_arrival with (sched := sched) (j1 := j_orig) => //; rewrite scheduled_at_def.
         now rewrite -EQ'.
       + move=> SCHED_j.
@@ -701,7 +699,7 @@ Section EDFPrefixInclusion.
       by rewrite scheduled_at_def /edf_transform_prefix; apply /eqP.
     apply fsc_range1 => //.
     - by apply edf_prefix_jobs_must_arrive.
-    - try ( apply edf_prefix_scheduled_job_has_later_deadline with (sched0 := sched) (horizon := h2) => // ) || apply edf_prefix_scheduled_job_has_later_deadline with (sched := sched) (horizon := h2) => //.
+    - apply edf_prefix_scheduled_job_has_later_deadline with (sched := sched) (horizon := h2) => //.
   Qed.
 
 End EDFPrefixInclusion.
@@ -796,7 +794,7 @@ Section EDFTransformFacts.
                                         H_completed_jobs_dont_execute H_no_deadline_misses t_dl.+1) => [_ [_ DL]].
       now apply (DL j t).
     - by apply (identical_prefix_inclusion _ _ t_dl.+1) => //; apply edf_finite_prefix.
-    - try ( by apply edf_prefix_scheduled_job_has_later_deadline with (sched0 := sched) (horizon := t.+1) ) || by apply edf_prefix_scheduled_job_has_later_deadline with (sched := sched) (horizon := t.+1).
+    - by apply edf_prefix_scheduled_job_has_later_deadline with (sched := sched) (horizon := t.+1).
   Qed.
 
   (** We observe that no new jobs are introduced: any job scheduled in the EDF
@@ -815,15 +813,12 @@ Section EDFTransformFacts.
     forall j t, scheduled_at sched j t -> exists t', scheduled_at sched_edf j t'.
   Proof.
     move=> j t SCHED_j.
-    try ( have EX: exists t', scheduled_at (edf_transform_prefix sched (job_deadline j)) j t'
-      by apply edf_prefix_job_scheduled' with (t0 := t) ) ||
     have EX: exists t', scheduled_at (edf_transform_prefix sched (job_deadline j)) j t'
       by apply edf_prefix_job_scheduled' with (t := t).
     move: EX => [t' SCHED'].
     exists t'.
     rewrite /sched_edf /edf_transform scheduled_at_def.
     rewrite (edf_prefix_inclusion _ _ _ _ t'.+1 (job_deadline j)) -?scheduled_at_def=> //.
-    try ( now apply edf_prefix_scheduled_job_has_later_deadline with (sched0 := sched) (horizon := job_deadline j) ) ||
     now apply edf_prefix_scheduled_job_has_later_deadline with (sched := sched) (horizon := job_deadline j).
   Qed.