diff --git a/analysis/facts/behavior/arrivals.v b/analysis/facts/behavior/arrivals.v
index 31612165f0a8d3fbb4ceb8326fe2a307eed0a1f7..3ff7f97392e2ec285756ba0059338b0e0d02cbbb 100644
--- a/analysis/facts/behavior/arrivals.v
+++ b/analysis/facts/behavior/arrivals.v
@@ -83,6 +83,16 @@ Section Arrived.
     by apply ready_implies_arrived.
   Qed.
 
+  (** Furthermore, in a valid schedule, jobs must arrive to execute. *)
+  Corollary valid_schedule_implies_jobs_must_arrive_to_execute:
+    forall arr_seq, 
+    valid_schedule sched arr_seq ->
+    jobs_must_arrive_to_execute sched.
+  Proof.
+    move=> arr_seq [??].
+    by apply jobs_must_arrive_to_be_ready.
+  Qed.
+  
   (** Since backlogged jobs are by definition ready, any backlogged job must have arrived. *)
   Corollary backlogged_implies_arrived:
     forall j t,
@@ -108,6 +118,10 @@ Section Arrived.
 
 End Arrived.
 
+(** We add the above lemma into a "Hint Database" basic_facts, so Coq
+    will be able to apply it automatically. *)
+Global Hint Resolve valid_schedule_implies_jobs_must_arrive_to_execute : basic_facts.
+
 (** In this section, we establish useful facts about arrival sequence prefixes. *)
 Section ArrivalSequencePrefix.
 
diff --git a/analysis/facts/behavior/completion.v b/analysis/facts/behavior/completion.v
index eaf7c733f2dce11d445c371f5c05fc0c0c6bb018..00b864885ebccc9495d3982fec9e55ceb79a0645 100644
--- a/analysis/facts/behavior/completion.v
+++ b/analysis/facts/behavior/completion.v
@@ -345,6 +345,16 @@ Section CompletedJobs.
     by apply ready_implies_incomplete.
   Qed.
 
