diff --git a/model/task/arrival/curve_as_rbf.v b/model/task/arrival/curve_as_rbf.v
index 27d3c62d926804680e3ccc8b1f6dedeb4f0660fd..c99d6015df208b02d63a563ad6dbae41460ae3fe 100644
--- a/model/task/arrival/curve_as_rbf.v
+++ b/model/task/arrival/curve_as_rbf.v
@@ -172,3 +172,12 @@ Section ArrivalCurveToRBF.
   End Facts.
   
 End ArrivalCurveToRBF.
+
+(** We add the lemmas into the "Hint Database" basic_rt_facts so that
+    they become available for proof automation. *)
+Global Hint Resolve
+  valid_arrival_curve_to_max_rbf
+  respects_arrival_curve_to_max_rbf
+  valid_taskset_arrival_curve_to_max_rbf
+  taskset_respects_arrival_curve_to_max_rbf
+  : basic_rt_facts.
diff --git a/util/tactics.v b/util/tactics.v
index 7f38418aa01b52ba9829c9d47aba9f7c71414817..603bb587d7e274fbcab6f9dc7e7cd25273ac8ca0 100644
--- a/util/tactics.v
+++ b/util/tactics.v
@@ -87,15 +87,17 @@ Ltac feed_n n H := match constr:(n) with
     [(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
+(** Note: constant [4] 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.
+    search which is equal to two. Two additional levels of depth (4)
+    was added to support rare exceptions to this rule. In particular,
+    depth 4 is needed for automatic periodic->RBF arrival model
+    conversion. 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 4 with basic_rt_facts.
+Ltac rt_eauto := eauto 4 with basic_rt_facts.
 
 (* ************************************************************************** *)
 (** * Handier movement of inequalities. *)