feat(data/nat/fib): add a strict monotonicity lemma.

With thanks to @b-mehta and @dwarn.

src/data/nat/fib.lean

@@ -82,6 +82,14 @@ lemma fib_le_fib_succ {n : ℕ} : fib n ≤ fib (n + 1) := by { cases n; simp [f
 @[mono] lemma fib_mono : monotone fib :=
 monotone_of_monotone_nat $ λ _, fib_le_fib_succ
 
+/-- If `2 ≤ n`, `fib` is strictly monotone. -/
+lemma fib_add_two_strict_mono : strict_mono (λ n, fib (n + 2)) := begin
+  apply strict_mono.nat,
+  intro n,
+  conv_rhs { rw fib_succ_succ, },
+  exact lt_add_of_pos_left _ (fib_pos succ_pos'),
+end
+
 lemma le_fib_self {n : ℕ} (five_le_n : 5 ≤ n) : n ≤ fib n :=
 begin
   induction five_le_n with n five_le_n IH,