. constructor
  . cases hxs
    rw[Nat.min_eq]
    split
    . assumption
    . rename_i nle
      simp at nle
      apply Nat.lt_trans nle
      assumption
  . cases hxs
    assumption
  . cases hxs with | cons hlt bt hf =>
      rename_i hlt₂
      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]
      rw [this]; clear this
      apply IsHeap_merge
      . assumption
      . apply IsHeapForest'_strengthen_pred
        . assumption
        . cases bt with | mk =>
            have hge : h₁.rank ≥ 0 := by
              cases h₁.rank
              . simp 
              . simp
            have hle : 0 ≤ h₁.rank := by
              apply hge
            have : 0 < h₂.rank := by
              apply lt_of_le_of_lt hle hlt₂
            assumption
case inl
α : 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 α)
hxs : IsHeapForest' rx (h₁ :: t₁)
hys : IsHeapForest' ry (h₂ :: t₂)
h✝ : h₁.rank < h₂.rank
⊢ IsHeapForest' (min rx ry) (h₁ :: mergeNodes le t₁ (h₂ :: t₂))

case inr
α : 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 α)
hxs : IsHeapForest' rx (h₁ :: t₁)
hys : IsHeapForest' ry (h₂ :: t₂)
h✝ : ¬h₁.rank < h₂.rank
⊢ IsHeapForest' (min rx ry)
    (if h₂.rank < h₁.rank then h₂ :: mergeNodes le t₂ (h₁ :: t₁)
    else
      let merged := combine le h₁ h₂;
      let r := merged.rank;
      if (r != hRank t₁) = true then
        if (r != hRank t₂) = true then merged :: mergeNodes le t₁ t₂ else mergeNodes le (merged :: t₁) t₂
      else if (r != hRank t₂) = true then mergeNodes le t₁ (merged :: t₂) else merged :: mergeNodes le t₁ t₂)
case inr
α : 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 α)
hxs : IsHeapForest' rx (h₁ :: t₁)
hys : IsHeapForest' ry (h₂ :: t₂)
h✝ : ¬h₁.rank < h₂.rank
⊢ IsHeapForest' (min rx ry)
    (if h₂.rank < h₁.rank then h₂ :: mergeNodes le t₂ (h₁ :: t₁)
    else
      let merged := combine le h₁ h₂;
      let r := merged.rank;
      if (r != hRank t₁) = true then
        if (r != hRank t₂) = true then merged :: mergeNodes le t₁ t₂ else mergeNodes le (merged :: t₁) t₂
      else if (r != hRank t₂) = true then mergeNodes le t₁ (merged :: t₂) else merged :: mergeNodes le t₁ t₂)