pub open spec fn is_pow2_exists(n: int) -> bool
{ exists |i: nat| pow(2, i) == n }
Returns true if the given integer is a power of 2 (defined by existential quantification in terms of pow).
pow