pub broadcast proof fn lemma_pow2_increases(e1: nat, e2: nat)Expand description
requires
e1 <= e2,#[trigger] pow2(e1) <= #[trigger] pow2(e2),pub broadcast proof fn lemma_pow2_increases(e1: nat, e2: nat)e1 <= e2,#[trigger] pow2(e1) <= #[trigger] pow2(e2),