vstd::arithmetic::power2

Function lemma_pow2

Source 
pub broadcast proof fn lemma_pow2(e: nat)
Expand description
ensures
#[trigger] pow2(e) == pow(2, e) as int,

Proof that pow2(e) is equivalent to pow(2, e).