refactor(data/nat/fib): explicitly state fibonacci sequence is monoto…

…ne (#5776)

https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/fib_mono




Co-authored-by: Julian-Kuelshammer <68201724+Julian-Kuelshammer@users.noreply.github.com>

src/data/nat/fib.lean

@@ -79,8 +79,8 @@ end
 
 lemma fib_le_fib_succ {n : ℕ} : fib n ≤ fib (n + 1) := by { cases n; simp [fib_succ_succ] }
 
-lemma fib_mono {n m : ℕ} (n_le_m : n ≤ m) : fib n ≤ fib m :=
-by { induction n_le_m with m n_le_m IH, { refl }, { exact (le_trans IH fib_le_fib_succ) }}
+@[mono] lemma fib_mono : monotone fib :=
+monotone_of_monotone_nat $ λ _, fib_le_fib_succ
 
 lemma le_fib_self {n : ℕ} (five_le_n : 5 ≤ n) : n ≤ fib n :=
 begin