pub broadcast proof fn lemma_u64_shl_is_mul(x: u64, shift: u64)Expand description
requires
0 <= shift < <u64>::BITS,x * pow2(shift as nat) <= <u64>::MAX,#[trigger] (x << shift) == x * pow2(shift as nat),Proof that for x and n of type u64 , shifting x left by n is equivalent to multiplication of x by 2^n (provided no overflow).