src/HOL/Inductive.thy

--- a/src/HOL/Inductive.thy	Fri Sep 30 17:12:50 2016 +0100
+++ b/src/HOL/Inductive.thy	Sat Oct 01 11:14:00 2016 +0200
@@ -158,6 +158,10 @@
   by (rule antisym) (simp_all add: gfp_upperbound gfp_unfold[symmetric])
 
 
+lemma lfp_le_gfp: "mono f \<Longrightarrow> lfp f \<le> gfp f"
+  by (iprover intro: gfp_upperbound lfp_lemma3)
+
+
 subsection \<open>Coinduction rules for greatest fixed points\<close>
 
 text \<open>Weak version.\<close>