by
  dsimp only [OA_statement]
  let rank (b : List Nat) (q : Nat) := q + (b.filter fun boundary => boundary ≤ q).length
  have filter_empty_before (b : List Nat) (q : Nat)
      (h : ∀ r ∈ b, q < r) :
      (b.filter fun r => r ≤ q) = [] := by
    apply List.filter_eq_nil_iff.mpr
    intro r hr
    have ht := h r hr
    simp_all
  have physical_source_remote_lt_iff (b : List Nat)
      (hs : b.Pairwise (fun x y => x ≤ y))
      (j q : Nat) (hj : j < b.length) :
      rank b q < b[j] + j ↔ q < b[j] := by
    induction b generalizing j with
    | nil => simp at hj
    | cons r rs ih =>
      have htail := hs.of_cons
      have hrel : ∀ x ∈ rs, r ≤ x := (List.pairwise_cons.mp hs).1
      cases j with
      | zero =>
        simp only [List.getElem_cons_zero, Nat.add_zero]
        by_cases hq : q < r
        · have he : (rs.filter fun x => x ≤ q) = [] :=
            filter_empty_before rs q (by intro x hx; have hh := hrel x hx; omega)
          simp [rank, show ¬ r ≤ q by omega, he, hq]
        · have hh : r ≤ q := by omega
          simp [rank, hh]
          omega
      | succ j =>
        have hj' : j < rs.length := by simp only [List.length_cons] at hj; omega
        have hrelj := hrel rs[j] (List.getElem_mem hj')
        simp only [List.getElem_cons_succ]
        by_cases hq : q < r
        · have he : (rs.filter fun x => x ≤ q) = [] :=
            filter_empty_before rs q (by intro x hx; have hh := hrel x hx; omega)
          have hb : q < rs[j] := by omega
          simp [rank, show ¬ r ≤ q by omega, he]
          omega
        · have hh : r ≤ q := by omega
          have h := ih htail j hj'
          simp [rank, hh] at h ⊢
          omega
  have remote_count_lt_iff (b : List Nat)
      (hs : b.Pairwise (fun x y => x ≤ y))
      (j q : Nat) (hj : j < b.length) :
      j < (b.filter fun r => r ≤ q).length ↔ b[j] ≤ q := by
    induction b generalizing j with
    | nil => simp at hj
    | cons r rs ih =>
      have htail := hs.of_cons
      have hrel : ∀ x ∈ rs, r ≤ x := (List.pairwise_cons.mp hs).1
      cases j with
      | zero =>
        simp only [List.getElem_cons_zero]
        by_cases hq : r ≤ q
        · simp [hq]
        · have he := filter_empty_before rs q
            (by intro x hx; have hh := hrel x hx; omega)
          simp [hq, he]
      | succ j =>
        have hj' : j < rs.length := by simp only [List.length_cons] at hj; omega
        have hrelj := hrel rs[j] (List.getElem_mem hj')
        simp only [List.getElem_cons_succ]
        by_cases hq : r ≤ q
        · simpa [hq] using ih htail j hj'
        · have he := filter_empty_before rs q
            (by intro x hx; have hh := hrel x hx; omega)
          simp [hq, he]
          omega
  intro b j q hs hj
  have hl := physical_source_remote_lt_iff b hs j q hj
  have hc := remote_count_lt_iff b hs j q hj
  refine ⟨hl, ?_, ?_⟩
  · dsimp only [rank] at hl
    omega
  · dsimp only [rank] at hl
    omega