Polynomial-time bit access and unary-prefix parsing

Relate the existing Cobham bit reader and leading-true-run loop to ordinary list operations. These proofs include missing bits and unterminated unary prefixes.

theorem Complexity.bitOf_eq_getElem?_internal (bits : List Bool) (i : ℕ) : bitOf bits i = bits[i]?.getD false

theorem Complexity.runTrue_length_takeWhile_internal (bits : List Bool) : (runTrue bits bits.length).length = (List.takeWhile id bits).length