[STATEMENT]
lemma dual_ccpo_mono_simp: "monotone (\<ge>) (\<ge>) f \<longleftrightarrow> mono f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. monotone (\<lambda>x y. y \<le> x) (\<lambda>x y. y \<le> x) f = mono f
[PROOF STEP]
unfolding monotone_def mono_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>x y. y \<le> x \<longrightarrow> f y \<le> f x) = (\<forall>x y. x \<le> y \<longrightarrow> f x \<le> f y)
[PROOF STEP]
by auto