pub proof fn lemma_log_nonnegative(base: int, pow: int)Expand description
requires
base > 1,0 <= pow,log(base, pow) >= 0,Proof that the integer logarithm is always nonnegative. Specifically,
log(base, pow) >= 0.