Function lemma_u128_pow2_no_overflow 

pub broadcast proof fn lemma_u128_pow2_no_overflow(n: nat)

requires

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

ensures

0 < #[trigger] pow2(n) < <u128>::MAX,

Proof that 2^n does not overflow u128 for an exponent n.