diff --git a/analysis/abstract/ideal_jlfp_rta.v b/analysis/abstract/ideal_jlfp_rta.v
index ddfadd5c845fc0758bbe78c654d457ec36c3376f..839ad64b9781e9e7403bed6f9d02af5a8a1b170e 100644
--- a/analysis/abstract/ideal_jlfp_rta.v
+++ b/analysis/abstract/ideal_jlfp_rta.v
@@ -514,7 +514,7 @@ Section JLFPInstantiation.
             rewrite eqn_add2r; unfold hep_job.
             erewrite H_priority_is_reflexive; eauto 2.
             rewrite eqn_leq; apply/andP; split; try eauto 2.
-              by apply service_at_most_cost; eauto with basic_facts.
+              by apply service_at_most_cost; rt_eauto.
         Qed.
  
         (** The equivalence trivially follows from the lemmas above. *)
diff --git a/analysis/facts/behavior/arrivals.v b/analysis/facts/behavior/arrivals.v
index 05335ff2b4c38665df66dd9eb23bff17dfc19bc5..27461995c45892f1e41ce6a03643640780bb5a56 100644
--- a/analysis/facts/behavior/arrivals.v
+++ b/analysis/facts/behavior/arrivals.v
@@ -81,13 +81,6 @@ Section Arrived.
 
 End Arrived.
 
-(** We add some of the above lemmas to the "Hint Database"
-    [basic_facts], so the [auto] tactic will be able to use them. *)
-Global Hint Resolve
-       valid_schedule_implies_jobs_must_arrive_to_execute
-       jobs_must_arrive_to_be_ready
-  : basic_facts.
-
 (** In this section, we establish useful facts about arrival sequence prefixes. *)
 Section ArrivalSequencePrefix.
 
@@ -295,3 +288,75 @@ Section ArrivalSequencePrefix.
   End ArrivalTimes.
 
 End ArrivalSequencePrefix.
