lemma_usize_pow2_no_overflow

vstd::bits

Function lemma_usize_pow2_no_overflow 

Source 
pub broadcast proof fn lemma_usize_pow2_no_overflow(n: nat)
Expand description
requires
0 <= n < <usize>::BITS,
ensures
0 < #[trigger] pow2(n) < <usize>::MAX,

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