rw [this, this]
k n : Nat
this : ∀ (a b : Nat), (a < b + 1) = (a ≤ b)
⊢ k < log2' (succ n) + 1 ↔ 2 ^ k < succ (succ n)
k n : Nat
this : ∀ (a b : Nat), (a < b + 1) = (a ≤ b)
⊢ k ≤ log2' (succ n) ↔ 2 ^ k ≤ n + 1