Function vstd::arithmetic::power::lemma_pow_positive

source · 
pub broadcast proof fn lemma_pow_positive(b: int, e: nat)
Expand description
requires
b > 0,
ensures
0 < #[trigger] pow(b, e),

Proof that taking the given positive integer b to the power of the given natural number n produces a positive result