pub broadcast proof fn lemma_u64_set_bits_nonzero(w: u64)Expand description
ensures
(w != 0u64) == (1 <= u64_set_bits(w)),0 <= u64_set_bits(w) <= 64,A nonzero word has at least one set bit (and zero has none).