theorem Nat.nextPowerOfTwo_dec {n power : Nat} (h₁ : power > 0) (h₂ : power < n) : n - power * 2 < n - power

def Nat.nextPowerOfTwo (n : Nat) : Nat

Returns the least power of two that's greater than or equal to n.

Examples:

• Nat.nextPowerOfTwo 0 = 1
• Nat.nextPowerOfTwo 1 = 1
• Nat.nextPowerOfTwo 2 = 2
• Nat.nextPowerOfTwo 3 = 4
• Nat.nextPowerOfTwo 5 = 8

Equations

• n.nextPowerOfTwo = Nat.nextPowerOfTwo.go✝ n 1 Nat.nextPowerOfTwo._proof_1✝

def Nat.isPowerOfTwo (n : Nat) : Prop

A natural number n is a power of two if there exists some k : Nat such that n = 2 ^ k.

Equations

• n.isPowerOfTwo = ∃ (k : Nat), n = 2 ^ k

theorem Nat.isPowerOfTwo_one : isPowerOfTwo 1

theorem Nat.isPowerOfTwo_mul_two_of_isPowerOfTwo {n : Nat} (h : n.isPowerOfTwo) : (n * 2).isPowerOfTwo

theorem Nat.pos_of_isPowerOfTwo {n : Nat} (h : n.isPowerOfTwo) : n > 0

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