specialize IH ((i-1)/2) (gt_parent hpos)
case ind.inr
i : Nat
IH : ∀ (m : Nat), m < i → Descendant 0 m
hpos : i > 0
⊢ Descendant 0 i
case ind.inr
i : Nat
hpos : i > 0
IH : Descendant 0 ((i - 1) / 2)
⊢ Descendant 0 i