feat(data/nat/fib): add bit0/bit1 lemmas and fast_fib (#12444)
This provides lemmas that let `simp` calculate `fib` from the bit0/bit1 numeral representation. (This isn't intended to be for speed, although it does evaluate things reasonably quick.)
```lean
lemma foo : fib 64 = 10610209857723 :=
begin
norm_num [fib_bit0, fib_bit1, fib_bit0_succ, fib_bit1_succ],
end
```
These are then used to show that `fast_fib` computes `fib`.
