Function lemma_u32_and_zero 

pub proof fn lemma_u32_and_zero(x: u32)

ensures

0u32 & x == 0u32,

AND-ing the zero word with any word is zero.