[STATEMENT]
lemma real_arch_simple: "\<exists>n. x \<le> of_nat n"
  for x :: "'a::archimedean_field"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>n. x \<le> of_nat n
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>n. x \<le> of_nat n
[PROOF STEP]
obtain n where "x < of_nat n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>n. x < of_nat n \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using reals_Archimedean2
[PROOF STATE]
proof (prove)
using this:
\<exists>n. ?x < of_nat n

goal (1 subgoal):
 1. (\<And>n. x < of_nat n \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
x < of_nat n

goal (1 subgoal):
 1. \<exists>n. x \<le> of_nat n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x < of_nat n
[PROOF STEP]
have "x \<le> of_nat n"
[PROOF STATE]
proof (prove)
using this:
x < of_nat n

goal (1 subgoal):
 1. x \<le> of_nat n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x \<le> of_nat n

goal (1 subgoal):
 1. \<exists>n. x \<le> of_nat n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<le> of_nat n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<le> of_nat n

goal (1 subgoal):
 1. \<exists>n. x \<le> of_nat n
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<exists>n. x \<le> of_nat n

goal:
No subgoals!
[PROOF STEP]
qed