induction h with
| refl => exact .refl _
| node_left i' _ IH =>
  rewrite [Nat.succ_sub_one, Nat.mul_div_right _ (by decide)] at IH
  exact .trans (.parent i') IH
| node_right i' _ IH =>
  rewrite [Nat.succ_sub_one, Nat.add_comm, Nat.add_mul_div_left _ _ (by decide)] at IH
  conv at IH =>
    lhs; change 0 + i'; rewrite [Nat.zero_add]
  exact .trans (.parent i') IH
i j : Nat
h : Descendant i j
⊢ Descendant ((i - 1) / 2) ((j - 1) / 2)
no goals