simpa [← Nat.add_assoc, Nat.add_right_comm _ 1, ← Nat.two_mul] using e _
C : ℕ → Sort u
z : C 0
o : (n : ℕ) → C (2 * n + 1)
e : (n : ℕ) → C (2 * n + 2)
n✝ n : ℕ
hb : n + 1 = 0 → false = true
a✝ : bit false (n + 1) = n + 1 → C (bit false (n + 1))
⊢ C (bit false (n + 1))
no goals