Function lemma_usize_masked_bit_keep 

pub broadcast proof fn lemma_usize_masked_bit_keep(word: usize, mask: usize, k: int, b: int)

requires

0 < k <= usize::BITS as int,

0 <= b < k,

mask == (1usize << (k as usize)) - 1usize,

ensures

usize_bit_is_set(word & mask, b) == usize_bit_is_set(word, b),

Masking with the low-k-bits mask keeps every bit below k unchanged.