--- a/src/HOL/Nat.thy Mon May 04 18:49:51 2015 +0200
+++ b/src/HOL/Nat.thy Tue May 05 14:52:17 2015 +0200
@@ -1877,6 +1877,11 @@
shows "mono Q \<Longrightarrow> mono (\<lambda>i. (Q ^^ i) \<bottom>)"
by (auto intro!: funpow_decreasing simp: mono_def)
+lemma antimono_funpow:
+ fixes Q :: "('i \<Rightarrow> 'a::{lattice, order_top}) \<Rightarrow> ('i \<Rightarrow> 'a)"
+ shows "mono Q \<Longrightarrow> antimono (\<lambda>i. (Q ^^ i) \<top>)"
+ by (auto intro!: funpow_increasing simp: antimono_def)
+
subsection {* The divides relation on @{typ nat} *}
lemma dvd_1_left [iff]: "Suc 0 dvd k"