[STATEMENT]
lemma ex_dist_less:
  assumes "c \<in> carrier Q\<^sub>p"
  shows "\<exists> a \<in> carrier Q\<^sub>p. val (a \<ominus> c) < \<beta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>a\<in>carrier Q\<^sub>p. val (a \<ominus> c) < \<beta>
[PROOF STEP]
using ex_val_less[of \<beta>] assms
[PROOF STATE]
proof (prove)
using this:
\<exists>\<alpha>. \<alpha> < \<beta>
c \<in> carrier Q\<^sub>p

goal (1 subgoal):
 1. \<exists>a\<in>carrier Q\<^sub>p. val (a \<ominus> c) < \<beta>
[PROOF STEP]
by (metis dist_nonempty' ex_val_less)