Function vstd::bits::lemma_u64_pow2_no_overflow

source · 
pub broadcast proof fn lemma_u64_pow2_no_overflow(n: nat)
Expand description
requires
0 <= n < <u64>::BITS,
ensures
#[trigger] pow2(n) <= <u64>::MAX,

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