feat(data/nat/fib): add bit0/bit1 lemmas and fast_fib (#12444)
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`.





leanprover-community/mathlib,leanprover-community/mathlib