+  (** Furthermore, in a valid schedule, completed jobs don't execute. *)
+  Corollary valid_schedule_implies_completed_jobs_dont_execute:
+    forall arr_seq, 
+    valid_schedule sched arr_seq ->
+    completed_jobs_dont_execute sched.
+  Proof.
+    move=> arr_seq [??].
+    by apply completed_jobs_are_not_ready.
+  Qed.
+
   (** We further observe that completed jobs don't execute if scheduled jobs
      always receive non-zero service and cumulative service never exceeds job
      costs. *)
@@ -363,6 +373,10 @@ Section CompletedJobs.
 
 End CompletedJobs.
 
+(** We add the above lemma into a "Hint Database" basic_facts, so Coq
+    will be able to apply it automatically. *)
+Global Hint Resolve valid_schedule_implies_completed_jobs_dont_execute : basic_facts.
+
 (** Next, we relate the completion of jobs in schedules with identical prefixes. *)
 Section CompletionInTwoSchedules.
   (** Consider any processor model and any type of jobs with costs, arrival times, and a notion of readiness. *)
diff --git a/results/edf/rta/bounded_nps.v b/results/edf/rta/bounded_nps.v
index 0249c761626e943154b48c95367d9aa8c86e39ab..724872487ecd8587b7f52116c5a8848745f18edc 100644
--- a/results/edf/rta/bounded_nps.v
+++ b/results/edf/rta/bounded_nps.v
@@ -58,10 +58,6 @@ Section RTAforEDFwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
   Variable sched : schedule (ideal.processor_state Job).
   Hypothesis H_sched_valid : valid_schedule sched arr_seq.
   
-  (** ... where jobs do not execute before their arrival or after completion. *)
-  Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
-  Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
-  
   (** In addition, we assume the existence of a function mapping jobs
       to their preemption points ... *)
   Context `{JobPreemptable Job}.
@@ -277,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.
+      eapply uniprocessor_response_time_bound_edf; eauto 2 with basic_facts.
       - 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 965e25fc0ac070269e0783357f130874c23b2ded..4df6367f7370afb1c2924a9d912db053c58a9247 100644
--- a/results/edf/rta/bounded_pi.v
+++ b/results/edf/rta/bounded_pi.v
@@ -67,10 +67,6 @@ Section AbstractRTAforEDFwithArrivalCurves.
   Variable sched : schedule (ideal.processor_state Job).
   Hypothesis H_sched_valid : valid_schedule sched arr_seq.
 
-  (** ... where jobs do not execute before their arrival or after completion. *)
-  Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
-  Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
-
   (** Note that we differentiate between abstract and 
      classical notions of work conserving schedule. *)
   Let work_conserving_ab := definitions.work_conserving arr_seq sched.
@@ -370,9 +366,7 @@ Section AbstractRTAforEDFwithArrivalCurves.
           erewrite instantiated_cumulative_interference_of_hep_tasks_equal_total_interference_of_hep_tasks;
             eauto 2 with basic_facts.
           - by rewrite -H_job_of_tsk /jobs.
-          - rewrite /edf.EDF /EDF instantiated_quiet_time_equivalent_quiet_time //.
-            + by apply EDF_is_reflexive.
-            + by apply EDF_respects_sequential_tasks.
+          - rewrite instantiated_quiet_time_equivalent_quiet_time; eauto 2 with basic_facts.
         Qed.
 
         (** By lemma [service_of_jobs_le_workload], the total
@@ -689,7 +683,7 @@ Section AbstractRTAforEDFwithArrivalCurves.
     { by rewrite /job_response_time_bound /completed_by ZERO. }    
     eapply uniprocessor_response_time_bound_seq with
         (interference0 := interference) (interfering_workload0 := interfering_workload)
-        (task_interference_bound_function := fun tsk A R => IBF A R) (L0 := L); eauto 3.
+        (task_interference_bound_function := fun tsk A R => IBF A R) (L0 := L); eauto 2 with basic_facts.
     - 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 d12eb4c3d33251d32793e3dde2b56b726178c7c7..d8e0a69359ca9b6b397f31434e852261e378ad4e 100644
--- a/results/edf/rta/floating_nonpreemptive.v
+++ b/results/edf/rta/floating_nonpreemptive.v
@@ -74,10 +74,6 @@ Section RTAforModelWithFloatingNonpreemptiveRegionsWithArrivalCurves.
   Hypothesis H_sched_valid: valid_schedule sched arr_seq.
   Hypothesis H_schedule_with_limited_preemptions:
     schedule_respects_preemption_model arr_seq sched.
-  
-  (** ... where jobs do not execute before their arrival or after completion. *)
-  Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
-  Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
 
   (** Next, we assume that the schedule is a work-conserving schedule... *)
   Hypothesis H_work_conserving : work_conserving arr_seq sched.
diff --git a/results/edf/rta/fully_nonpreemptive.v b/results/edf/rta/fully_nonpreemptive.v
index 2d8d78d569a5a2f82984b37f92327a570d53891e..8b1c16ddfc219fb70967730a8a46088cecc2d765 100644
--- a/results/edf/rta/fully_nonpreemptive.v
+++ b/results/edf/rta/fully_nonpreemptive.v
@@ -64,10 +64,6 @@ Section RTAforFullyNonPreemptiveEDFModelwithArrivalCurves.
   Variable sched : schedule (ideal.processor_state Job).
   Hypothesis H_sched_valid: valid_schedule sched arr_seq.
   Hypothesis H_nonpreemptive_sched : nonpreemptive_schedule sched.
-  
-  (** ... where jobs do not execute before their arrival or after completion. *)
-  Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
-  Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
 
   (** Next, we assume that the schedule is a work-conserving schedule... *)
   Hypothesis H_work_conserving : work_conserving arr_seq sched.  
@@ -141,7 +137,7 @@ Section RTAforFullyNonPreemptiveEDFModelwithArrivalCurves.
         by rewrite /job_response_time_bound /completed_by ZEROj.
     }
     eapply uniprocessor_response_time_bound_edf_with_bounded_nonpreemptive_segments with (L0 := L).
-    all: eauto 2 with basic_facts.
+    all: eauto 3 with basic_facts.
   Qed.
   
 End RTAforFullyNonPreemptiveEDFModelwithArrivalCurves.
diff --git a/results/edf/rta/fully_preemptive.v b/results/edf/rta/fully_preemptive.v
index e7f66b7b2a17c446d5375f0b8b1b3974478ec46e..4b1bf311c4e261d2cc697c60a9b5a8d2a61e1c17 100644
--- a/results/edf/rta/fully_preemptive.v
+++ b/results/edf/rta/fully_preemptive.v
@@ -65,10 +65,6 @@ Section RTAforFullyPreemptiveEDFModelwithArrivalCurves.
   Hypothesis H_jobs_come_from_arrival_sequence:
     jobs_come_from_arrival_sequence sched arr_seq.
 
-  (** ... where jobs do not execute before their arrival or after completion. *)
-  Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
-  Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
-
   (** Next, we assume that the schedule is a work-conserving schedule... *)
   Hypothesis H_work_conserving : work_conserving arr_seq sched.
   
diff --git a/results/edf/rta/limited_preemptive.v b/results/edf/rta/limited_preemptive.v
index 7bf011585fd5074c1b9eddba1d87427a61d23852..07c3c9fa792a3e72d2c91a2cf565e1391d1ac6ea 100644
--- a/results/edf/rta/limited_preemptive.v
+++ b/results/edf/rta/limited_preemptive.v
@@ -75,10 +75,6 @@ Section RTAforFixedPreemptionPointsModelwithArrivalCurves.
   Hypothesis H_sched_valid: valid_schedule sched arr_seq.
   Hypothesis H_schedule_with_limited_preemptions:
     schedule_respects_preemption_model arr_seq sched.
-  
-  (** ... where jobs do not execute before their arrival or after completion. *)
-  Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
-  Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
 
   (** Next, we assume that the schedule is a work-conserving schedule... *)
   Hypothesis H_work_conserving : work_conserving arr_seq sched.
diff --git a/results/fixed_priority/rta/bounded_nps.v b/results/fixed_priority/rta/bounded_nps.v
index 7224726f06d6140b8049f98f5148a43da696e261..019dbefa3f9c41d57c7c3b23b37d3fb656ee36c1 100644
--- a/results/fixed_priority/rta/bounded_nps.v
+++ b/results/fixed_priority/rta/bounded_nps.v
@@ -54,10 +54,6 @@ Section RTAforFPwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
 
   (** ... and assume that the schedule is valid.  *)
   Hypothesis H_sched_valid : valid_schedule sched arr_seq.
-
-  (** We also assume that jobs do not execute before their arrival or after completion. *)
-  Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
-  Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
   
   (** In addition, we assume the existence of a function mapping jobs
       to their preemption points ... *)
@@ -177,7 +173,8 @@ 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; move: NEQ => /andP [GE LE].
+      edestruct (@preemption_time_exists) as [ppt [PPT NEQ]]; eauto 2 with basic_facts.
+      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.
       - rewrite leq_subLR.
@@ -198,7 +195,8 @@ Section RTAforFPwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
         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) (t1 := t1) (t2 := t2) (t := t) as [j_hp [ARRB [HP SCHEDHP]]]; eauto 2.
+          with (K := ppt - t1) (t1 := t1) (t2 := t2) (t := t)
+          as [j_hp [ARRB [HP SCHEDHP]]]; eauto 2 with basic_facts.
         { by exists ppt; split; [done | rewrite subnKC //; apply/andP]. } 
         { by rewrite subnKC //; apply/andP; split. }
         apply/eqP; rewrite eqb0 Bool.negb_involutive.
@@ -244,7 +242,7 @@ Section RTAforFPwithBoundedNonpreemptiveSegmentsWithArrivalCurves.
       response_time_bounded_by tsk R.
     Proof.
       eapply uniprocessor_response_time_bound_fp;
-        eauto using priority_inversion_is_bounded. 
+        eauto using priority_inversion_is_bounded with basic_facts. 
     Qed.
     
   End ResponseTimeBound.
diff --git a/results/fixed_priority/rta/bounded_pi.v b/results/fixed_priority/rta/bounded_pi.v
index c78811bd0a3d3a8e487cdc95c2e7d83bd9c0726c..2489c3064a019e97eaedc9cbec05734fcafcd1d4 100644
--- a/results/fixed_priority/rta/bounded_pi.v
+++ b/results/fixed_priority/rta/bounded_pi.v
@@ -60,10 +60,6 @@ Section AbstractRTAforFPwithArrivalCurves.
   (** ... and assume that the schedule is valid.  *)
   Hypothesis H_sched_valid : valid_schedule sched arr_seq.
 
-  (** We also assume that jobs do not execute before their arrival or after completion. *)
-  Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
-  Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
-  
   (** Note that we differentiate between abstract and 
      classical notions of work conserving schedule. *)
   Let work_conserving_ab := definitions.work_conserving arr_seq sched.
@@ -205,7 +201,7 @@ Section AbstractRTAforFPwithArrivalCurves.
         + exfalso; clear HYP1 HYP2.
           eapply instantiated_busy_interval_equivalent_edf_busy_interval in BUSY; eauto with basic_facts.
             by move: BUSY => [PREF _]; eapply not_quiet_implies_not_idle;
-                              eauto 2 using eqprop_to_eqbool.
+                              eauto 2 using eqprop_to_eqbool with basic_facts.
       - 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.
@@ -246,7 +242,8 @@ Section AbstractRTAforFPwithArrivalCurves.
     Proof.
       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.
+      edestruct (exists_busy_interval) with (delta := L) as [t1 [t2 [T1 [T2 GGG]]]];
+        eauto 2 with basic_facts.
       { by intros; rewrite {2}H_fixed_point leq_add //; apply total_workload_le_total_rbf'. }
       exists t1, t2; split; first by done.
       split; first by done.
@@ -295,11 +292,11 @@ Section AbstractRTAforFPwithArrivalCurves.
             (workload_of_jobs
                (fun jhp : Job => (FP_to_JLFP _ _) jhp j && (job_task jhp != job_task j))
                (arrivals_between arr_seq t1 (t1 + R0))).
-        { by apply service_of_jobs_le_workload; first apply ideal_proc_model_provides_unit_service. } 
+        { apply service_of_jobs_le_workload; first apply ideal_proc_model_provides_unit_service.
+          by apply (valid_schedule_implies_completed_jobs_dont_execute sched arr_seq). } 
         { rewrite /workload_of_jobs /total_ohep_rbf /total_ohep_request_bound_function_FP.
-          by rewrite -TSK; apply total_workload_le_total_rbf.
-        }
-      }
+          by rewrite -TSK; apply total_workload_le_total_rbf. } 
+        all: eauto 2 using arr_seq with basic_facts. }
     Qed.
 
     (** Finally, we show that there exists a solution for the response-time recurrence. *)
@@ -370,7 +367,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 3.
+    eapply uniprocessor_response_time_bound_seq; eauto 2 with basic_facts.
     - 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 a420c2cfe0e99929377a10577d7c30eb1a49a60d..10396808f69ad7b6d93cbde7a1cb9a22ce2de870 100644
--- a/results/fixed_priority/rta/floating_nonpreemptive.v
+++ b/results/fixed_priority/rta/floating_nonpreemptive.v
@@ -75,10 +75,6 @@ Section RTAforFloatingModelwithArrivalCurves.
   Variable sched : schedule (ideal.processor_state Job).
   Hypothesis H_sched_valid : valid_schedule sched arr_seq.
   Hypothesis H_schedule_with_limited_preemptions : schedule_respects_preemption_model arr_seq sched.
-  
-  (** ... where jobs do not execute before their arrival or after completion. *)
-  Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
-  Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
 
   (** Consider an FP policy that indicates a higher-or-equal priority relation,
       and assume that the relation is reflexive and transitive. *)
diff --git a/results/fixed_priority/rta/fully_nonpreemptive.v b/results/fixed_priority/rta/fully_nonpreemptive.v
index 1f4f18249357b1ea474353617a3f12893df3e0e3..0ba1115e8551920bab3a0b292a47982f4f83e5e2 100644
--- a/results/fixed_priority/rta/fully_nonpreemptive.v
+++ b/results/fixed_priority/rta/fully_nonpreemptive.v
@@ -68,10 +68,6 @@ Section RTAforFullyNonPreemptiveFPModelwithArrivalCurves.
   Hypothesis H_sched_valid : valid_schedule sched arr_seq.
   Hypothesis H_nonpreemptive_sched : nonpreemptive_schedule  sched.
 
-  (** ... where jobs do not execute before their arrival or after completion. *)
-  Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
-  Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
-
   (** Consider an FP policy that indicates a higher-or-equal priority relation,
      and assume that the relation is reflexive and transitive. *)
   Context `{FP_policy Task}.
@@ -153,7 +149,7 @@ Section RTAforFullyNonPreemptiveFPModelwithArrivalCurves.
     }
     eapply uniprocessor_response_time_bound_fp_with_bounded_nonpreemptive_segments with
         (L0 := L).
