Function lemma_u8_clearbit_not_bit_is_set 

pub broadcast proof fn lemma_u8_clearbit_not_bit_is_set(word: u8, b: int)

requires

0 <= b < 8,

ensures

!u8_bit_is_set(word & (!(1u8 << (b as usize))), b),

Clearing bit b makes that bit clear.