pub broadcast proof fn is_pow2_equiv(n: int)
is_pow2(n) <==> is_pow2_exists(n),
Proof that the recursive and existential specifications for is_pow2 are equivalent.
is_pow2