cases Nat.lt_or_ge i j with
| inl hlt => exact Or.inl <| ascend_right (Nat.le_of_lt hlt) hik hjk
| inr hge => exact Or.inr <| ascend_right hge hjk hik
i j k : Nat
hik : Descendant i k
hjk : Descendant j k
⊢ Descendant i j ∨ Descendant j i
no goals