cases i.mod_two_eq_zero_or_one with
| inl hi_even =>
  rewrite [hi_even, Nat.add_zero]; exact .child_left _
| inr hi_odd =>
  rewrite [hi_odd]; exact .child_right _
case succ
i : Nat
⊢ Descendant (i / 2) (2 * (i / 2) + i % 2 + 1)
no goals