[STATEMENT]
lemma ceiling_le_numeral [simp]: "\<lceil>x\<rceil> \<le> numeral v \<longleftrightarrow> x \<le> numeral v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lceil>x\<rceil> \<le> numeral v) = (x \<le> numeral v)
[PROOF STEP]
by (simp add: ceiling_le_iff)