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

def Nat.nextPowerOfTwo (n : Nat) : Nat

Equations

• Nat.nextPowerOfTwo n = Nat.nextPowerOfTwo.go n 1 Nat.nextPowerOfTwo.proof_1

def Nat.nextPowerOfTwo.go (n : Nat) (power : Nat) (h : power > 0) : Nat

Equations

• Nat.nextPowerOfTwo.go n power h = if power < n then Nat.nextPowerOfTwo.go n (power * 2) (_ : power * 2 > 0) else power

def Nat.isPowerOfTwo (n : Nat) : Prop

Equations

• Nat.isPowerOfTwo n = ∃ k, n = 2 ^ k

theorem Nat.one_isPowerOfTwo : Nat.isPowerOfTwo 1

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

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

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

theorem Nat.isPowerOfTwo_nextPowerOfTwo.isPowerOfTwo_go (n : Nat) (power : Nat) (h₁ : power > 0) (h₂ : Nat.isPowerOfTwo power) : Nat.isPowerOfTwo (Nat.nextPowerOfTwo.go n power h₁)