rw[Nat.not_beq_eq_true_eq] at hneq₂
α : 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
ht₁ : IsHeapForest' h₁.rank t₁
a✝³ : IsBinTree h₂
a✝² : ry < h₂.rank
ht₂ : IsHeapForest' h₂.rank t₂
hneq : (h₁.rank + 1 != hRank []) = true
bt : BinTree α
ts✝ : List (BinTree α)
hlt : h₁.rank < bt.rank
a✝¹ : IsBinTree bt
a✝ : IsHeapForest' bt.rank ts✝
hneq₂ : (!h₁.rank + 1 == bt.rank) = true
ih : IsHeapForest' (min h₁.rank h₂.rank) (bt :: ts✝)
h : ¬([] = [] ∧ bt :: ts✝ = [])
h✝ min_le : hRank [] ≤ bt.rank
⊢ h₁.rank + 1 < bt.rank
α : 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
ht₁ : IsHeapForest' h₁.rank t₁
a✝³ : IsBinTree h₂
a✝² : ry < h₂.rank
ht₂ : IsHeapForest' h₂.rank t₂
hneq : (h₁.rank + 1 != hRank []) = true
bt : BinTree α
ts✝ : List (BinTree α)
hlt : h₁.rank < bt.rank
a✝¹ : IsBinTree bt
a✝ : IsHeapForest' bt.rank ts✝
hneq₂ : ¬h₁.rank + 1 = bt.rank
ih : IsHeapForest' (min h₁.rank h₂.rank) (bt :: ts✝)
h : ¬([] = [] ∧ bt :: ts✝ = [])
h✝ min_le : hRank [] ≤ bt.rank
⊢ h₁.rank + 1 < bt.rank