Function lemma_usize_unit_le_shl 

pub broadcast proof fn lemma_usize_unit_le_shl(k: int)

requires

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

ensures

1usize <= (1usize << (k as usize)),

An in-range unit shift is at least 1, so (1 << k) - 1 cannot underflow.