Function lemma_u128_and_zero 

pub proof fn lemma_u128_and_zero(x: u128)

ensures

0u128 & x == 0u128,

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