[STATEMENT]
lemma nat_less_real_le: "n < m \<longleftrightarrow> real n + 1 \<le> real m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (n < m) = (real n + 1 \<le> real m)
[PROOF STEP]
by (metis discrete of_nat_1 of_nat_add of_nat_le_iff)