Lemmas unifying `nat.bits` and `computability.encode_nat`

Stream: general

[Praneeth Kolichala]

Lean has nat.bits and nat.bitwise operators that allow bitwise operations. We also have https://github.com/leanprover-community/mathlib/blob/76a3b82dc0ae6c9a60a8714d74c6cf2b854cf17b/src/computability/encoding.lean which defines encode_nat which is literally equal to nat.bits. Do we want to unify these into one function? I'm finding it relatively difficult to work with nat.bits, because there don't seem to be a lot of lemmas about it, but it seems wasteful to have two functions doing the exact same thing.