Function vstd::arithmetic::power2::lemma_pow2_strictly_increases

source · 
pub broadcast proof fn lemma_pow2_strictly_increases(e1: nat, e2: nat)
Expand description
requires
e1 < e2,
ensures
#[trigger] pow2(e1) < #[trigger] pow2(e2),

Proof that if e1 < e2 then 2^e1 < 2^e2.