# HG changeset patch
# User nipkow
# Date 1588023555 -7200
# Node ID 62b17adad0cca1e6966eea583255c798f798a4d0
# Parent  6fd70ed181996d7b0947384a29227ab74eb728e8
added lemmas

diff -r 6fd70ed18199 -r 62b17adad0cc src/HOL/Number_Theory/Fib.thy
--- a/src/HOL/Number_Theory/Fib.thy	Mon Apr 27 16:18:51 2020 +0000
+++ b/src/HOL/Number_Theory/Fib.thy	Mon Apr 27 23:39:15 2020 +0200
@@ -37,6 +37,11 @@
 lemma fib_neq_0_nat: "n > 0 \<Longrightarrow> fib n > 0"
   by (induct n rule: fib.induct) auto
 
+lemma fib_Suc_mono: "fib m \<le> fib (Suc m)"
+by(induction m) auto
+
+lemma fib_mono: "m \<le> n \<Longrightarrow> fib m \<le> fib n"
+by (simp add: fib_Suc_mono lift_Suc_mono_le)
 
 subsection \<open>More efficient code\<close>