Function vstd::arithmetic::power2::lemma_pow2_unfold

source · 
pub broadcast proof fn lemma_pow2_unfold(e: nat)
Expand description
requires
e > 0,
ensures
#[trigger] pow2(e) == 2 * pow2((e - 1) as nat),

Proof relating 2^e to 2^(e-1).