cases Nat.eq_zero_or_pos i with
| inl hz => cases hz; exact .refl 0
| inr hpos =>
  specialize IH ((i-1)/2) (gt_parent hpos)
  exact .trans IH (.parent i)
case ind
i : Nat
IH : ∀ (m : Nat), m < i → Descendant 0 m
⊢ Descendant 0 i
no goals