Deprecate ltn_leq_trans

analysis/definitions/schedule_prefix.v

@@ -42,7 +42,7 @@ Section PrefixDefinition.
   Proof.
     move=> sched sched' h IDENT h' INCL t LT_h'.
     apply IDENT.
-    now apply (ltn_leq_trans LT_h').
+    now apply (leq_trans LT_h').
   Qed.
 
 End PrefixDefinition.

analysis/facts/behavior/completion.v

@@ -74,7 +74,7 @@ Section CompletionFacts.
       job_cost_positive j.
   Proof.
     move=> t INCOMP.
-    apply: (ltn_leq_trans _);
+    apply: (leq_trans _);
       last by apply leq_subr.
     apply incomplete_is_positive_remaining_cost.
     exact INCOMP.
@@ -379,7 +379,7 @@ Section CompletedJobs.
     move=> IDEAL SERVICE_BOUND j t SCHED.
     have UB := SERVICE_BOUND j t.+1.
     have POS := IDEAL _ _ SCHED.
-    apply ltn_leq_trans with (n := service sched j t.+1) => //.
+    apply leq_trans with (n := service sched j t.+1) => //.
     rewrite -service_last_plus_before /service_at.
     by rewrite -{1}(addn0 (service sched j t)) ltn_add2l.
   Qed.

analysis/facts/behavior/deadlines.v

@@ -49,7 +49,7 @@ Section DeadlineFacts.
       rewrite -(ltn_add2l (service sched j t)) addn0.
       rewrite service_cat;
         last by (apply ltnW; apply incomplete_implies_later_deadline).
-      apply ltn_leq_trans with (n := job_cost j);
+      apply leq_trans with (n := job_cost j);
         first by rewrite less_service_than_cost_is_incomplete.
       by apply MET.
     Qed.

analysis/facts/job_index.v

@@ -151,7 +151,7 @@ Section JobIndexLemmas.
     rewrite -> arrivals_P_cat with (t := job_arrival j1); last by apply job_arrival_between in IN1 => //.
     rewrite !index_cat ifT; last by eapply arrival_lt_implies_job_in_arrivals_between_P; eauto.
     rewrite ifF.
-    - eapply ltn_leq_trans; [ | now erewrite leq_addr].
+    - eapply leq_trans; [ | now erewrite leq_addr].
       rewrite index_mem.
       now eapply arrival_lt_implies_job_in_arrivals_between_P; eauto.
     - apply Bool.not_true_is_false; intro T.
@@ -192,7 +192,7 @@ Section JobIndexLemmas.
     rewrite -> task_arrivals_cat with (t_m := job_arrival j1); try by ssrlia.
     rewrite -H_same_task !index_cat ifT; try by apply arrives_in_task_arrivals_up_to.
     rewrite ifF.
-    - now eapply ltn_leq_trans;
+    - now eapply leq_trans;
         [apply index_job_lt_size_task_arrivals_up_to_job | rewrite leq_addr].
     - apply Bool.not_true_is_false; intro T.
       now apply job_arrival_between in T; try ssrlia.
@@ -359,7 +359,7 @@ Section PreviousJob.
     exists (nth j (task_arrivals_up_to_job_arrival arr_seq j) k).
     set (jk := nth j (task_arrivals_up_to_job_arrival arr_seq j) k).
     have K_LT_SIZE : (k < size (task_arrivals_up_to_job_arrival arr_seq j)) by
-        apply ltn_leq_trans with (n := job_index arr_seq j) => //; first by apply index_size.
+        apply leq_trans with (n := job_index arr_seq j) => //; first by apply index_size.
     have JK_IN : (jk \in task_arrivals_up_to_job_arrival arr_seq j) by rewrite /jk; apply mem_nth => //. 
     rewrite mem_filter in JK_IN; move : JK_IN => /andP [/eqP TSK JK_IN].
     apply mem_bigcat_nat_exists in JK_IN; move : JK_IN => [i [JK_IN I_INEQ]]. 

analysis/facts/transform/edf_opt.v

@@ -503,7 +503,7 @@ Section MakeEDFAtFacts.
       by rewrite scheduled_at_def; apply /eqP.
     have LT_t_fsc:  t < find_swap_candidate sched t_edf j_orig.
     {
-      apply ltn_leq_trans with (n := t_edf) => //.
+      apply leq_trans with (n := t_edf) => //.
       apply fsc_range1 => //.
       now apply scheduled_job_in_sched_has_later_deadline.
     }
@@ -693,14 +693,14 @@ Section EDFPrefixInclusion.
       identical_prefix (edf_transform_prefix sched h1) (edf_transform_prefix sched h2) h1.
   Proof.
     move=> h1 h2 LE_h1_h2. rewrite /identical_prefix => t LT_t_h1.
-    induction h2; first by move: (ltn_leq_trans LT_t_h1 LE_h1_h2).
+    induction h2; first by move: (leq_trans LT_t_h1 LE_h1_h2).
     move: LE_h1_h2. rewrite leq_eqVlt => /orP [/eqP ->|LT]; first by done.
     move: LT. rewrite ltnS => LE_h1_h2.
     rewrite [RHS]/edf_transform_prefix /prefix_map -/prefix_map IHh2 //.
     rewrite {1}/make_edf_at.
     destruct (prefix_map sched make_edf_at h2 h2) as [j|] eqn:SCHED; last by done.
     rewrite -(swap_before_invariant _  h2 (find_swap_candidate (edf_transform_prefix sched h2) h2 j)) // ;
-      last by apply ltn_leq_trans with (n := h1).
+      last by apply leq_trans with (n := h1).
     have SCHED_j: scheduled_at (edf_transform_prefix sched h2) j h2
       by rewrite scheduled_at_def /edf_transform_prefix; apply /eqP.
     apply fsc_range1 => //.

analysis/facts/transform/swaps.v

@@ -201,7 +201,7 @@ Section SwappedFacts.
       sched t = sched' t.
   Proof.
     move=> t t_lt_t1.
-    move: (ltn_leq_trans t_lt_t1 H_well_ordered) => t_lt_t2.
+    move: (leq_trans t_lt_t1 H_well_ordered) => t_lt_t2.
     by apply swap_other_times_invariant => /eqP /eqP EQ; subst;
        [move: t_lt_t1|move: t_lt_t2]; rewrite ltnn.
   Qed.
@@ -450,7 +450,7 @@ Section EDFSwap.
       move: (H_not_EDF j j2 AT_t1 AT_t2) => DL2_le_DL1.
       rewrite -service_invariant_implies_deadline_met; first by exact H_deadline_met.
       apply service_after_swap_invariant => //.
-      apply ltn_leq_trans with (n := job_deadline j2) => //.
+      apply leq_trans with (n := job_deadline j2) => //.
     Qed.
 
   End NoNewDeadlineMissesCases.

analysis/facts/transform/wc_correctness.v

@@ -466,14 +466,14 @@ Section AuxiliaryLemmasWorkConservingTransformation.
       Proof.
         move=> t before_horizon.
         rewrite /sched1 /sched2.
-        induction h2; first by move: (ltn_leq_trans before_horizon H_horizon_order).
+        induction h2; first by move: (leq_trans before_horizon H_horizon_order).
         move: H_horizon_order. rewrite leq_eqVlt => /orP [/eqP ->|LT]; first by done.
         move: LT. rewrite ltnS => H_horizon_order_lt.
         rewrite [RHS]/wc_transform_prefix /prefix_map -/prefix_map IHi //.
         rewrite {1}/make_wc_at.
         destruct (prefix_map sched (make_wc_at arr_seq) i i) as [j|] eqn:SCHED; first by done.   
         rewrite -(swap_before_invariant _ i (find_swap_candidate arr_seq (wc_transform_prefix arr_seq sched i) i));
-          last by apply ltn_leq_trans with (n := h1).
+          last by apply leq_trans with (n := h1).
         rewrite //.
         apply swap_candidate_is_in_future.
       Qed.

util/nat.v

@@ -133,6 +133,7 @@ Section NatOrderLemmas.
      Nonetheless we introduce it here because an additional (even though
      arguably redundant) lemma doesn't hurt, and for newcomers the apparent
      absence of the mirror case of [leq_ltn_trans] can be somewhat confusing.  *)
+  #[deprecated(since="0.4",note="Use leq_trans instead since n < m is just a notation for n.+1 <= m (c.f., comment in util/nat.v).")]
   Lemma ltn_leq_trans n m p : m < n -> n <= p -> m < p.
   Proof. exact (@leq_trans n m.+1 p). Qed.