theory Real
imports RComplete RealVector
begin
lemma field_le_epsilon:
fixes x y :: "'a:: {number_ring,division_by_zero,linordered_field}"
assumes e: "(!!e. 0 < e ==> x \<le> y + e)"
shows "x \<le> y"
proof (rule ccontr)
assume xy: "\<not> x \<le> y"
hence "(x-y)/2 > 0"
by simp
hence "x \<le> y + (x - y) / 2"
by (rule e [of "(x-y)/2"])
also have "... = (x - y + 2*y)/2"
by (simp add: diff_divide_distrib)
also have "... = (x + y) / 2"
by simp
also have "... < x" using xy
by simp
finally have "x<x" .
thus False
by simp
qed
end