Function lemma_usize_and_zero 

pub proof fn lemma_usize_and_zero(x: usize)

ensures

0usize & x == 0usize,

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