rename coq proofs to simplified lemma bits_and_bounds