add coq lemma bits_and_bounds and use it

to prove a postcondition (the lemma itself is admitted)