Theorem: Algdata.BinaryHeap.Descendant.ascendants_total (Algdata/Data/BinaryHeap/Index.lean)

State before:
i j k : Nat
hik : Descendant i k
hjk : Descendant j k
⊢ Descendant i j ∨ Descendant j i
Tactic:
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
State after:
no goals

State before:
case inl
i j k : Nat
hik : Descendant i k
hjk : Descendant j k
hlt : i < j
⊢ Descendant i j ∨ Descendant j i
Tactic:
exact Or.inl <| ascend_right (Nat.le_of_lt hlt) hik hjk
State after:
no goals

State before:
case inr
i j k : Nat
hik : Descendant i k
hjk : Descendant j k
hge : i ≥ j
⊢ Descendant i j ∨ Descendant j i
Tactic:
exact Or.inr <| ascend_right hge hjk hik
State after:
no goals