+
+(** In this section, we establish a few auxiliary facts about the
+    relation between the property of being scheduled and arrival
+    predicates to facilitate automation. *)
+Section ScheduledImpliesArrives.
+
+  (** Consider any type of jobs. *) 
+  Context {Job : JobType}.
+  Context `{JobArrival Job}.
+
+  (** Consider any kind of processor state model, ... *)
+  Context {PState : ProcessorState Job}.
+
+  (** ... any job arrival sequence with consistent arrivals, .... *)
+  Variable arr_seq : arrival_sequence Job.
+  Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
+
+  (** ... and any schedule of this arrival sequence ... *)
+  Variable sched : schedule PState.
+  Hypothesis H_jobs_come_from_arrival_sequence : jobs_come_from_arrival_sequence sched arr_seq.
+
+  (** ... where jobs do not execute before their arrival. *)
+  Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
+
+
+  (** Next, consider a job [j] ... *)
+  Variable j : Job.
+  
+  (** ... which is scheduled at a time instant [t]. *)
+  Variable t : instant.
+  Hypothesis H_scheduled_at : scheduled_at sched j t.
+  
+  (** Then we show that [j] arrives in [arr_seq]. *) 
+  Lemma arrives_in_jobs_come_from_arrival_sequence :
+    arrives_in arr_seq j.
+  Proof.
+    by apply: H_jobs_come_from_arrival_sequence H_scheduled_at.
+  Qed.
+  
+  (** Job [j] has arrived by time instant [t]. *) 
+  Lemma arrived_between_jobs_must_arrive_to_execute :
+    has_arrived j t.
+  Proof.
+    by apply: H_jobs_must_arrive_to_execute H_scheduled_at.
+  Qed.
+
+  (** Finally, for any future time [t'], job [j] arrives before [t']. *) 
+  Lemma arrivals_before_scheduled_at :
+    forall t',
+      t < t' ->
+      j \in arrivals_before arr_seq t'.
+  Proof.
+    move=> t' LTtt'.
+    apply: arrived_between_implies_in_arrivals => //.
+    - by apply: arrives_in_jobs_come_from_arrival_sequence. 
+    - apply: leq_ltn_trans LTtt'.
+      by apply: arrived_between_jobs_must_arrive_to_execute.
+  Qed.
+
+End ScheduledImpliesArrives.
+
+(** We add some of the above lemmas to the "Hint Database"
+    [basic_rt_facts], so the [auto] tactic will be able to use them. *)
+Global Hint Resolve
+ arrivals_before_scheduled_at
+ arrivals_uniq
+ arrived_between_implies_in_arrivals 
+ arrived_between_jobs_must_arrive_to_execute
+ arrives_in_jobs_come_from_arrival_sequence
+ jobs_must_arrive_to_be_ready
+ valid_schedule_implies_jobs_must_arrive_to_execute
+  : basic_rt_facts.
diff --git a/analysis/facts/behavior/completion.v b/analysis/facts/behavior/completion.v
index 29ff9170af990be57e50a9c2c32eced060230b0f..3caae12cf0100b0ccdce6c869700ab6fc19c10e2 100644
--- a/analysis/facts/behavior/completion.v
+++ b/analysis/facts/behavior/completion.v
@@ -359,9 +359,9 @@ Section CompletedJobs.
 
 End CompletedJobs.
 
-(** We add the above lemma into a "Hint Database" basic_facts, so Coq
+(** We add the above lemma into a "Hint Database" basic_rt_facts, so Coq
     will be able to apply it automatically. *)
-Global Hint Resolve valid_schedule_implies_completed_jobs_dont_execute : basic_facts.
+Global Hint Resolve valid_schedule_implies_completed_jobs_dont_execute : basic_rt_facts.
 
 (** Next, we relate the completion of jobs in schedules with identical prefixes. *)
 Section CompletionInTwoSchedules.
diff --git a/analysis/facts/busy_interval/busy_interval.v b/analysis/facts/busy_interval/busy_interval.v
index 7cf5cd230d77d29631f92077c3351314c5ec9423..5f910fa80e83d46247f8785030ae44dc11e53427 100644
--- a/analysis/facts/busy_interval/busy_interval.v
+++ b/analysis/facts/busy_interval/busy_interval.v
@@ -46,7 +46,6 @@ Section ExistsBusyIntervalJLFP.
   (** For simplicity, let's define some local names. *)
   Let job_pending_at := pending sched.
   Let job_completed_by := completed_by sched.
-  Let arrivals_between := arrivals_between arr_seq.
   
   (** Consider an arbitrary task [tsk]. *)
   Variable tsk : Task.
@@ -107,7 +106,7 @@ Section ExistsBusyIntervalJLFP.
     Proof.
       rename H_quiet into QUIET, H_not_quiet into NOTQUIET.
       destruct (has (fun j_hp => (~~ job_completed_by j_hp t2) && hep_job j_hp j)
-                    (arrivals_between t1 t2)) eqn:COMP.
+                    (arrivals_between arr_seq t1 t2)) eqn:COMP.
       { move: COMP => /hasP [j_hp ARR /andP [NOTCOMP HP]].
         move: (ARR) => INarr.
         apply in_arrivals_implies_arrived_between in ARR; last by done.
@@ -189,7 +188,7 @@ Section ExistsBusyIntervalJLFP.
       - by exfalso; move_neq_down CONTR; eapply leq_ltn_trans; eauto 2.
       - have EX: exists hp__seq: seq Job,
         forall j__hp, j__hp \in hp__seq <-> arrives_in arr_seq j__hp /\ job_pending_at j__hp t /\ hep_job j__hp j.
-        { exists (filter (fun jo => (job_pending_at jo t) && (hep_job jo j)) (arrivals_between 0 t.+1)).
+        { exists (filter (fun jo => (job_pending_at jo t) && (hep_job jo j)) (arrivals_between arr_seq 0 t.+1)).
           intros; split; intros T.
           - move: T; rewrite mem_filter; move => /andP [/andP [PEN HP] IN].
             repeat split; eauto using in_arrivals_implies_arrived.
@@ -260,7 +259,7 @@ Section ExistsBusyIntervalJLFP.
         time interval <<[t1, t1 + Δ)>>. *)
     Let service_received_by_hep_jobs_released_during t_beg t_end :=
       service_of_higher_or_equal_priority_jobs
-        sched (arrivals_between t_beg t_end) j t1 (t1 + Δ).
+        sched (arrivals_between arr_seq t_beg t_end) j t1 (t1 + Δ).
 
     (** We prove that jobs with higher-than-or-equal priority that
         released before time instant [t1] receive no service after time
@@ -271,12 +270,11 @@ Section ExistsBusyIntervalJLFP.
     Proof.
       intros.
       rewrite /service_received_by_hep_jobs_released_during
-              /service_of_higher_or_equal_priority_jobs
-              /service_of_jobs /arrivals_between.
+              /service_of_higher_or_equal_priority_jobs /service_of_jobs.
       rewrite [in X in _ = X](arrivals_between_cat _ _ t1);
         [ | | rewrite leq_addr]; try done.
       rewrite big_cat //=.
-      rewrite -{1}[\sum_(j <- arrivals_between _ (t1 + Δ) | _)
+      rewrite -{1}[\sum_(j <- arrivals_between arr_seq _ (t1 + Δ) | _)
                     service_during sched j t1 (t1 + Δ)]add0n.
       apply/eqP. rewrite eqn_add2r eq_sym exchange_big //=.
       rewrite big1_seq //.
@@ -295,14 +293,14 @@ Section ExistsBusyIntervalJLFP.
     (** Next we prove that the total service within a "non-quiet" 
         time interval <<[t1, t1 + Δ)>> is exactly [Δ]. *)
     Lemma no_idle_time_within_non_quiet_time_interval:
-      service_of_jobs sched predT (arrivals_between 0 (t1 + Δ)) t1 (t1 + Δ) = Δ.
+      service_of_jobs sched predT (arrivals_between arr_seq 0 (t1 + Δ)) t1 (t1 + Δ) = Δ.
     Proof.
       intros; unfold service_of_jobs, service_of_higher_or_equal_priority_jobs. 
       rewrite -{3}[Δ](sum_of_ones t1) exchange_big //=.
       apply/eqP; rewrite eqn_leq; apply/andP; split.
       { rewrite leq_sum // => t' _.
-        have SCH := @service_of_jobs_le_1 _ _ _ _ sched predT (arrivals_between 0 (t1 + Δ)).        
-        by eapply leq_trans; last apply SCH; eauto using arrivals_uniq with basic_facts. }
+        have SCH := @service_of_jobs_le_1 _ _ _ _ sched predT (arrivals_between arr_seq 0 (t1 + Δ)).        
+        by eapply leq_trans; last apply SCH; rt_eauto. }
       { rewrite [in X in X <= _]big_nat_cond [in X in _ <= X]big_nat_cond //=
                 leq_sum // => t' /andP [/andP [LT GT] _]; apply/sum_seq_gt0P.
         ideal_proc_model_sched_case_analysis_eq sched t' jo.
@@ -355,14 +353,14 @@ Section ExistsBusyIntervalJLFP.
         a given interval <<[t1, t2)>> that have higher-or-equal
         priority w.r.t. the job [j] being analyzed. *)
     Let hp_workload t1 t2 :=
-      workload_of_higher_or_equal_priority_jobs j (arrivals_between t1 t2).
+      workload_of_higher_or_equal_priority_jobs j (arrivals_between arr_seq t1 t2).
 
     (** With regard to the jobs with higher-or-equal priority that are released
            in a given interval <<[t1, t2)>>, we also recall the service received by these
            jobs in the same interval <<[t1, t2)>>. *)
     Let hp_service t1 t2 :=
       service_of_higher_or_equal_priority_jobs
-        sched (arrivals_between t1 t2) j t1 t2.
+        sched (arrivals_between arr_seq t1 t2) j t1 t2.
 
     (** Now we begin the proof. First, we show that the busy interval is bounded. *)
     Section BoundingBusyInterval.
@@ -483,7 +481,7 @@ Section ExistsBusyIntervalJLFP.
                 { rewrite leqn0 big1_seq // /service_at => i Hi.
                   by rewrite service_in_def SCHED. }
                 { case PRIO1: (hep_job j1 j) => /=; first last.
-                  - apply service_of_jobs_le_1; auto with basic_facts.
+                  - apply service_of_jobs_le_1; rt_auto.
                     by apply arrivals_uniq.
                   - rewrite leqn0 big1_seq; first by done.
                     move => j2 /andP [PRIO2 ARRj2].
@@ -515,11 +513,11 @@ Section ExistsBusyIntervalJLFP.
             have PEND := not_quiet_implies_exists_pending_job.
             rename H_no_quiet_time into NOTQUIET, 
             H_is_busy_prefix into PREFIX.
-            set l := arrivals_between t1 (t1 + delta).
+            set l := arrivals_between arr_seq t1 (t1 + delta).
             set hep := hep_job.
             unfold hp_service, service_of_higher_or_equal_priority_jobs, service_of_jobs,
             hp_workload, workload_of_higher_or_equal_priority_jobs, workload_of_jobs.
-            fold arrivals_between l hep.
+            fold l hep.
             move: (PREFIX) => [_ [QUIET _]].
             move: (NOTQUIET) => NOTQUIET'.
             feed (NOTQUIET' (t1 + delta)).
diff --git a/analysis/facts/busy_interval/carry_in.v b/analysis/facts/busy_interval/carry_in.v
index 2601666fde846e64585ed75b1d0ffb6ad135636f..708962c38c20654e8e77309eb19dc33d2e5891f1 100644
--- a/analysis/facts/busy_interval/carry_in.v
+++ b/analysis/facts/busy_interval/carry_in.v
@@ -171,7 +171,7 @@ Section ExistsNoCarryIn.
       Proof.
         unfold total_service. 
         rewrite -{3}[Δ]addn0 -{2}(subnn t) addnBA // [in X in _ <= X]addnC.
-        apply service_of_jobs_le_length_of_interval'; auto with basic_facts.
+        apply service_of_jobs_le_length_of_interval'; rt_auto.
         by eapply arrivals_uniq; eauto 2.
       Qed.
 
@@ -228,7 +228,7 @@ Section ExistsNoCarryIn.
                           H_jobs_must_arrive_to_execute
                           H_completed_jobs_dont_execute
                           predT 0 t t.
-          feed_n 2 COMPL; auto with basic_facts.
+          feed_n 2 COMPL; rt_auto.
           { intros j A B; apply H_no_carry_in.
             - eapply in_arrivals_implies_arrived; eauto 2.
             - eapply in_arrivals_implies_arrived_between in A; eauto 2.
@@ -247,8 +247,7 @@ Section ExistsNoCarryIn.
           by apply H_workload_is_bounded.
         }  
         intros s ARR BEF.
-        eapply workload_eq_service_impl_all_jobs_have_completed; eauto with basic_facts.
-        by eapply arrived_between_implies_in_arrivals.
+        by eapply workload_eq_service_impl_all_jobs_have_completed; rt_eauto.
       Qed.
 
     End ProcessorIsNotTooBusyInduction.
diff --git a/analysis/facts/busy_interval/priority_inversion.v b/analysis/facts/busy_interval/priority_inversion.v
index d1a8964e4ab2ec14a6da7d0b3ff40a25f9b8e6f7..88c90824a4fdacd103ca0e26265f44d2bd1fde55 100644
--- a/analysis/facts/busy_interval/priority_inversion.v
+++ b/analysis/facts/busy_interval/priority_inversion.v
@@ -125,7 +125,7 @@ Section PriorityInversionIsBounded.
         ~ is_idle sched t.
       Proof.
         intros IDLE.
-        by exfalso; apply: not_quiet_implies_not_idle; eauto 2 with basic_facts.
+        by exfalso; apply: not_quiet_implies_not_idle; rt_eauto.
       Qed.
       
       (** Next we consider two cases: (1) when [t] is less than [t2 - 1] and (2) [t] is equal to [t2 - 1]. *)
@@ -202,7 +202,7 @@ Section PriorityInversionIsBounded.
             now rewrite -pred_Sn.
           }
           have PEND: pending sched j t2.-1
-            by rewrite -ARR; apply job_pending_at_arrival => //; eauto with basic_facts.
+            by rewrite -ARR; apply job_pending_at_arrival => //; rt_eauto.
           apply H_job_ready in PEND => //; destruct PEND as [jhp [ARRhp [PENDhp HEPhp]]].
           eapply NOTHP, (H_priority_is_transitive 0); last by apply HEPhp.
           apply (H_respects_policy _ _ t2.-1); auto.
@@ -259,13 +259,13 @@ Section PriorityInversionIsBounded.
         move: (H_t_in_busy_interval) => /andP [GEt LEt].
         have HP := scheduled_at_preemption_time_implies_higher_or_equal_priority _ Sched_jhp.
         move: (Sched_jhp) => PENDING.
-        eapply scheduled_implies_pending in PENDING; eauto 2 with basic_facts.
+        eapply scheduled_implies_pending in PENDING; rt_eauto.
         apply/andP; split; last by apply leq_ltn_trans with (n := t); first by move: PENDING => /andP [ARR _]. 
         apply contraT; rewrite -ltnNge; intro LT; exfalso.
         feed (QUIET jhp); first by eapply CONS, Sched_jhp.
         specialize (QUIET HP LT).
         have COMP: job_completed_by jhp t by apply: completion_monotonic QUIET.
-        apply completed_implies_not_scheduled in COMP; eauto with basic_facts.
+        apply completed_implies_not_scheduled in COMP; rt_eauto.
         by move: COMP => /negP COMP; apply COMP.
       Qed.
       
@@ -331,14 +331,14 @@ Section PriorityInversionIsBounded.
       } 
       repeat split; try done. 
       move: (H_busy_interval_prefix) => [SL [QUIET [NOTQUIET EXj]]]; move: (Sched_jhp) => PENDING.
-      eapply scheduled_implies_pending in PENDING; eauto with basic_facts.
+      eapply scheduled_implies_pending in PENDING; rt_eauto.
       apply/andP; split; last by apply leq_ltn_trans with (n := t); first by move: PENDING => /andP [ARR _].
       apply contraT; rewrite -ltnNge; intro LT; exfalso.
       feed (QUIET jhp); first by eapply H_jobs_come_from_arrival_sequence, Sched_jhp.
       specialize (QUIET HP LT).
       have COMP: job_completed_by jhp t.
       { apply: completion_monotonic QUIET; exact: leq_trans LEtp. }
-      apply completed_implies_not_scheduled in COMP; eauto with basic_facts.
+      apply completed_implies_not_scheduled in COMP; rt_eauto.
       by move : COMP => /negP COMP; apply : COMP.
     Qed. 
     
@@ -388,10 +388,10 @@ Section PriorityInversionIsBounded.
       apply/negP; intros SCHED2.
       specialize (QT jhp).
       feed_n 3 QT; eauto.
-      - have MATE: jobs_must_arrive_to_execute sched by eauto with basic_facts.
+      - have MATE: jobs_must_arrive_to_execute sched by rt_eauto.
         have HA: has_arrived jhp t by apply MATE.
         by done.
-      apply completed_implies_not_scheduled in QT; eauto with basic_facts.
+      apply completed_implies_not_scheduled in QT; rt_eauto.
       by move: QT => /negP NSCHED; apply: NSCHED.
     Qed.
 
@@ -677,7 +677,7 @@ Section PriorityInversionIsBounded.
             specialize (EXPP (service jlp t1)).
             feed EXPP.
             { apply/andP; split; first by done.
-              apply service_at_most_cost; eauto with basic_facts.
+              apply service_at_most_cost; rt_eauto.
             }
             move: EXPP => [pt [NEQ PP]].
             exists pt; apply/andP; split; by done.
diff --git a/analysis/facts/model/ideal_schedule.v b/analysis/facts/model/ideal_schedule.v
index f3ce907d2db1aa00b81ba868c15d4b507cf0bae2..230402d36297f7db75238e258a4903aca1815c2e 100644
--- a/analysis/facts/model/ideal_schedule.v
+++ b/analysis/facts/model/ideal_schedule.v
@@ -247,11 +247,11 @@ Section IncrementalService.
 End IncrementalService.
 
 (** * Automation *)
-(** We add the above lemmas into a "Hint Database" basic_facts, so Coq
+(** We add the above lemmas into a "Hint Database" basic_rt_facts, so Coq
     will be able to apply them automatically. *)
 Global Hint Resolve ideal_proc_model_is_a_uniprocessor_model
      ideal_proc_model_ensures_ideal_progress
-     ideal_proc_model_provides_unit_service : basic_facts.
+     ideal_proc_model_provides_unit_service : basic_rt_facts.
 
 (** We also provide tactics for case analysis on ideal processor state. *)
 
diff --git a/analysis/facts/model/preemption.v b/analysis/facts/model/preemption.v
index f38a46af59f50a86f95102acc4f746f292c1b8d6..1ccd9e2561a17e055557b42982a38319f6139319 100644
--- a/analysis/facts/model/preemption.v
+++ b/analysis/facts/model/preemption.v
@@ -96,7 +96,7 @@ Section PreemptionFacts.
       apply/allP; intros t'.
       by rewrite mem_index_iota ltnS -eqn_leq; move => /eqP <-.  
     }
-    have MATE : jobs_must_arrive_to_execute sched by eauto with basic_facts. 
+    have MATE : jobs_must_arrive_to_execute sched by rt_eauto. 
     move :  (H_sched_valid) =>  [COME_ARR READY].
     have MIN := ex_minnP EX. 
     move: MIN => [mpt /andP [/andP [LT1 SCHEDsmpt] /allP ALL] MIN]; clear EX.
diff --git a/analysis/facts/model/rbf.v b/analysis/facts/model/rbf.v
index 31df27fef863916755d82c869bf0c4655a6246e7..3508f44bd681b83640585649ff7b19ded30cea6f 100644
--- a/analysis/facts/model/rbf.v
+++ b/analysis/facts/model/rbf.v
@@ -319,7 +319,7 @@ Section RequestBoundFunctions.
   Proof.
     move => t GE.
     destruct t; first by done.
-    eapply leq_trans; first by apply task_rbf_1_ge_task_cost; eauto with basic_facts.
+    eapply leq_trans; first by apply task_rbf_1_ge_task_cost; rt_eauto.
     rewrite /total_request_bound_function.
     erewrite big_rem; last by exact H_tsk_in_ts.
     apply leq_trans with (task_request_bound_function tsk t.+1); last by apply leq_addr.
diff --git a/analysis/facts/periodic/arrival_separation.v b/analysis/facts/periodic/arrival_separation.v
index 46af75dbfe4b35415f53043de5e535662a5629c3..89ed08c0e9aadc15a0ea93840996f019440d6a7c 100644
--- a/analysis/facts/periodic/arrival_separation.v
+++ b/analysis/facts/periodic/arrival_separation.v
@@ -103,7 +103,7 @@ Section JobArrivalSeparation.
           move : BEFORE => [nj [NEQNJ [TSKNJ [ARRNJ INDNJ]]]]; rewrite TSKj2 in TSKNJ.
           specialize (IHs nj j2); feed_n 6 IHs => //; first by lia.          
           { by apply (lower_index_implies_earlier_arrival _ H_consistent_arrivals tsk);
-              eauto with basic_facts; lia.
+              rt_eauto; lia.
           }
           move : IHs => [n [NZN ARRJ'NJ]].          
           move: (H_periodic_model nj) => PERIODIC; feed_n 3 PERIODIC => //; first by lia. 
@@ -143,13 +143,13 @@ Section JobArrivalSeparation.
     apply job_arrival_separation_when_index_diff_is_k with (k := (job_index arr_seq j2 - job_index arr_seq j1)); try done.
     - apply subnKC.
       move_neq_up IND.
-      eapply lower_index_implies_earlier_arrival in IND; eauto with basic_facts.
+      eapply lower_index_implies_earlier_arrival in IND; rt_eauto.
       now move_neq_down IND.      
     - case: (boolP (job_index arr_seq j1 == job_index arr_seq j2)) => [/eqP EQ_IND|NEQ_IND].
       + now apply equal_index_implies_equal_jobs in EQ_IND => //; rewrite H_j1_of_task.
       + move: NEQ_IND; rewrite neq_ltn => /orP [LT|LT].
-        * now eapply (lower_index_implies_earlier_arrival) in LT; eauto with basic_facts.
-        * eapply (lower_index_implies_earlier_arrival) in LT; eauto with basic_facts.
+        * now eapply (lower_index_implies_earlier_arrival) in LT; rt_eauto.
+        * eapply (lower_index_implies_earlier_arrival) in LT; rt_eauto.
           now move_neq_down LT.
   Qed.  
   
diff --git a/analysis/facts/periodic/sporadic.v b/analysis/facts/periodic/sporadic.v
index 2a4f509e17d60390ac3869b6de712bfc1b648ddc..3fb575218ce7ebe5a5c0de8239088b6a7059e6e3 100644
--- a/analysis/facts/periodic/sporadic.v
+++ b/analysis/facts/periodic/sporadic.v
@@ -87,6 +87,6 @@ Section PeriodicTasksAsSporadicTasks.
   
 End PeriodicTasksAsSporadicTasks.
 
-(** We add the [periodic_task_respects_sporadic_task_model] lemma into a "Hint Database" basic_facts,
+(** We add the [periodic_task_respects_sporadic_task_model] lemma into a "Hint Database" basic_rt_facts,
     so Coq will be able to apply it automatically. *)
-Global Hint Extern 1 => apply periodic_task_respects_sporadic_task_model : basic_facts.
+Global Hint Extern 1 => apply periodic_task_respects_sporadic_task_model : basic_rt_facts.
diff --git a/analysis/facts/periodic/task_arrivals_size.v b/analysis/facts/periodic/task_arrivals_size.v
index 8d3b831fe49ffa503a18926061d278dca5cc075b..587383df7a0d54ebed0f67e4fd0121b47eceb606 100644
--- a/analysis/facts/periodic/task_arrivals_size.v
+++ b/analysis/facts/periodic/task_arrivals_size.v
@@ -67,7 +67,7 @@ Section TaskArrivalsSize.
     move: A_IN B_IN => /andP [/eqP TSKA ARRA] /andP [/eqP TSKB ARRB].
     move: (ARRA); move: (ARRB); rewrite /arrivals_at => A_IN B_IN.
     apply in_arrseq_implies_arrives in A_IN; apply in_arrseq_implies_arrives in B_IN.
-    have SPO : respects_sporadic_task_model arr_seq tsk; try by auto with basic_facts.
+    have SPO : respects_sporadic_task_model arr_seq tsk; try by rt_auto.
     have EQ_ARR_A : (job_arrival a = t) by apply H_consistent_arrivals.
     have EQ_ARR_B : (job_arrival b = t) by apply H_consistent_arrivals.
     specialize (SPO a b); feed_n 6 SPO => //; try by lia.
@@ -129,7 +129,7 @@ Section TaskArrivalsSize.
       move : (jobs_exists_later n) => [j' [ARR [TSK [ARRIVAL IND]]]].
       apply (only_j_in_task_arrivals_at_j
                arr_seq H_consistent_arrivals H_uniq_arr_seq tsk) in ARR => //;
-        last by auto with basic_facts.
+        last by rt_auto.
       rewrite /task_arrivals_at_job_arrival TSK in ARR.
       now rewrite -ARRIVAL ARR.
     Qed.
diff --git a/analysis/facts/preemption/job/limited.v b/analysis/facts/preemption/job/limited.v
index 6db85b5040d732fdf7663af9e59f156e671f98a7..d992e4620bfc48198bee8dfaa78c57d72d6d914e 100644
--- a/analysis/facts/preemption/job/limited.v
+++ b/analysis/facts/preemption/job/limited.v
@@ -225,4 +225,4 @@ Section ModelWithLimitedPreemptions.
   Qed.
   
 End ModelWithLimitedPreemptions.
-Global Hint Resolve valid_fixed_preemption_points_model_lemma : basic_facts.
+Global Hint Resolve valid_fixed_preemption_points_model_lemma : basic_rt_facts.
diff --git a/analysis/facts/preemption/job/nonpreemptive.v b/analysis/facts/preemption/job/nonpreemptive.v
index adb04aae5aa2a486d77a0b59b1f5fa59796c20c6..b59ee9eb0c573c09f774ecb1e338d4b6fd9a5a14 100644
--- a/analysis/facts/preemption/job/nonpreemptive.v
+++ b/analysis/facts/preemption/job/nonpreemptive.v
@@ -49,7 +49,7 @@ Section FullyNonPreemptiveModel.
       + rewrite /completed_by -ltnNge.
         move: NCOMPL; rewrite neq_ltn; move => /orP [LE|GE]; [by done | exfalso].
         move: GE; rewrite ltnNge; move => /negP GE; apply: GE.
-        apply completion.service_at_most_cost; eauto 2 with basic_facts.
+        apply completion.service_at_most_cost; rt_eauto.
     - intros t NSCHED SCHED.
       rewrite /job_preemptable /fully_nonpreemptive_model.
       apply/orP; left. 
@@ -66,7 +66,7 @@ Section FullyNonPreemptiveModel.
           have <-: (service_at sched j t.+1) = 1.
           { by apply/eqP; rewrite service_at_def eqb1 -scheduled_at_def. }
             by rewrite -big_nat_recr //=.
-            by apply completion.service_at_most_cost; eauto 2 with basic_facts.
+            by apply completion.service_at_most_cost; rt_eauto.
   Qed.
 
   (** We also prove that under the fully non-preemptive model
@@ -127,7 +127,7 @@ Section FullyNonPreemptiveModel.
   Qed.
   
 End FullyNonPreemptiveModel.
-Global Hint Resolve valid_fully_nonpreemptive_model : basic_facts.
+Global Hint Resolve valid_fully_nonpreemptive_model : basic_rt_facts.
 
 (** In this section, we prove the equivalence between no preemptions and a non-preemptive schedule. *)
 Section NoPreemptionsEquivalence.
diff --git a/analysis/facts/preemption/job/preemptive.v b/analysis/facts/preemption/job/preemptive.v
index bb8fc1366d272fccef3b9420575238c1b727e9e1..9df41b73044a5b05b1d6bf208ffd80a5303d2113 100644
--- a/analysis/facts/preemption/job/preemptive.v
+++ b/analysis/facts/preemption/job/preemptive.v
@@ -64,4 +64,4 @@ Section FullyPreemptiveModel.
   Qed.    
   
 End FullyPreemptiveModel.
-Global Hint Resolve valid_fully_preemptive_model : basic_facts.
+Global Hint Resolve valid_fully_preemptive_model : basic_rt_facts.
diff --git a/analysis/facts/preemption/rtc_threshold/floating.v b/analysis/facts/preemption/rtc_threshold/floating.v
index cbfe9ce95407ec77afce4e81471058d66c70ed2a..5cb88383616dc618689f95d39fd427d663b6a2a9 100644
--- a/analysis/facts/preemption/rtc_threshold/floating.v
+++ b/analysis/facts/preemption/rtc_threshold/floating.v
@@ -35,9 +35,9 @@ Section TaskRTCThresholdFloatingNonPreemptiveRegions.
     intros; split.
     - by rewrite /task_rtc_bounded_by_cost.
     - intros j ARR TSK.
-      apply leq_trans with (job_cost j); eauto 2 with basic_facts.
+      apply leq_trans with (job_cost j); rt_eauto.
       by move: TSK => /eqP <-; apply H_valid_job_cost.
   Qed.
   
 End TaskRTCThresholdFloatingNonPreemptiveRegions.
-Global Hint Resolve floating_preemptive_valid_task_run_to_completion_threshold : basic_facts.
+Global Hint Resolve floating_preemptive_valid_task_run_to_completion_threshold : basic_rt_facts.
diff --git a/analysis/facts/preemption/rtc_threshold/job_preemptable.v b/analysis/facts/preemption/rtc_threshold/job_preemptable.v
index 69778b68d180aa6cf4bb88d784ba2e9a7c17de46..451319b8af79ea8ce4667e1dbe02a6bb5f4a3bad 100644
--- a/analysis/facts/preemption/rtc_threshold/job_preemptable.v
+++ b/analysis/facts/preemption/rtc_threshold/job_preemptable.v
@@ -258,6 +258,6 @@ Section RunToCompletionThreshold.
 
 End RunToCompletionThreshold.
 
-(** We add the above lemmas into a "Hint Database" basic_facts, so Coq 
+(** We add the above lemmas into a "Hint Database" basic_rt_facts, so Coq 
     will be able to apply them automatically. *)   
-Global Hint Resolve job_run_to_completion_threshold_le_job_cost : basic_facts.
+Global Hint Resolve job_run_to_completion_threshold_le_job_cost : basic_rt_facts.
diff --git a/analysis/facts/preemption/rtc_threshold/limited.v b/analysis/facts/preemption/rtc_threshold/limited.v
index 4e560671a0316aed259af94e44c74da1cc6f8076..a202b2916ba5f2893dcaf11b565e8d7d91b40546 100644
--- a/analysis/facts/preemption/rtc_threshold/limited.v
+++ b/analysis/facts/preemption/rtc_threshold/limited.v
@@ -140,4 +140,4 @@ Section TaskRTCThresholdLimitedPreemptions.
   Qed.
   
 End TaskRTCThresholdLimitedPreemptions.
-Global Hint Resolve limited_valid_task_run_to_completion_threshold : basic_facts.
+Global Hint Resolve limited_valid_task_run_to_completion_threshold : basic_rt_facts.
diff --git a/analysis/facts/preemption/rtc_threshold/nonpreemptive.v b/analysis/facts/preemption/rtc_threshold/nonpreemptive.v
index 5fde74ce93efdc650bf83056517938244ec03de5..4fbcecd897fa3bdbe7d1279db8286022184bfedc 100644
--- a/analysis/facts/preemption/rtc_threshold/nonpreemptive.v
+++ b/analysis/facts/preemption/rtc_threshold/nonpreemptive.v
@@ -77,4 +77,4 @@ Section TaskRTCThresholdFullyNonPreemptive.
   Qed.
     
 End TaskRTCThresholdFullyNonPreemptive.
-Global Hint Resolve fully_nonpreemptive_valid_task_run_to_completion_threshold : basic_facts.
+Global Hint Resolve fully_nonpreemptive_valid_task_run_to_completion_threshold : basic_rt_facts.
diff --git a/analysis/facts/preemption/rtc_threshold/preemptive.v b/analysis/facts/preemption/rtc_threshold/preemptive.v
index 2a47fb546ab22d45d6021571fd1c679a085be932..f6495c33b7b962daa809b5128d499fb02503d540 100644
--- a/analysis/facts/preemption/rtc_threshold/preemptive.v
+++ b/analysis/facts/preemption/rtc_threshold/preemptive.v
@@ -33,9 +33,9 @@ Section TaskRTCThresholdFullyPreemptiveModel.
     intros; split.
     - by rewrite /task_rtc_bounded_by_cost.
     - intros j ARR TSK.
-      apply leq_trans with (job_cost j); eauto 2 with basic_facts.
+      apply leq_trans with (job_cost j); rt_eauto.
       by move: TSK => /eqP <-; apply H_valid_job_cost.
   Qed.
     
 End TaskRTCThresholdFullyPreemptiveModel.
-Global Hint Resolve fully_preemptive_valid_task_run_to_completion_threshold : basic_facts.
+Global Hint Resolve fully_preemptive_valid_task_run_to_completion_threshold : basic_rt_facts.
diff --git a/analysis/facts/preemption/task/floating.v b/analysis/facts/preemption/task/floating.v
index 92ced12af85969e10a7185952e6f8d192abcb7db..0171bff614ec3a3b3f5a9bd42cbcef86038ca9fd 100644
--- a/analysis/facts/preemption/task/floating.v
+++ b/analysis/facts/preemption/task/floating.v
@@ -106,8 +106,8 @@ Section FloatingNonPreemptiveRegionsModel.
 
 End FloatingNonPreemptiveRegionsModel.
 
-(** We add the above lemma into a "Hint Database" basic_facts, so Coq will be able to apply them automatically. *)
+(** We add the above lemma into a "Hint Database" basic_rt_facts, so Coq will be able to apply them automatically. *)
 Global Hint Resolve
      valid_fixed_preemption_points_model_lemma
      floating_preemption_points_model_is_model_with_bounded_nonpreemptive_regions
-     floating_preemption_points_model_is_valid_model_with_bounded_nonpreemptive_regions : basic_facts.
+     floating_preemption_points_model_is_valid_model_with_bounded_nonpreemptive_regions : basic_rt_facts.
diff --git a/analysis/facts/preemption/task/limited.v b/analysis/facts/preemption/task/limited.v
index 983c8c61bb27d32b496f684529f4f3862c33c121..80ba93c846e4d1080fe6a6a80ba989a0cf57db50 100644
--- a/analysis/facts/preemption/task/limited.v
+++ b/analysis/facts/preemption/task/limited.v
@@ -108,8 +108,8 @@ Section LimitedPreemptionsModel.
   
 End LimitedPreemptionsModel. 
 
-(** We add the above lemma into a "Hint Database" basic_facts, so Coq will be able to apply them automatically. *)
+(** We add the above lemma into a "Hint Database" basic_rt_facts, so Coq will be able to apply them automatically. *)
 Global Hint Resolve
      valid_fixed_preemption_points_model_lemma
      fixed_preemption_points_model_is_model_with_bounded_nonpreemptive_regions
-     fixed_preemption_points_model_is_valid_model_with_bounded_nonpreemptive_regions : basic_facts.
+     fixed_preemption_points_model_is_valid_model_with_bounded_nonpreemptive_regions : basic_rt_facts.
diff --git a/analysis/facts/preemption/task/nonpreemptive.v b/analysis/facts/preemption/task/nonpreemptive.v
index 2867566428f97b4f6a0151a4fa0343793882b738..bc3360d5026e594729b0afa7dc29ca0d5bee0ea1 100644
--- a/analysis/facts/preemption/task/nonpreemptive.v
+++ b/analysis/facts/preemption/task/nonpreemptive.v
@@ -85,8 +85,8 @@ Section FullyNonPreemptiveModel.
     
 End FullyNonPreemptiveModel.
 
-(** We add the above lemma into a "Hint Database" basic_facts, so Coq will be able to apply them automatically. *)
+(** We add the above lemma into a "Hint Database" basic_rt_facts, so Coq will be able to apply them automatically. *)
 Global Hint Resolve 
      valid_fully_nonpreemptive_model
      fully_nonpreemptive_model_is_model_with_bounded_nonpreemptive_regions
-     fully_nonpreemptive_model_is_valid_model_with_bounded_nonpreemptive_regions : basic_facts.
+     fully_nonpreemptive_model_is_valid_model_with_bounded_nonpreemptive_regions : basic_rt_facts.
diff --git a/analysis/facts/preemption/task/preemptive.v b/analysis/facts/preemption/task/preemptive.v
index 512b68311695e7cfc416802030ab756b1edacf53..f82e5bcd6fb56f1a2e0a9f470fb1ffa3fe41c5c2 100644
--- a/analysis/facts/preemption/task/preemptive.v
+++ b/analysis/facts/preemption/task/preemptive.v
@@ -57,8 +57,8 @@ Section FullyPreemptiveModel.
     
 End FullyPreemptiveModel.
 
-(** We add the above lemma into a "Hint Database" basic_facts, so Coq will be able to apply them automatically. *)
+(** We add the above lemma into a "Hint Database" basic_rt_facts, so Coq will be able to apply them automatically. *)
 Global Hint Resolve
      valid_fully_preemptive_model
      fully_preemptive_model_is_model_with_bounded_nonpreemptive_regions
-     fully_preemptive_model_is_valid_model_with_bounded_nonpreemptive_segments : basic_facts.
+     fully_preemptive_model_is_valid_model_with_bounded_nonpreemptive_segments : basic_rt_facts.
diff --git a/analysis/facts/priority/edf.v b/analysis/facts/priority/edf.v
index ed19b6a0af3b4db710a6e12090bc45267925ad93..a9d7d2ebb262dbd5a17acbad6471dd736b28a5cc 100644
--- a/analysis/facts/priority/edf.v
+++ b/analysis/facts/priority/edf.v
@@ -29,9 +29,9 @@ Section PropertiesOfEDF.
 
 End PropertiesOfEDF.
 
-(** We add the above lemma into a "Hint Database" basic_facts, so Coq
+(** We add the above lemma into a "Hint Database" basic_rt_facts, so Coq
     will be able to apply it automatically. *)
-Global Hint Resolve EDF_respects_sequential_tasks : basic_facts.
+Global Hint Resolve EDF_respects_sequential_tasks : basic_rt_facts.
 
 
 Require Export prosa.model.task.sequentiality.
@@ -98,7 +98,7 @@ Section SequentialEDF.
   Proof.
     intros ? ? ? ARR1 ARR2 SAME LT.
     eapply early_hep_job_is_scheduled => //; eauto 2.
-    - by auto with basic_facts.
+    - by rt_auto.
     - move : H_valid_model_with_bounded_nonpreemptive_segments => [VALID _]; apply VALID.
     - clear t; intros ?.
       move: SAME => /eqP SAME.
diff --git a/analysis/facts/priority/fifo.v b/analysis/facts/priority/fifo.v
index 3228d7e60937e1ffa6352f7b3407f4afa44bc09b..94941ff1d6f1c5c403b85862c6cdb10dd7e401ef 100644
--- a/analysis/facts/priority/fifo.v
+++ b/analysis/facts/priority/fifo.v
@@ -56,7 +56,7 @@ Section BasicLemmas.
     apply /negP; rewrite negb_and.
     apply /orP; right; apply /negPn.
     have -> : scheduled_at sched s t -> completed_by sched j t => //.
-    eapply (early_hep_job_is_scheduled); try eauto 2 with basic_facts.
+    eapply (early_hep_job_is_scheduled); try rt_eauto.
     - by move=> ?; apply /andP; split; [apply ltnW | rewrite -ltnNge //=].
   Qed.
 
@@ -74,7 +74,7 @@ Section BasicLemmas.
     move => j' t SCHED j_hp ARRjhp HEP.
     have EARLIER: job_arrival j_hp < job_arrival j' by rewrite -ltnNge in HEP.
     eapply (early_hep_job_is_scheduled arr_seq _ sched _ _ _ _ j_hp j' _ _ _ t).
-    Unshelve. all : eauto with basic_facts.
+    Unshelve. all : rt_eauto.
     move=> t'; apply /andP; split => //.
     by apply ltnW.
   Qed.
@@ -91,7 +91,7 @@ Section BasicLemmas.
     Lemma tasks_execute_sequentially : sequential_tasks arr_seq sched.
     Proof.
       move => j1 j2 t ARRj1 ARRj2 SAME_TASKx LT => //.
-      eapply (early_hep_job_is_scheduled); try eauto 2 with basic_facts.
+      eapply (early_hep_job_is_scheduled); try rt_eauto.
       by move=> ?; apply /andP; split; [apply ltnW | rewrite -ltnNge //=].
     Qed.
 
@@ -117,7 +117,7 @@ Section BasicLemmas.
     { specialize (H_work_conservation j t).
       destruct H_work_conservation as [j_other SCHEDj_other]; first by eapply (COME j t.-1 SCHED1).
       - do 2 (apply /andP; split; last by done).
-        eapply scheduled_implies_pending in SCHED1; try eauto with basic_facts.
+        eapply scheduled_implies_pending in SCHED1; try rt_eauto.
         move : SCHED1 => /andP [HAS COMPL].
         by apply leq_trans with t.-1; [exact HAS| lia].
       - move: SCHEDj_other IDLE.
@@ -130,8 +130,8 @@ Section BasicLemmas.
         by repeat (apply /andP ; split; try by done).
       }
       rewrite /hep_job /fifo.FIFO -ltnNge in HEP. 
-      eapply (early_hep_job_is_scheduled arr_seq ) in SCHED1; try eauto 2 with basic_facts.
-      - apply scheduled_implies_not_completed in INTER; eauto with basic_facts.
+      eapply (early_hep_job_is_scheduled arr_seq ) in SCHED1; try rt_eauto.
+      - apply scheduled_implies_not_completed in INTER; rt_eauto.
         by eapply (incompletion_monotonic sched s t.-1 t) in INTER; [move: INTER => /negP|lia].
       - by move=> ?; apply /andP; split; [apply ltnW | rewrite -ltnNge //=]. }
   Qed.
diff --git a/analysis/facts/readiness/basic.v b/analysis/facts/readiness/basic.v
index c3e0d39f5216c6a1a10bd4d4dffc2808cd418a10..6b6f43775e6b1be564f6df54dc08b49e640c176f 100644
--- a/analysis/facts/readiness/basic.v
+++ b/analysis/facts/readiness/basic.v
@@ -67,6 +67,6 @@ Section LiuAndLaylandReadiness.
 
 End LiuAndLaylandReadiness.
 
-(** We add the above lemma into a "Hint Database" basic_facts, so Coq
+(** We add the above lemma into a "Hint Database" basic_rt_facts, so Coq
     will be able to apply it automatically. *)
-Global Hint Resolve basic_readiness_is_work_bearing_readiness : basic_facts.
+Global Hint Resolve basic_readiness_is_work_bearing_readiness : basic_rt_facts.
diff --git a/model/priority/classes.v b/model/priority/classes.v
index ac48795dcf47317f38c2209a0e6a11dc74d9e513..c7766865b99a018209bc3b080f19236bcd600819 100644
--- a/model/priority/classes.v
+++ b/model/priority/classes.v
@@ -151,6 +151,6 @@ Section Priorities.
 
 End Priorities.
 
-(** We add the above observation into the "Hint Database" basic_facts, so Coq
+(** We add the above observation into the "Hint Database" basic_rt_facts, so Coq
     will be able to apply it automatically. *)
-Global Hint Resolve respects_sequential_tasks : basic_facts.
+Global Hint Resolve respects_sequential_tasks : basic_rt_facts.
diff --git a/model/priority/deadline_monotonic.v b/model/priority/deadline_monotonic.v
index 625606f0cde83e669c598936676d4f7b6d281e6b..8e9ee8abd024f30aa82d1fb34ee2efcc86bda4bd 100644
--- a/model/priority/deadline_monotonic.v
+++ b/model/priority/deadline_monotonic.v
@@ -35,11 +35,11 @@ Section Properties.
 
 End Properties.
 
-(** We add the above lemmas into a "Hint Database" basic_facts, so Coq
+(** We add the above lemmas into a "Hint Database" basic_rt_facts, so Coq
     will be able to apply them automatically. *)
 Global Hint Resolve
      DM_is_reflexive
      DM_is_transitive
      DM_is_total
-  : basic_facts.
+  : basic_rt_facts.
 
diff --git a/model/priority/edf.v b/model/priority/edf.v
index 24b052b46944b497f941a4a45ef5949b7fc470ee..ea18bac0b1b6fca52df8cf5bbdb7649708fea737 100644
--- a/model/priority/edf.v
+++ b/model/priority/edf.v
@@ -35,11 +35,11 @@ Section PropertiesOfEDF.
 
 End PropertiesOfEDF.
 
-(** We add the above lemmas into a "Hint Database" basic_facts, so Coq
+(** We add the above lemmas into a "Hint Database" basic_rt_facts, so Coq
     will be able to apply them automatically. *)
 Global Hint Resolve
      EDF_is_reflexive
      EDF_is_transitive
      EDF_is_total
-  : basic_facts.
+  : basic_rt_facts.
 
diff --git a/model/priority/fifo.v b/model/priority/fifo.v
index a89e24c90256133d44b0ba33642628b1423365a6..453f296f66b6018b4c1fe2346d8954ea24141503 100644
--- a/model/priority/fifo.v
+++ b/model/priority/fifo.v
@@ -31,11 +31,11 @@ Section Properties.
 
 End Properties.
 
-(** We add the above lemmas into a "Hint Database" basic_facts, so Coq
+(** We add the above lemmas into a "Hint Database" basic_rt_facts, so Coq
     will be able to apply them automatically. *)
 Global Hint Resolve
      FIFO_is_reflexive
      FIFO_is_transitive
      FIFO_is_total
-  : basic_facts.
+  : basic_rt_facts.
 
diff --git a/model/priority/gel.v b/model/priority/gel.v
index 319574e0959478dfd3b424b11382006c63a98488..7127b03b749c835554d2b2e4923abddebd863aee 100644
--- a/model/priority/gel.v
+++ b/model/priority/gel.v
@@ -75,11 +75,11 @@ Section PropertiesOfGEL.
 
 End PropertiesOfGEL.
 
-(** We add the above facts into a "Hint Database" basic_facts, so Coq
+(** We add the above facts into a "Hint Database" basic_rt_facts, so Coq
     will be able to apply them automatically where needed. *)
 Global Hint Resolve
      GEL_is_reflexive
      GEL_is_transitive
      GEL_is_total
-  : basic_facts.
+  : basic_rt_facts.
 
diff --git a/model/priority/numeric_fixed_priority.v b/model/priority/numeric_fixed_priority.v
index 7dfb26e93cab85334aaefdc9116def2408504b74..7f5c73e101e3832954196c6ad459288add2d6b37 100644
--- a/model/priority/numeric_fixed_priority.v
+++ b/model/priority/numeric_fixed_priority.v
@@ -46,11 +46,11 @@ Section Properties.
 
 End Properties.
 
-(** We add the above lemmas into a "Hint Database" basic_facts, so Coq
+(** We add the above lemmas into a "Hint Database" basic_rt_facts, so Coq
     will be able to apply them automatically. *)
 Global Hint Resolve
      NFP_is_reflexive
      NFP_is_transitive
      NFP_is_total
-  : basic_facts.
+  : basic_rt_facts.
 
diff --git a/model/priority/rate_monotonic.v b/model/priority/rate_monotonic.v
index 0af602c49de3674701d0857d8f19cdeea695f402..ca0895ed064e113b19048fc29e6d1e2e716328b0 100644
--- a/model/priority/rate_monotonic.v
+++ b/model/priority/rate_monotonic.v
@@ -37,11 +37,11 @@ Section Properties.
 
 End Properties.
 
-(** We add the above lemmas into a "Hint Database" basic_facts, so Coq
+(** We add the above lemmas into a "Hint Database" basic_rt_facts, so Coq
     will be able to apply them automatically. *)
 Global Hint Resolve
      RM_is_reflexive
      RM_is_transitive
      RM_is_total
-  : basic_facts.
+  : basic_rt_facts.
 
diff --git a/results/edf/rta/bounded_nps.v b/results/edf/rta/bounded_nps.v
index ceec37fd490691d188145c7395940c5f5ed08a1c..123cb771cde38c82c8ef92e8839e01c0e9eed4e1 100644
--- a/results/edf/rta/bounded_nps.v
+++ b/results/edf/rta/bounded_nps.v
@@ -208,7 +208,7 @@ Section RTAforEDFwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
         intros t _; case: (sched t); last by done.
           by intros s; destruct (hep_job s j).
       }
-      edestruct @preemption_time_exists as [ppt [PPT NEQ2]]; eauto 2 with basic_facts.
+      edestruct @preemption_time_exists as [ppt [PPT NEQ2]]; rt_eauto.
       move: NEQ2 => /andP [GE LE].
       apply leq_trans with (cumulative_priority_inversion sched j t1 ppt);
         last apply leq_trans with (ppt - t1).
@@ -222,7 +222,7 @@ Section RTAforEDFwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
         rewrite big_nat_cond big1 //; move => t /andP [/andP [GEt LTt] _ ].
         case SCHED: (sched t) => [s | ]; last by done. 
         edestruct @not_quiet_implies_exists_scheduled_hp_job
-          with (K := ppt - t1) (t := t) as [j_hp [ARRB [HP SCHEDHP]]]; eauto 2 with basic_facts.
+          with (K := ppt - t1) (t := t) as [j_hp [ARRB [HP SCHEDHP]]]; rt_eauto.
         { exists ppt; split.  by done.  by rewrite subnKC //; apply/andP; split. } 
         { by rewrite subnKC //; apply/andP; split. }
         apply/eqP; rewrite eqb0 Bool.negb_involutive.
@@ -273,7 +273,7 @@ Section RTAforEDFwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
     Theorem uniprocessor_response_time_bound_edf_with_bounded_nonpreemptive_segments:
       response_time_bounded_by tsk R.
     Proof.
-      eapply uniprocessor_response_time_bound_edf; eauto 2 with basic_facts.
+      eapply uniprocessor_response_time_bound_edf; rt_eauto.
       - eapply EDF_implies_sequential_tasks; eauto 2.
         + by apply basic.basic_readiness_is_work_bearing_readiness, EDF_is_reflexive.
       - by apply priority_inversion_is_bounded. 
diff --git a/results/edf/rta/bounded_pi.v b/results/edf/rta/bounded_pi.v
index 793083c42afcbf8f3d72b90bfe793fdaf31e8e30..01fa39bfae741b77e49126a19a3d1185009872a3 100644
--- a/results/edf/rta/bounded_pi.v
+++ b/results/edf/rta/bounded_pi.v
@@ -226,9 +226,9 @@ Section AbstractRTAforEDFwithArrivalCurves.
         move => /andP [HYP1 HYP2].
         ideal_proc_model_sched_case_analysis_eq sched t jo.
         { exfalso; clear HYP1 HYP2.
-          eapply instantiated_busy_interval_equivalent_busy_interval in BUSY; eauto 2 with basic_facts.
+          eapply instantiated_busy_interval_equivalent_busy_interval in BUSY; rt_eauto.
           move: BUSY => [PREF _].
-          by eapply not_quiet_implies_not_idle; eauto 2 with basic_facts. }
+          by eapply not_quiet_implies_not_idle; rt_eauto. }
         { clear EqSched_jo; move: Sched_jo; rewrite scheduled_at_def; move => /eqP EqSched_jo.
           rewrite EqSched_jo in HYP1, HYP2. 
           move: HYP1 HYP2.
@@ -258,8 +258,8 @@ Section AbstractRTAforEDFwithArrivalCurves.
       unfold EDF in *.
       intros j t1 t2 ARR TSK POS BUSY.
       move: H_sched_valid => [CARR MBR].
-      eapply instantiated_busy_interval_equivalent_busy_interval in BUSY; eauto 2 with basic_facts.
-      eapply all_jobs_have_completed_equiv_workload_eq_service; eauto 2 with basic_facts.
+      eapply instantiated_busy_interval_equivalent_busy_interval in BUSY; rt_eauto.
+      eapply all_jobs_have_completed_equiv_workload_eq_service; rt_eauto.
       intros s INs TSKs.
       rewrite /arrivals_between in INs. 
       move: (INs) => NEQ.
@@ -286,11 +286,11 @@ Section AbstractRTAforEDFwithArrivalCurves.
       intros j ARR TSK POS.
       move: H_sched_valid => [CARR MBR].
       edestruct exists_busy_interval_from_total_workload_bound
-        with (Δ := L) as [t1 [t2 [T1 [T2 GGG]]]]; eauto 2 with basic_facts.
+        with (Δ := L) as [t1 [t2 [T1 [T2 GGG]]]]; rt_eauto.
       { by intros; rewrite {2}H_fixed_point; apply total_workload_le_total_rbf. }
       exists t1, t2; split; first by done.
       split; first by done.
-      by eapply instantiated_busy_interval_equivalent_busy_interval; eauto 2 with basic_facts.
+      by eapply instantiated_busy_interval_equivalent_busy_interval; rt_eauto.
     Qed.
     
     (** Next, we prove that [IBF_other] is indeed an interference bound. *)
@@ -346,7 +346,7 @@ Section AbstractRTAforEDFwithArrivalCurves.
             + by rewrite /is_priority_inversion leq_addr.
             + by rewrite ltnW.
           - apply H_priority_inversion_is_bounded; try done.
-            eapply instantiated_busy_interval_equivalent_busy_interval in H_busy_interval; eauto 2 with basic_facts.
+            eapply instantiated_busy_interval_equivalent_busy_interval in H_busy_interval; rt_eauto.
             by move: H_busy_interval => [PREF _].
         Qed.
 
@@ -367,9 +367,9 @@ Section AbstractRTAforEDFwithArrivalCurves.
           move: (H_busy_interval) => [[/andP [JINBI JINBI2] [QT _]] _].
           move: H_sched_valid => [CARR MBR].
           erewrite instantiated_cumulative_interference_of_hep_tasks_equal_total_interference_of_hep_tasks;
-            eauto 2 with basic_facts.
+            rt_eauto.
           - by move: (H_job_of_tsk) => /eqP ->; rewrite /jobs.
-          - by rewrite instantiated_quiet_time_equivalent_quiet_time; eauto 2 with basic_facts.
+          - by rewrite instantiated_quiet_time_equivalent_quiet_time; rt_eauto.
         Qed.
 
         (** By lemma [service_of_jobs_le_workload], the total
@@ -380,7 +380,7 @@ Section AbstractRTAforEDFwithArrivalCurves.
           service_of_jobs sched (EDF_not_from tsk) jobs t1 (t1 + Δ)
           <= workload_of_jobs (EDF_not_from tsk) jobs.
         Proof.
-            by apply service_of_jobs_le_workload; eauto 2 with basic_facts.
+            by apply service_of_jobs_le_workload; rt_eauto.
         Qed.
 
         (** Next, we prove that the total workload of jobs
@@ -577,7 +577,7 @@ Section AbstractRTAforEDFwithArrivalCurves.
             by rewrite /completed_by /completed_by ZERO. 
         - move: (BUSY) => [[/andP [JINBI JINBI2] [QT _]] _]. 
           rewrite (cumulative_task_interference_split arr_seq sched _ _ _ tsk j);
-            eauto 2 with basic_facts; last first.
+            rt_eauto; last first.
           { by eapply arrived_between_implies_in_arrivals; eauto. }
           rewrite /I leq_add //.  
           + by apply cumulative_priority_inversion_is_bounded with t2.
@@ -683,7 +683,7 @@ Section AbstractRTAforEDFwithArrivalCurves.
         (task_interference_bound_function := fun tsk A R => IBF_other A R) (L0 := L) ) ||
     eapply uniprocessor_response_time_bound_seq with
         (interference := interference) (interfering_workload := interfering_workload)
-        (task_interference_bound_function := fun tsk A R => IBF_other A R) (L := L)); eauto 2 with basic_facts.
+        (task_interference_bound_function := fun tsk A R => IBF_other A R) (L := L)); rt_eauto.
     - by apply instantiated_i_and_w_are_coherent_with_schedule.
     - by apply instantiated_interference_and_workload_consistent_with_sequential_tasks.
     - by apply instantiated_busy_intervals_are_bounded.
diff --git a/results/edf/rta/floating_nonpreemptive.v b/results/edf/rta/floating_nonpreemptive.v
index 5b752d5c8a64838ed5d8b82c51fbe8228622d7b1..1c1bc8101dc328b376637b049f7c74fd1e7c6db6 100644
--- a/results/edf/rta/floating_nonpreemptive.v
+++ b/results/edf/rta/floating_nonpreemptive.v
@@ -143,7 +143,7 @@ Section RTAforModelWithFloatingNonpreemptiveRegionsWithArrivalCurves.
     move: (LIMJ) => [BEG [END _]].
     try ( eapply uniprocessor_response_time_bound_edf_with_bounded_nonpreemptive_segments with (L0 := L) ) ||
     eapply uniprocessor_response_time_bound_edf_with_bounded_nonpreemptive_segments with (L := L).
-    all: eauto 2 with basic_facts.
+    all: rt_eauto.
     rewrite subnn.
     intros A SP.
     apply H_R_is_maximum in SP.
diff --git a/results/edf/rta/fully_nonpreemptive.v b/results/edf/rta/fully_nonpreemptive.v
index a828bdffa324fd6feea834da4c66602d58cb207c..ff4d924cc4d1657d4578fef5854a8d26ac07b558 100644
--- a/results/edf/rta/fully_nonpreemptive.v
+++ b/results/edf/rta/fully_nonpreemptive.v
@@ -141,7 +141,7 @@ Section RTAforFullyNonPreemptiveEDFModelwithArrivalCurves.
     }
     try ( eapply uniprocessor_response_time_bound_edf_with_bounded_nonpreemptive_segments with (L0 := L) ) ||
     eapply uniprocessor_response_time_bound_edf_with_bounded_nonpreemptive_segments with (L := L).
-    all: eauto 3 with basic_facts.
+    all: rt_eauto.
   Qed.
   
 End RTAforFullyNonPreemptiveEDFModelwithArrivalCurves.
diff --git a/results/edf/rta/fully_preemptive.v b/results/edf/rta/fully_preemptive.v
index 9be9531432810283262d483e1b96b393b523874d..aa060227ef6f3f12c9bf280336f0f56e2fd1d35d 100644
--- a/results/edf/rta/fully_preemptive.v
+++ b/results/edf/rta/fully_preemptive.v
@@ -129,7 +129,7 @@ Section RTAforFullyPreemptiveEDFModelwithArrivalCurves.
                  /fully_preemptive.fully_preemptive_model subnn big1_eq. } 
     try ( eapply uniprocessor_response_time_bound_edf_with_bounded_nonpreemptive_segments with (L0 := L) ) ||
     eapply uniprocessor_response_time_bound_edf_with_bounded_nonpreemptive_segments with (L := L) .
-    all: eauto 2 with basic_facts.
+    all: rt_eauto.
     - move => A /andP [LT NEQ].
       specialize (H_R_is_maximum A); feed H_R_is_maximum.
       { by apply/andP; split. }
diff --git a/results/edf/rta/limited_preemptive.v b/results/edf/rta/limited_preemptive.v
index 061fab7368c193fe24b7a7c7e67b718523ad658a..2004a0e5d28263c2dbe0500e2f151b08b17a3980 100644
--- a/results/edf/rta/limited_preemptive.v
+++ b/results/edf/rta/limited_preemptive.v
@@ -150,7 +150,7 @@ Section RTAforFixedPreemptionPointsModelwithArrivalCurves.
     }
     try ( eapply uniprocessor_response_time_bound_edf_with_bounded_nonpreemptive_segments with (L0 := L) ) ||
     eapply uniprocessor_response_time_bound_edf_with_bounded_nonpreemptive_segments with (L := L).
-    all: eauto 2 with basic_facts.
+    all: rt_eauto.
     rewrite subKn; first by done.
     rewrite /task_last_nonpr_segment  -(leq_add2r 1) subn1 !addn1 prednK; last first.
     - rewrite /last0 -nth_last.
diff --git a/results/fifo/rta.v b/results/fifo/rta.v
index 59e285a0d729204d461997a0f7d55ed7a23fa5fb..ec72b8f43bcb87af9e95baf055022e56da31deea 100644
--- a/results/fifo/rta.v
+++ b/results/fifo/rta.v
@@ -165,9 +165,9 @@ Section AbstractRTAforFIFOwithArrivalCurves.
         ideal_proc_model_sched_case_analysis_eq sched t jo.
         { exfalso; clear HYP1 HYP2.
           destruct H_valid_schedule as [A B].
-          eapply instantiated_busy_interval_equivalent_busy_interval in BUSY; try by eauto 2 with basic_facts.
+          eapply instantiated_busy_interval_equivalent_busy_interval in BUSY; try by rt_eauto.
           move: BUSY => [PREF _].
-          by eapply not_quiet_implies_not_idle; eauto 2 with basic_facts. }
+          by eapply not_quiet_implies_not_idle; rt_eauto. }
         { clear EqSched_jo; move: Sched_jo; rewrite scheduled_at_def; move => /eqP EqSched_jo.
           rewrite EqSched_jo in HYP1, HYP2. 
           move: HYP1 HYP2.
@@ -196,11 +196,11 @@ Section AbstractRTAforFIFOwithArrivalCurves.
       intros j ARR TSK POS.
       destruct H_valid_schedule as [COME MUST ].
       edestruct exists_busy_interval_from_total_workload_bound
-        with (Δ := L) as [t1 [t2 [T1 [T2 GGG]]]]; eauto 2 with basic_facts.
+        with (Δ := L) as [t1 [t2 [T1 [T2 GGG]]]]; rt_eauto.
       { by intros; rewrite {2}H_fixed_point; apply total_workload_le_total_rbf. }
       { exists t1, t2; split; first by done.
         split; first by done.
-        by eapply instantiated_busy_interval_equivalent_busy_interval; eauto 2 with basic_facts. }
+        by eapply instantiated_busy_interval_equivalent_busy_interval; rt_eauto. }
     Qed.
     
     (** In this section, we prove that, under FIFO scheduling, the cumulative priority inversion experienced
@@ -236,7 +236,7 @@ Section AbstractRTAforFIFOwithArrivalCurves.
         destruct (leqP (job_arrival j) t).
         { destruct (completed_by sched j t) eqn : COMPL; last first.
           { apply /negP.
-            eapply (FIFO_implies_no_priority_inversion arr_seq); eauto with basic_facts.
+            eapply (FIFO_implies_no_priority_inversion arr_seq); rt_eauto.
             by apply /andP; split; [| rewrite COMPL]. }
           { rewrite scheduled_at_def in INTER.
             rewrite /is_priority_inversion. 
@@ -249,11 +249,11 @@ Section AbstractRTAforFIFOwithArrivalCurves.
               - by move : INTER => /eqP INTER; rewrite -scheduled_at_def in INTER.
               - by rewrite -ltnNge; apply leq_ltn_trans with (job_arrival j). } 
             apply instantiated_busy_interval_equivalent_busy_interval in H_busy_interval;
-              eauto 2 with basic_facts;last by done.
+              rt_eauto;last by done.
             move : H_busy_interval => [ [_ [_ [QUIET /andP [ARR _ ]]]] _].
             destruct (leqP t t1) as [LE | LT].
             { have EQ : t = job_arrival j by apply eq_trans with t1; lia.
-              rewrite EQ in COMPL; apply completed_on_arrival_implies_zero_cost in COMPL; eauto with basic_facts.
+              rewrite EQ in COMPL; apply completed_on_arrival_implies_zero_cost in COMPL; rt_eauto.
               by move: (H_job_cost_positive); rewrite /job_cost_positive COMPL. }
             { specialize (QUIET t); feed QUIET.
               - apply /andP; split; first by done.
@@ -284,9 +284,9 @@ Section AbstractRTAforFIFOwithArrivalCurves.
       move: (BUSY) => [ [ /andP [LE GT] [QUIETt1 _ ] ] [QUIETt2 EQNs]].
       erewrite (cumulative_priority_inversion_is_bounded j ARRj JPOS t1 t2); rewrite //= add0n.
       rewrite (instantiated_cumulative_interference_of_hep_jobs_equal_total_interference_of_hep_jobs arr_seq) //=; 
-              try by (try rewrite instantiated_quiet_time_equivalent_quiet_time); eauto 2 with basic_facts.
-      eapply leq_trans; first by apply service_of_jobs_le_workload; eauto 2 with basic_facts.
-      rewrite (leqRW (workload_equal_subset _ _ _ _ _ _  _)); eauto 2 with basic_facts.
+              try by (try rewrite instantiated_quiet_time_equivalent_quiet_time); rt_eauto.
+      eapply leq_trans; first by apply service_of_jobs_le_workload; rt_eauto.
+      rewrite (leqRW (workload_equal_subset _ _ _ _ _ _  _)); rt_eauto.
       specialize (workload_minus_job_cost j) => ->.
       { rewrite /workload_of_jobs /IBF (big_rem tsk) //= (addnC (rbf tsk (job_arrival j - t1 + ε))).
         rewrite -addnBA; last first.
@@ -386,12 +386,12 @@ Section AbstractRTAforFIFOwithArrivalCurves.
             have GE: task_cost tsk <= R; last by lia.
             rewrite !add0n in LE1.
             rewrite -(leqRW LE2) -(leqRW LE1).
-            by eapply (task_cost_le_sum_rbf arr_seq); eauto with basic_facts. }
+            by eapply (task_cost_le_sum_rbf arr_seq); rt_eauto. }
         { rewrite subnK; first by done.
           rewrite !add0n in LE1. apply leq_trans with F; last by done.
           apply leq_trans with (\sum_(tsko <- ts) rbf tsko ε); last by done.
           apply leq_trans with (task_cost tsk); first by lia.
-          eapply task_cost_le_sum_rbf; eauto with basic_facts. }
+          eapply task_cost_le_sum_rbf; rt_eauto. }
       Qed.
       
     End SolutionOfResponseTimeReccurenceExists.
@@ -412,7 +412,7 @@ Section AbstractRTAforFIFOwithArrivalCurves.
       (interference_bound_function := fun tsk A R => IBF tsk A R) (L0 := L) ) ||
     eapply uniprocessor_response_time_bound with
       (interference := interference) (interfering_workload := interfering_workload)
-      (interference_bound_function := fun tsk A R => IBF tsk A R) (L := L)); eauto 2 with basic_facts.
+      (interference_bound_function := fun tsk A R => IBF tsk A R) (L := L)); rt_eauto.
     - by apply instantiated_i_and_w_are_coherent_with_schedule.
     - by apply instantiated_busy_intervals_are_bounded.
     - by apply instantiated_interference_is_bounded.
diff --git a/results/fixed_priority/rta/bounded_nps.v b/results/fixed_priority/rta/bounded_nps.v
index 40bce6903858ddbed284a3bb66c4bba8d5e69d5d..1a7068ab5babe7ff2ce7722541ec9f9dddf6a212 100644
--- a/results/fixed_priority/rta/bounded_nps.v
+++ b/results/fixed_priority/rta/bounded_nps.v
@@ -173,7 +173,7 @@ Section RTAforFPwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
         by intros s; case: (hep_job s j). 
       } 
       move: NEQ => /negP /negP; rewrite -ltnNge; move => BOUND.
-      edestruct (@preemption_time_exists) as [ppt [PPT NEQ]]; eauto 2 with basic_facts.
+      edestruct (@preemption_time_exists) as [ppt [PPT NEQ]]; rt_eauto.
       move: NEQ => /andP [GE LE].
       apply leq_trans with (cumulative_priority_inversion sched j t1 ppt);
         last apply leq_trans with (ppt - t1); first last.
@@ -196,7 +196,7 @@ Section RTAforFPwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
         case SCHED: (sched t) => [s | ]; last by done.
         edestruct (@not_quiet_implies_exists_scheduled_hp_job)
           with (K := ppt - t1) (t1 := t1) (t2 := t2) (t := t)
-          as [j_hp [ARRB [HP SCHEDHP]]]; eauto 2 with basic_facts.
+          as [j_hp [ARRB [HP SCHEDHP]]]; rt_eauto.
         { by exists ppt; split; [done | rewrite subnKC //; apply/andP]. } 
         { by rewrite subnKC //; apply/andP; split. }
         apply/eqP; rewrite eqb0 Bool.negb_involutive.
@@ -242,7 +242,7 @@ Section RTAforFPwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
       response_time_bounded_by tsk R.
     Proof.
       eapply uniprocessor_response_time_bound_fp;
-        eauto using priority_inversion_is_bounded with basic_facts. 
+        eauto using priority_inversion_is_bounded with basic_rt_facts. 
     Qed.
     
   End ResponseTimeBound.
diff --git a/results/fixed_priority/rta/bounded_pi.v b/results/fixed_priority/rta/bounded_pi.v
index 3f59660980b9a93a8b8107c8fe79b9339f2e3528..38f8f68c8edee66f2c6684f2af764fa88ae873f4 100644
--- a/results/fixed_priority/rta/bounded_pi.v
+++ b/results/fixed_priority/rta/bounded_pi.v
@@ -200,8 +200,8 @@ Section AbstractRTAforFPwithArrivalCurves.
           * by exfalso.
           * by subst s; rewrite scheduled_at_def //; apply/eqP. 
         + exfalso; clear HYP1 HYP2.
-          eapply instantiated_busy_interval_equivalent_busy_interval in BUSY; eauto with basic_facts.
-          by move: BUSY => [PREF _]; eapply not_quiet_implies_not_idle; eauto 2 with basic_facts; apply/eqP.
+          eapply instantiated_busy_interval_equivalent_busy_interval in BUSY; rt_eauto.
+          by move: BUSY => [PREF _]; eapply not_quiet_implies_not_idle; rt_eauto; apply/eqP.
       - move: (HYP); rewrite scheduled_at_def; move => /eqP HYP2; apply/negP.
         rewrite /interference /ideal_jlfp_rta.interference /is_priority_inversion
                   /is_interference_from_another_hep_job HYP2 negb_or.
@@ -219,8 +219,8 @@ Section AbstractRTAforFPwithArrivalCurves.
     Proof.
       intros j t1 t2 ARR TSK POS BUSY.
       move: H_sched_valid => [CARR MBR].
-      eapply instantiated_busy_interval_equivalent_busy_interval in BUSY; eauto with basic_facts.
-      eapply all_jobs_have_completed_equiv_workload_eq_service; eauto with basic_facts.
+      eapply instantiated_busy_interval_equivalent_busy_interval in BUSY; rt_eauto.
+      eapply all_jobs_have_completed_equiv_workload_eq_service; rt_eauto.
       intros s ARRs TSKs.
       move: (BUSY) => [[_ [QT _]] _].
       apply QT.
@@ -243,11 +243,11 @@ Section AbstractRTAforFPwithArrivalCurves.
       intros j ARR TSK POS.
       move: H_sched_valid => [CARR MBR].
       edestruct (exists_busy_interval) with (delta := L) as [t1 [t2 [T1 [T2 GGG]]]];
-        eauto 2 with basic_facts.
+        rt_eauto.
       { by intros; rewrite {2}H_fixed_point leq_add //; apply total_workload_le_total_hep_rbf. }
       exists t1, t2; split; first by done.
       split; first by done.
-      by eapply instantiated_busy_interval_equivalent_busy_interval; eauto 2 with basic_facts.
+      by eapply instantiated_busy_interval_equivalent_busy_interval; rt_eauto.
     Qed.
 
     (** Next, we prove that [IBF_other] is indeed an interference bound.
@@ -271,8 +271,8 @@ Section AbstractRTAforFPwithArrivalCurves.
       move: H_sched_valid => [CARR MBR].
       move: (posnP (@job_cost _ Cost j)) => [ZERO|POS].
       { by exfalso; rewrite /completed_by ZERO in  NCOMPL. }
-      eapply instantiated_busy_interval_equivalent_busy_interval in BUSY; eauto 2 with basic_facts.
-      rewrite /interference; erewrite cumulative_task_interference_split; eauto 2 with basic_facts; last first.
+      eapply instantiated_busy_interval_equivalent_busy_interval in BUSY; rt_eauto.
+      rewrite /interference; erewrite cumulative_task_interference_split; rt_eauto; last first.
       { move: BUSY => [[_ [_ [_ /andP [GE LT]]]] _].
           by eapply arrived_between_implies_in_arrivals; eauto 2. }
       unfold IBF_other, interference.
@@ -297,7 +297,7 @@ Section AbstractRTAforFPwithArrivalCurves.
         { rewrite /workload_of_jobs /total_ohep_rbf /total_ohep_request_bound_function_FP.
           move: (TSK) => /eqP <-; apply total_workload_le_total_ohep_rbf; try done.
           by move: (TSK) => /eqP ->. } 
-        all: eauto 2 using arr_seq with basic_facts. }
+        all: eauto 2 using arr_seq with basic_rt_facts. }
     Qed.
 
     (** Finally, we show that there exists a solution for the response-time recurrence. *)
@@ -368,7 +368,7 @@ Section AbstractRTAforFPwithArrivalCurves.
     move: H_sched_valid => [CARR MBR].
     move: (posnP (@job_cost _ Cost js)) => [ZERO|POS].
     { by rewrite /job_response_time_bound /completed_by ZERO. }
-    eapply uniprocessor_response_time_bound_seq; eauto 2 with basic_facts.
+    eapply uniprocessor_response_time_bound_seq; rt_eauto.
     - by apply instantiated_i_and_w_are_consistent_with_schedule. 
     - by apply instantiated_interference_and_workload_consistent_with_sequential_tasks. 
     - by apply instantiated_busy_intervals_are_bounded.
diff --git a/results/fixed_priority/rta/floating_nonpreemptive.v b/results/fixed_priority/rta/floating_nonpreemptive.v
index 4699544090733a1cdf67f50bf8b6ea37a9a1ebcc..73a987d3e4e305ada2747bab4eb1cde8f97ee9be 100644
--- a/results/fixed_priority/rta/floating_nonpreemptive.v
+++ b/results/fixed_priority/rta/floating_nonpreemptive.v
@@ -148,7 +148,7 @@ Section RTAforFloatingModelwithArrivalCurves.
     move: (H_valid_task_model_with_floating_nonpreemptive_regions) => [LIMJ JMLETM].
     move: (LIMJ) => [BEG [END _]].
     eapply uniprocessor_response_time_bound_fp_with_bounded_nonpreemptive_segments.
-    all: eauto 2 with basic_facts.
+    all: rt_eauto.
     - by apply sequential_readiness_implies_work_bearing_readiness.
     - by apply sequential_readiness_implies_sequential_tasks.
     - intros A SP.
diff --git a/results/fixed_priority/rta/fully_nonpreemptive.v b/results/fixed_priority/rta/fully_nonpreemptive.v
index 925ad4882d48201d14416e369aef05c32387e8c2..e3d35cf107bef20c00f437ce0563bc2dce03d302 100644
--- a/results/fixed_priority/rta/fully_nonpreemptive.v
+++ b/results/fixed_priority/rta/fully_nonpreemptive.v
@@ -154,7 +154,7 @@ Section RTAforFullyNonPreemptiveFPModelwithArrivalCurves.
         (L0 := L) ) ||
     eapply uniprocessor_response_time_bound_fp_with_bounded_nonpreemptive_segments with
         (L := L).
-    all: eauto 3 with basic_facts.
+    all: rt_eauto.
     - by apply sequential_readiness_implies_work_bearing_readiness.
     - by apply sequential_readiness_implies_sequential_tasks.
   Qed.
diff --git a/results/fixed_priority/rta/fully_preemptive.v b/results/fixed_priority/rta/fully_preemptive.v
index 28ceef67f90438fcac8de2897cd2cdcc6425ceea..31574f38f760e4b538e97df8871d2b9827c3fe6b 100644
--- a/results/fixed_priority/rta/fully_preemptive.v
+++ b/results/fixed_priority/rta/fully_preemptive.v
@@ -136,7 +136,7 @@ Section RTAforFullyPreemptiveFPModelwithArrivalCurves.
     { by rewrite /blocking_bound /parameters.task_max_nonpreemptive_segment
                /fully_preemptive.fully_preemptive_model subnn big1_eq. } 
     eapply uniprocessor_response_time_bound_fp_with_bounded_nonpreemptive_segments.      
-    all: eauto 2 with basic_facts.
+    all: rt_eauto.
     rewrite /work_bearing_readiness.
     - by apply sequential_readiness_implies_work_bearing_readiness.
     - by apply sequential_readiness_implies_sequential_tasks => //.
diff --git a/results/fixed_priority/rta/limited_preemptive.v b/results/fixed_priority/rta/limited_preemptive.v
index 1dadfd26cc56c782cc2375c1d3575ea0789eeb7d..4d39b8f3246447fb9418dd1dd4764f6d72ad50e6 100644
--- a/results/fixed_priority/rta/limited_preemptive.v
+++ b/results/fixed_priority/rta/limited_preemptive.v
@@ -158,7 +158,7 @@ Section RTAforFixedPreemptionPointsModelwithArrivalCurves.
       with (L0 := L) ) ||
     eapply uniprocessor_response_time_bound_fp_with_bounded_nonpreemptive_segments
       with (L := L).
-    all: eauto 2 with basic_facts.
+    all: rt_eauto.
     - by apply sequential_readiness_implies_work_bearing_readiness.
     - by apply sequential_readiness_implies_sequential_tasks.
     - intros A SP.
diff --git a/util/tactics.v b/util/tactics.v
index 074cda81cc536a0c047af1f8fa15d03c1c431821..7f38418aa01b52ba9829c9d47aba9f7c71414817 100644
--- a/util/tactics.v
+++ b/util/tactics.v
@@ -83,6 +83,20 @@ Ltac feed_n n H := match constr:(n) with
   | (S ?m) => feed H ; [| feed_n m H]
   end.
 
+(** We introduce tactics [rt_auto] and [rt_eauto] as a shorthand for
+    [(e)auto with basic_rt_facts] to facilitate automation. Here, we
+    use scope [basic_rt_facts] that contains a collection of basic
+    real-time theory lemmas. *)
+(** Note: constant [3] was chosen because most of the basic rt facts
+    have the structure [A1 -> A2 -> ... B], where [Ai] is a hypothesis
+    usually present in the context, which gives the depth of the
+    search which is equal to two. One additional level of depth (3)
+    was added to support rare exceptions to this rule. At the same
+    time, the constant should not be too large to avoid slowdowns in
+    case of an unsuccessful application of automation. *)
+Ltac rt_auto := auto 3 with basic_rt_facts.
+Ltac rt_eauto := eauto 3 with basic_rt_facts.
+
 (* ************************************************************************** *)
 (** * Handier movement of inequalities. *)
 (* ************************************************************************** *)