cases h with
| refl => cases Nat.add_left_cancel hn
| node_left _ h =>
  cases hn; apply absurd h.le
  rewrite [Nat.two_mul (2*i+1), Nat.succ_le_succ_iff, Nat.add_le_add_iff_left (m:=0)]
  exact (2*i).not_lt_zero
| node_right _ h =>
  cases hn; apply absurd h.le
  rewrite [Nat.two_mul (2*i+1), Nat.add_le_add_iff_right]
  conv => rhs; rhs; change 2*i+0
  rewrite [Nat.add_assoc, Nat.add_le_add_iff_left, Nat.add_comm 1]
  exact (2*i+1).not_lt_zero
i n : Nat
hn : 2 * i + 1 = n
h : Descendant n (2 * i + 2)
⊢ False
no goals