[STATEMENT]
lemma pfp_pfp: assumes "pfp f x0 = Some x" shows "f x \<le> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f x \<le> x
[PROOF STEP]
using while_option_stop[OF assms[simplified pfp_def]]
[PROOF STATE]
proof (prove)
using this:
\<not> \<not> f x \<le> x

goal (1 subgoal):
 1. f x \<le> x
[PROOF STEP]
by simp