specialize IH (Nat.le_trans hij (Nat.le_of_lt <| (lt_child_left j)))
case node_left
i j✝ k : Nat
hik : Descendant i k
j : Nat
h✝ : Descendant (2 * j + 1) k
IH : i ≤ 2 * j + 1 → Descendant i (2 * j + 1)
hij : i ≤ j
⊢ Descendant i j
case node_left
i j✝ k : Nat
hik : Descendant i k
j : Nat
h✝ : Descendant (2 * j + 1) k
hij : i ≤ j
IH : Descendant i (2 * j + 1)
⊢ Descendant i j