@[simp]

theorem Nat.not_isPowerOfTwo_zero : ¬isPowerOfTwo 0

theorem Nat.nextPowerOfTwo_eq_iff {n m : Nat} : n.nextPowerOfTwo = m ↔ n ≤ m ∧ m.isPowerOfTwo ∧ ∀ (k : Nat), n ≤ k → k.isPowerOfTwo → m ≤ k

@[simp]

theorem Nat.le_nextPowerOfTwo (n : Nat) : n ≤ n.nextPowerOfTwo

theorem Nat.nextPowerOfTwo_le {n m : Nat} (hn : n ≤ m) (hm : m.isPowerOfTwo) : n.nextPowerOfTwo ≤ m

theorem Nat.nextPowerOfTwo_eq_self {n : Nat} (h : n.isPowerOfTwo) : n.nextPowerOfTwo = n

@[simp]

theorem Nat.isPowerOfTwo_nextPowerOfTwo (n : Nat) : n.nextPowerOfTwo.isPowerOfTwo