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