add coq lemma bits_and_bounds and use it

to prove a postcondition (the lemma itself is admitted)
reome old proofs
use bits_and_bounds for proof of another obligation