# HG changeset patch
# User nipkow
# Date 1609174346 -3600
# Node ID 8644c1efbda2c03c213c24a2db5fd2c5075e5530
# Parent  2d7060a3ea11917a6fb78a55f20282a61423ddce
added lemma

diff -r 2d7060a3ea11 -r 8644c1efbda2 src/HOL/Analysis/Harmonic_Numbers.thy
--- a/src/HOL/Analysis/Harmonic_Numbers.thy	Sun Dec 27 17:53:08 2020 +0100
+++ b/src/HOL/Analysis/Harmonic_Numbers.thy	Mon Dec 28 17:52:26 2020 +0100
@@ -33,6 +33,9 @@
 lemma harm_pos: "n > 0 \<Longrightarrow> harm n > (0 :: 'a :: {real_normed_field,linordered_field})"
   unfolding harm_def by (intro sum_pos) simp_all
 
+lemma harm_mono: "m \<le> n \<Longrightarrow> harm m \<le> (harm n :: 'a :: {real_normed_field,linordered_field})"
+by(simp add: harm_def sum_mono2)
+
 lemma of_real_harm: "of_real (harm n) = harm n"
   unfolding harm_def by simp