Function lemma_usize_allones_bit_it_set 

pub broadcast proof fn lemma_usize_allones_bit_it_set(k: int)

requires

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

ensures

usize_bit_is_set(!0usize, k),

Every bit of the all-ones word is set.