refactor(data/nat/fib): use `nat.iterate` (#10489)
The main drawback of the new definition is that `fib (n + 2) = fib n + fib (n + 1)` is no longer `rfl` but I think that we should have one API for iterates.
See discussion at https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.60nat.2Eiterate.60.20vs.20.60stream.2Eiterate.60
