lemma_pow2_is_pow2

vstd_extra::external::ilog2

Function lemma_pow2_is_pow2 

Source 
pub broadcast proof fn lemma_pow2_is_pow2(e: nat)
Expand description
ensures
#[trigger] is_pow2(pow2(e) as int),