b : Bool
n : ℕ
h : bit b n ≠ 0
⊢ binaryRec 0 (fun x x => succ) (bit b n) = succ (binaryRec 0 (fun x x => succ) n)
b : Bool
n : ℕ
h : bit b n ≠ 0
⊢ size (bit b n) = succ (size n)
rw [size]
b : Bool
n : ℕ
h : bit b n ≠ 0
⊢ succ (binaryRec 0 (fun x x => succ) (div2 (bit b n))) = succ (binaryRec 0 (fun x x => succ) n)
b : Bool
n : ℕ
h : bit b n ≠ 0
⊢ binaryRec 0 (fun x x => succ) (bit b n) = succ (binaryRec 0 (fun x x => succ) n)
conv =>
  lhs
  rw [binaryRec]
  simp [h]
no goals
b : Bool
n : ℕ
h : bit b n ≠ 0
⊢ succ (binaryRec 0 (fun x x => succ) (div2 (bit b n))) = succ (binaryRec 0 (fun x x => succ) n)
rw [div2_bit]