Skip to main content

lemma_pow256_succ

vest_lib::primitives::base256

Function lemma_pow256_succ 

Source 
pub proof fn lemma_pow256_succ(exp: nat)
Expand description
ensures
pow(256, exp + 1) == pow(256, exp) * 256,