Function vstd::arithmetic::logarithm::lemma_log_s

pub broadcast proof fn lemma_log_s(base: int, pow: int)

Expand description

requires

base > 1,

pow >= base,

ensures

pow / base >= 0,

log(base, pow) == 1 + log(base, pow / base),

Proof that since pow is greater than or equal to base, its logarithm in that base is 1 more than the logarithm of pow / base

Function vstd::arithmetic::logarithm::lemma_log_sCopy item path