Function vstd::arithmetic::power2::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)