Function vstd::arithmetic::logarithm::lemma_log_nonnegative

source · 
pub proof fn lemma_log_nonnegative(base: int, pow: int)
Expand description
requires
base > 1,
0 <= pow,
ensures
log(base, pow) >= 0,

Proof that the integer logarithm is always nonnegative. Specifically, log(base, pow) >= 0.