cases i with
| zero => exact .refl 0
| succ i =>
  rewrite [Nat.succ_sub_one, Nat.succ_eq_add_one]
  conv => rhs; rewrite [← Nat.div_add_mod i 2]
  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 _
i : Nat
⊢ Descendant ((i - 1) / 2) i
no goals