refactor(data/nat/fib): simplify proof of fib_succ_succ (#2443)
By tweaking some of the lemmas, I managed to shorten `fib_succ_succ` from 7 complicated lines to a single call to `simp`.
An alternative expression would be:
```lean
unfold fib,
repeat { rw fib_aux_stream_succ },
unfold fib_aux_step,
```
I can change to that if you think the `simp` is too pithy.
