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