Function vstd::arithmetic::power2::lemma_pow2_adds

source · 
pub broadcast proof fn lemma_pow2_adds(e1: nat, e2: nat)
Expand description
ensures
#[trigger] pow2(e1 + e2) == pow2(e1) * pow2(e2),

Proof that 2^(e1 + e2) is equivalent to 2^e1 * 2^e2.