[STATEMENT]
lemma dgrad_set_subset:
  assumes "m \<le> n"
  shows "dgrad_set d m \<subseteq> dgrad_set d n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dgrad_set d m \<subseteq> dgrad_set d n
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
m \<le> n

goal (1 subgoal):
 1. dgrad_set d m \<subseteq> dgrad_set d n
[PROOF STEP]
by (auto simp: dgrad_set_def)