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

State before:
i : Nat
⊢ ¬Descendant (2 * i + 2) (2 * i + 1)
Tactic:
intro h
State after:
i : Nat
h : Descendant (2 * i + 2) (2 * i + 1)
⊢ False

State before:
i : Nat
h : Descendant (2 * i + 2) (2 * i + 1)
⊢ False
Tactic:
apply absurd h.le
State after:
i : Nat
h : Descendant (2 * i + 2) (2 * i + 1)
⊢ ¬2 * i + 2 ≤ 2 * i + 1

State before:
i : Nat
h : Descendant (2 * i + 2) (2 * i + 1)
⊢ ¬2 * i + 2 ≤ 2 * i + 1
Tactic:
rewrite [Nat.add_le_add_iff_left]
State after:
i : Nat
h : Descendant (2 * i + 2) (2 * i + 1)
⊢ ¬2 ≤ 1

State before:
i : Nat
h : Descendant (2 * i + 2) (2 * i + 1)
⊢ ¬2 ≤ 1
Tactic:
decide
State after:
no goals