pub broadcast proof fn lemma_usize_pow2_shl_is_pow2(x: usize, shift: usize)Expand description
requires
0 <= shift < usize::BITS,is_pow2(x as int),x * pow2(shift as nat) <= usize::MAX,#[trigger] is_pow2((x << shift) as int),