Function lemma_usize_clearbit_bit_unchanged 

pub broadcast proof fn lemma_usize_clearbit_bit_unchanged(word: usize, b: int, b2: int)

requires

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

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

b != b2,

ensures

usize_bit_is_set(word & (!(1usize << (b as usize))), b2) == usize_bit_is_set(word, b2),

Clearing bit b leaves a different in-range bit b2 unchanged.