src/HOL/Orderings.thy

--- a/src/HOL/Orderings.thy	Thu Nov 13 14:40:06 2014 +0100
+++ b/src/HOL/Orderings.thy	Thu Nov 13 17:19:52 2014 +0100
@@ -1524,6 +1524,9 @@
 lemma le_funD: "f \<le> g \<Longrightarrow> f x \<le> g x"
   by (rule le_funE)
 
+lemma mono_compose: "mono Q \<Longrightarrow> mono (\<lambda>i x. Q i (f x))"
+  unfolding mono_def le_fun_def by auto
+
 
 subsection {* Order on unary and binary predicates *}