pub broadcast proof fn lemma_pow2_unfold(e: nat)
e > 0,
#[trigger] pow2(e) == 2 * pow2((e - 1) as nat),
Proof relating 2^e to 2^(e-1).