lemma_pow2_log2

vstd_extra::external::ilog2

Function lemma_pow2_log2 

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