Function lemma_u128_shl_is_mul 

pub broadcast proof fn lemma_u128_shl_is_mul(x: u128, shift: u128)

requires

0 <= shift < <u128>::BITS,

x * pow2(shift as nat) <= <u128>::MAX,

ensures

#[trigger] (x << shift) == x * pow2(shift as nat),

Proof that for x and n of type u128 , shifting x left by n is equivalent to multiplication of x by 2^n (provided no overflow).