case succ n =>
  rw [log2'_mul2]
  have : ∀ (a b : Nat), (a < b+1) = (a ≤ b) :=
    λ a b => propext ⟨Nat.le_of_lt_succ, Nat.lt_succ_of_le⟩
  rw [this, this]
  exact le_log2'_iff_pow2_le n.zero_lt_succ
k n : Nat
⊢ k < log2' (2 * succ n) ↔ 2 ^ k < succ (succ n)
no goals