[STATEMENT]
lemma real_of_nat_div4: "real (n div x) \<le> real n / real x" for n x :: nat
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real (n div x) \<le> real n / real x
[PROOF STEP]
using real_of_nat_div2 [of n x]
[PROOF STATE]
proof (prove)
using this:
0 \<le> real n / real x - real (n div x)

goal (1 subgoal):
 1. real (n div x) \<le> real n / real x
[PROOF STEP]
by simp