assumption
case inr.inl.a.hys.a.cons.a.succ.h
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
hys : IsHeapForest' ry (h₂ :: t₂)
h✝¹ : ¬h₁.rank < h₂.rank
h✝ : h₂.rank < h₁.rank
heq : min h₂.rank (h₁.rank - 1) = h₂.rank
a✝² : IsBinTree h₁
a✝¹ : IsHeapForest' h₁.rank t₁
n✝ : ℕ
a✝ : Nat.succ n✝ < h₁.rank
⊢ ?inr.inl.a.hys.a.cons.a.succ.b < h₁.rank

case inr.inl.a.hys.a.cons.a.succ.b
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
hys : IsHeapForest' ry (h₂ :: t₂)
h✝¹ : ¬h₁.rank < h₂.rank
h✝ : h₂.rank < h₁.rank
heq : min h₂.rank (h₁.rank - 1) = h₂.rank
a✝² : IsBinTree h₁
a✝¹ : IsHeapForest' h₁.rank t₁
n✝ : ℕ
a✝ : Nat.succ n✝ < h₁.rank
⊢ ℕ
no goals