Skip to main content
lemma_pow128_succ
vest_
lib
In vest_
lib::
primitives::
base128
vest_lib
::
primitives
::
base128
Function
lemma_
pow128_
succ
Copy item path
Source
pub
proof
fn lemma_pow128_succ(exp: nat)
Expand description
ensures
pow(
128
, exp +
1
) == pow(
128
, exp) *
128
,