[STATEMENT]
lemma floor_le_one [simp]: "\<lfloor>x\<rfloor> \<le> 1 \<longleftrightarrow> x < 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lfloor>x\<rfloor> \<le> 1) = (x < (2::'a))
[PROOF STEP]
by (simp add: floor_le_iff)