Mission-critical systems depend on bit arithmetic algorithms for specific and efficient calculations. Providing formal guarantees for these algorithms is difficult because it requires reasoning about obscure facts of binary arithmetic. These obscure properties often build off one another, suggesting that a library of solved algorithms would provide the necessary logic to prove the correctness of more complex algorithms. This paper presents proofs of correctness for 14 unique bit arithmetic algorithms at the raw (stripped) machine code level and a supporting theory library covering subtle properties of binary arithmetic within the Rocq interactive theorem-proving environment.