add lemma as assertion (for the time being)
add (unproven) Cdiv_bounds and use it for Bitstream_Read
use Cdiv_bounds for proof of Bitstream_Write