rewrite [Nat.succ_sub_one, Nat.mul_div_right _ (by decide)] at IH
case node_left
i j i' : Nat
h✝ : Descendant (2 * i' + 1) j
IH : Descendant ((2 * i' + 1 - 1) / 2) ((j - 1) / 2)
⊢ Descendant ((i' - 1) / 2) ((j - 1) / 2)
case node_left
i j i' : Nat
h✝ : Descendant (2 * i' + 1) j
IH : Descendant i' ((j - 1) / 2)
⊢ Descendant ((i' - 1) / 2) ((j - 1) / 2)