# HG changeset patch
# User wenzelm
# Date 1475313240 -7200
# Node ID c1a481bb82d33fcd8df5bc969d25bcc157403fbe
# Parent  6728b5007ad026a5d48747a3157b898b029d3e7a
added lemma;

diff -r 6728b5007ad0 -r c1a481bb82d3 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>