vstd::arithmetic::power2

Function lemma_pow2_pos

Source 
pub broadcast proof fn lemma_pow2_pos(e: nat)
Expand description
ensures
#[trigger] pow2(e) > 0,

Proof that 2 to the power of any natural number (specifically, e) is positive.