Further lemmas about Nat.isPowerOfTwo, with the convenience of having bitwise lemmas available.

theorem Nat.and_sub_one_testBit_log2 {n : Nat} (h : n ≠ 0) (hpow2 : ¬n.isPowerOfTwo) : (n &&& n - 1).testBit n.log2 = true

theorem Nat.and_sub_one_eq_zero_iff_isPowerOfTwo {n : Nat} (h : n ≠ 0) : n &&& n - 1 = 0 ↔ n.isPowerOfTwo

theorem Nat.ne_zero_and_sub_one_eq_zero_iff_isPowerOfTwo {n : Nat} : n ≠ 0 ∧ n &&& n - 1 = 0 ↔ n.isPowerOfTwo

@[instance_reducible, inline]

instance Nat.instDecidableIsPowerOfTwo {n : Nat} : Decidable n.isPowerOfTwo