-    all: eauto 2 with basic_facts.
+    all: eauto 3 with basic_facts.
     - 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 1f1913a83ebdcc7c419403c78e8430dcd1a45f57..15e1f4670ed98bee97fdae9a44ed76f09dca6acf 100644
--- a/results/fixed_priority/rta/fully_preemptive.v
+++ b/results/fixed_priority/rta/fully_preemptive.v
@@ -68,10 +68,6 @@ Section RTAforFullyPreemptiveFPModelwithArrivalCurves.
   Hypothesis H_jobs_come_from_arrival_sequence:
     jobs_come_from_arrival_sequence sched arr_seq.
 
-  (** ... where jobs do not execute before their arrival or after completion. *)
-  Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
-  Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
-
   (** Consider an FP policy that indicates a higher-or-equal priority relation,
      and assume that the relation is reflexive and transitive. *)
   Context `{FP_policy Task}.
diff --git a/results/fixed_priority/rta/limited_preemptive.v b/results/fixed_priority/rta/limited_preemptive.v
index 4707900dc6835a251de2d7358a7bd2cbbf79440b..a3d0b71da247c5e8aa9059655f1e67e4e055ff14 100644
--- a/results/fixed_priority/rta/limited_preemptive.v
+++ b/results/fixed_priority/rta/limited_preemptive.v
@@ -76,10 +76,6 @@ Section RTAforFixedPreemptionPointsModelwithArrivalCurves.
   Hypothesis H_schedule_respects_preemption_model:
     schedule_respects_preemption_model arr_seq sched.
 
-  (** ... where jobs do not execute before their arrival or after completion. *)
-  Hypothesis H_jobs_must_arrive_to_execute : jobs_must_arrive_to_execute sched.
-  Hypothesis H_completed_jobs_dont_execute : completed_jobs_dont_execute sched.
-
   (** Consider an FP policy that indicates a higher-or-equal priority relation,
      and assume that the relation is reflexive and transitive. *)
   Context `{FP_policy Task}.