rewrite [Nat.two_mul (2*i+1), Nat.add_le_add_iff_right]
case node_right.refl
i : Nat
h : Descendant (2 * (2 * i + 1) + 2) (2 * i + 2)
a✝ : 2 * i + 1 = 2 * (2 * i + 1) + 2 → HEq (_ : Descendant (2 * i + 1) (2 * i + 2)) h → False
⊢ ¬2 * (2 * i + 1) + 2 ≤ 2 * i + 2
case node_right.refl
i : Nat
h : Descendant (2 * (2 * i + 1) + 2) (2 * i + 2)
a✝ : 2 * i + 1 = 2 * (2 * i + 1) + 2 → HEq (_ : Descendant (2 * i + 1) (2 * i + 2)) h → False
⊢ ¬2 * i + 1 + (2 * i + 1) ≤ 2 * i