have := IH.ascend_right_parent (Nat.lt_of_le_of_lt hij (lt_child_right j))
case node_right
i j✝ k : Nat
hik : Descendant i k
j : Nat
h✝ : Descendant (2 * j + 2) k
hij : i ≤ j
IH : Descendant i (2 * j + 2)
⊢ Descendant i j
case node_right
i j✝ k : Nat
hik : Descendant i k
j : Nat
h✝ : Descendant (2 * j + 2) k
hij : i ≤ j
IH : Descendant i (2 * j + 2)
this : Descendant i ((2 * j + 2 - 1) / 2)
⊢ Descendant i j