case succ n =>
  dsimp [log2RU]; simp [log2RU]
  cases n
  case zero =>
    conv => lhs; rhs; reduce
    constructor
    . intro h; cases h
    . intro hlt1
      have : 2^k > 0 := Nat.pos_pow_of_pos k (by decide)
      exact absurd hlt1 (Nat.not_lt_of_le this)
  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 < log2RU (succ n) ↔ 2 ^ k < succ n
no goals