[Merged by Bors] - feat(data/nat/fib): add a strict monotonicity lemma.

[Julian]

Prove strict monotonicity of fib (n + 2).

With thanks to @b-mehta and @dwarn.

---

I suspect it's highly likely I didn't name the lemma appropriately (or that there are other suggestions for improving things) which are of course very welcome.

[benjamindavidson]

Thanks! I don't know whether or not this lemma ought to be labeled with @[mono].

[Julian]

Lean made fun of me with quite an interesting error message when I tried adding it, so I figured the answer was "no". Specifically, it quizzically emits:

oh? strict_mono.{0 0} nat nat nat.has_lt nat.has_lt (fun (n : nat), (nat.fib (has_add.add.{0} nat nat.has_add n (bit0.{0} nat nat.has_add (has_one.one.{0} nat nat.has_one)))))

and yes with the oh? part of the error message :D

[kim-em]

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests