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