[STATEMENT]
theorem sublistD_bounds_D_and_RD_bounds_sublistD: 
  fixes PROB :: "'a problem"
  assumes "finite PROB"
  shows "
    problem_plan_bound_charles PROB \<le> problem_plan_bound PROB 
    \<and> problem_plan_bound PROB \<le> RD PROB
  "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. problem_plan_bound_charles PROB \<le> problem_plan_bound PROB \<and> problem_plan_bound PROB \<le> RD PROB
[PROOF STEP]
using assms sublistD_bounds_D RD_bounds_sublistD
[PROOF STATE]
proof (prove)
using this:
finite PROB
finite ?PROB \<Longrightarrow> problem_plan_bound_charles ?PROB \<le> problem_plan_bound ?PROB
finite ?Pi \<Longrightarrow> problem_plan_bound ?Pi \<le> RD ?Pi

goal (1 subgoal):
 1. problem_plan_bound_charles PROB \<le> problem_plan_bound PROB \<and> problem_plan_bound PROB \<le> RD PROB
[PROOF STEP]
by auto


\<comment> \<open>NOTE type of `PROB` had to be fixed for MP of lemmas.\<close>