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),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)