apply Nat.lt_of_succ_le this
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂✝ : List (BinTree α)
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝³ : h₂.rank ≤ h₁.rank
h✝² : h₁.rank ≤ h₂.rank
heq : h₁.rank = h₂.rank
a✝⁹ : IsBinTree h₁
a✝⁸ : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
a✝⁷ : IsBinTree h₂
a✝⁶ : ry < h₂.rank
hf₂ : IsHeapForest' h₂.rank t₂✝
t : BinTree α
ts : List (BinTree α)
a✝⁵ : h₂.rank < t.rank
a✝⁴ : IsBinTree t
a✝³ : IsHeapForest' t.rank ts
h✝¹ : h₁.rank + 1 = t.rank
t₂ : BinTree α
ts₂ : List (BinTree α)
a✝² : h₁.rank < t₂.rank
a✝¹ : IsBinTree t₂
a✝ : IsHeapForest' t₂.rank ts₂
heq₂ : h₁.rank + 1 = t₂.rank
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le (t₂ :: ts₂) (t :: ts))
h✝ : t₂.rank ≤ t.rank
hle : t₂.rank ≤ hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
h : True
ht₁ : IsHeapForest' h₁.rank (t₂ :: ts₂)
ht₂ : IsHeapForest' h₁.rank (t :: ts)
this : t₂.rank + 1 ≤ hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
⊢ t₂.rank < hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
no goals