by
  intro α
  have earlier_count_le (b : List (α × Nat))
      (hs : b.Pairwise (fun x y => x.2 ≤ y.2))
      (j : Nat) (hj : j < b.length) :
      (b.filter fun r => r.2 < b[j].2).length ≤ j := by
    induction b generalizing j with
    | nil => simp at hj
    | cons r rs ih =>
      have ht := hs.of_cons
      have hrel := (List.pairwise_cons.mp hs).1
      cases j with
      | zero =>
        have hf : (rs.filter fun x => x.2 < r.2) = [] := by
          apply List.filter_eq_nil_iff.mpr
          intro x hx
          have hh := hrel x hx
          simp only [decide_eq_true_eq]
          omega
        simp [hf]
      | succ j =>
        have hj' : j < rs.length := by simp only [List.length_cons] at hj; omega
        have hh := ih ht j hj'
        simp only [List.getElem_cons_succ, List.filter_cons]
        split
        · change (rs.filter fun x => x.2 < rs[j].2).length + 1 ≤ j + 1
          omega
        · change (rs.filter fun x => x.2 < rs[j].2).length ≤ j + 1
          omega
  
  have gap_getElem (b : List (α × Nat))
      (hs : b.Pairwise (fun x y => x.2 ≤ y.2))
      (j : Nat) (hj : j < b.length) :
      (b.filter fun r => r.2 == b[j].2)[j - (b.filter fun r => r.2 < b[j].2).length]? = some b[j] := by
    induction b generalizing j with
    | nil => simp at hj
    | cons r rs ih =>
      have ht := hs.of_cons
      have hrel := (List.pairwise_cons.mp hs).1
      cases j with
      | zero =>
        have hf : (rs.filter fun x => x.2 < r.2) = [] := by
          apply List.filter_eq_nil_iff.mpr
          intro x hx
          have hh := hrel x hx
          simp only [decide_eq_true_eq]
          omega
        simp [hf]
      | succ j =>
        have hj' : j < rs.length := by simp only [List.length_cons] at hj; omega
        have hr := hrel rs[j] (List.getElem_mem hj')
        have hh := ih ht j hj'
        have hc := earlier_count_le rs ht j hj'
        simp only [List.getElem_cons_succ]
        by_cases he : r.2 = rs[j].2
        · simp only [List.filter_cons, he, beq_self_eq_true, ↓reduceIte,
            Nat.lt_irrefl, decide_false, Bool.false_eq_true, ↓reduceIte]
          have hi : j + 1 - (rs.filter fun x => x.2 < rs[j].2).length =
              (j - (rs.filter fun x => x.2 < rs[j].2).length) + 1 := by omega
          rw [hi, List.getElem?_cons_succ]
          exact hh
        · have hl : r.2 < rs[j].2 := by omega
          simp only [List.filter_cons, show (r.2 == rs[j].2) = false by
            simp [he],
            ↓reduceIte, Bool.false_eq_true, ↓reduceIte, hl, decide_true, List.length_cons]
          simpa only [Nat.succ_sub_succ_eq_sub] using hh
  intro b j hs hj
  exact gap_getElem b hs j hj