added lemmas

--- 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>