Function lemma_u32_masked_bit_clear 

pub broadcast proof fn lemma_u32_masked_bit_clear(word: u32, mask: u32, k: int, b: int)

requires

0 <= k <= 32,

k <= b < 32,

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

ensures

!u32_bit_is_set(word & mask, b),

Masking with the low-k-bits mask clears every bit at or above k.