rw [size_bit, bit_val, Nat.log_mul_add, Nat.succ_eq_add_one, Nat.add_sub_cancel, ← ih, Nat.sub_add_cancel]
case hi.succ
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) - 1 = log 2 (succ n✝)
⊢ size (bit b (succ n✝)) - 1 = log 2 (bit b (succ n✝))
case hi.succ
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) - 1 = log 2 (succ n✝)
⊢ 1 ≤ size (succ n✝)

case hi.succ.hb
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) - 1 = log 2 (succ n✝)
⊢ 1 < 2

case hi.succ.hn
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) - 1 = log 2 (succ n✝)
⊢ 1 ≤ succ n✝

case hi.succ.hc
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) - 1 = log 2 (succ n✝)
⊢ (bif b then 1 else 0) < 2

case hi.succ
n : ℕ
b : Bool
n✝ : ℕ
hb : succ n✝ = 0 → b = true
ih : size (succ n✝) - 1 = log 2 (succ n✝)
⊢ bit b (succ n✝) ≠ 0