Lemmas about Nat.nextPowerOfTwo

Do not simplify this file's header

The four parts of the header are coupled and each breaks the file differently if changed: module activates explicit-export mode; import all reaches Nat.nextPowerOfTwo.go, a private core auxiliary; the public imports re-export names appearing in the exported lemma signatures; and public lemma exports each lemma.

Rewriting go_ge/go_le to avoid .go is impossible: Nat.nextPowerOfTwo is opaque without it, and the only public spec (Nat.isPowerOfTwo_nextPowerOfTwo) does not pin the value. Lean core itself uses this same import all idiom for its own Init.Data.Nat.Power2.Lemmas, so the pattern is the intended one. In particular, do not replace this file with a 2 ^ Nat.clog 2 n workaround.

theorem isPowerOfTwo_iff_exists {n : ℕ} : n.isPowerOfTwo ↔ ∃ (k : ℕ), n = 2 ^ k

Destructuring bridge for core's Nat.isPowerOfTwo, which is a plain (unexposed) def unfolding to an existential. Inside a module file obtain/rcases cannot see through it, and core ships no iff-lemma; proving it here — where import all is already required — lets importers destructure it without needing import all themselves.

theorem nextPow2_nat_ge (n : ℕ) : n ≤ n.nextPowerOfTwo

theorem nextPow2_nat_le (n j : ℕ) (hn : n ≤ 2 ^ j) : n.nextPowerOfTwo ≤ 2 ^ j

theorem nextPowerOfTwo_eq_two_pow_clog (n : ℕ) : n.nextPowerOfTwo = 2 ^ Nat.clog 2 n