pub broadcast proof fn lemma_pow2_subtracts(e1: nat, e2: nat)Expand description
requires
e1 <= e2,#[trigger] pow2((e2 - e1) as nat) == pow2(e2) / pow2(e1) > 0,Proof that, as long as e1 <= e2, 2^(e2 - e1) is equivalent to 2^e2 / 2^e1.