vstd::arithmetic::power

Function lemma0_pow

Source 
pub broadcast proof fn lemma0_pow(e: nat)
Expand description
requires
e > 0,
ensures
#[trigger] pow(0, e) == 0,

Proof that 0 to the power of the given positive integer e is 0.