have : ∀ (a b : Nat), (a < b+1) = (a ≤ b) :=
  λ a b => propext ⟨Nat.le_of_lt_succ, Nat.lt_succ_of_le⟩
k n : Nat
⊢ 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) + 1 ↔ 2 ^ k < succ (succ n)