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)
k : Nat
⊢ k < log2' (2 * zero) ↔ 2 ^ k < succ zero
no goals