have : h₁.rank = min h₁.rank (h₂.rank - 1) := by
  have hle : h₁.rank ≤ (h₂.rank - 1) := by
    apply Nat.le_pred_of_lt hlt₂
  have : min h₁.rank (h₂.rank - 1) = h₁.rank := by
    apply min_eq_left hle
  rw[this]
case inl.a.cons
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
hys : IsHeapForest' ry (h₂ :: t₂)
hlt₂ : h₁.rank < h₂.rank
bt : IsBinTree h₁
hlt : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
⊢ IsHeapForest' h₁.rank (mergeNodes le t₁ (h₂ :: t₂))
case inl.a.cons
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
hys : IsHeapForest' ry (h₂ :: t₂)
hlt₂ : h₁.rank < h₂.rank
bt : IsBinTree h₁
hlt : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
this : h₁.rank = min h₁.rank (h₂.rank - 1)
⊢ IsHeapForest' h₁.rank (mergeNodes le t₁ (h₂ :: t₂))