apply absurd h.le
case node_left.refl
i : Nat
h : Descendant (2 * (2 * i + 1) + 1) (2 * i + 2)
a✝ : 2 * i + 1 = 2 * (2 * i + 1) + 1 → HEq (_ : Descendant (2 * i + 1) (2 * i + 2)) h → False
⊢ False
case node_left.refl
i : Nat
h : Descendant (2 * (2 * i + 1) + 1) (2 * i + 2)
a✝ : 2 * i + 1 = 2 * (2 * i + 1) + 1 → HEq (_ : Descendant (2 * i + 1) (2 * i + 2)) h → False
⊢ ¬2 * (2 * i + 1) + 1 ≤ 2 * i + 2