induction hjk with
| refl => exact hik
| node_left j _ IH =>
  specialize IH (Nat.le_trans hij (Nat.le_of_lt <| (lt_child_left j)))
  have := IH.ascend_right_parent (Nat.lt_of_le_of_lt hij (lt_child_left j))
  rewrite [Nat.succ_sub_one, Nat.mul_div_right _ (by decide)] at this
  exact this
| node_right j _ IH =>
  specialize IH (Nat.le_trans hij (Nat.le_of_lt <| (lt_child_right j)))
  have := IH.ascend_right_parent (Nat.lt_of_le_of_lt hij (lt_child_right j))
  conv at this =>
    rhs; rw [Nat.succ_sub_one, Nat.add_comm, Nat.add_mul_div_left 1 j (by decide)]
    change 0 + j; rw [Nat.zero_add]
  exact this
i j k : Nat
hij : i ≤ j
hik : Descendant i k
hjk : Descendant j k
⊢ Descendant i j
no goals