Function vstd::arithmetic::power::lemma_pow_division_inequality

source · 
pub proof fn lemma_pow_division_inequality(x: nat, b: nat, e1: nat, e2: nat)
Expand description
requires
b > 0,
e2 <= e1,
x < pow(b as int, e1),
ensures
pow(b as int, e2) > 0,
#[trigger] (x as int / pow(b as int, e2)) < #[trigger] pow(b as int, (e1 - e2) as nat),

Proof that if e2 <= e1 and x < pow(b, e1), then dividing x by pow(b, e2) produces a result less than pow(b, e1 - e2)