by
  let priorityAt : List Nat → Nat → Nat := fun a i => (a[i]?).getD 0
  let nearestLeft : List Nat → Nat → Option Nat := fun a i => (List.range i).reverse.find? (fun j => decide (priorityAt a j < priorityAt a i))
  let nearestRight : List Nat → Nat → Option Nat := fun a i => (List.range a.length).find? (fun j => decide (i < j ∧ priorityAt a j < priorityAt a i))
  let nextSameLeft : List Nat → Nat → Option Nat := fun a i => (List.range a.length).find? (fun j => decide (i < j ∧ nearestLeft a j = nearestLeft a i))
  let groupRight : List Nat → Nat → Option Nat := fun a i => match nextSameLeft a i with | some j => some j | none => (nearestLeft a i).bind (nearestRight a)

  
  have find_min_spec (p : Nat → Bool) (xs : List Nat)
      (hs : xs.Pairwise (· ≤ ·)) (b : Nat) :
      xs.find? p = some b ↔ b ∈ xs ∧ p b = true ∧ ∀ a ∈ xs, a < b → p a = false := by
    induction xs with
    | nil => simp
    | cons x xs ih =>
      have htail := hs.of_cons
      have hrel := (List.pairwise_cons.mp hs).1
      by_cases hx : p x = true
      · simp only [List.find?_cons_of_pos hx, Option.some.injEq]
        constructor
        · intro he; subst b
          refine ⟨List.mem_cons_self, hx, ?_⟩
          intro a ha hab
          rcases List.mem_cons.mp ha with rfl | ha
          · omega
          · have := hrel a ha; omega
        · rintro ⟨hb, hp, hn⟩
          rcases List.mem_cons.mp hb with rfl | hb
          · rfl
          · have he := hrel b hb
            by_cases hxb : x = b
            · exact hxb
            · have := hn x List.mem_cons_self (by omega)
              simp [hx] at this
      · have hf : p x = false := by cases h : p x <;> simp_all
        rw [List.find?_cons_of_neg (by simpa using hx), ih htail]
        constructor
        · rintro ⟨hb,hp,hn⟩
          refine ⟨List.mem_cons_of_mem x hb,hp,?_⟩
          intro a ha hab
          rcases List.mem_cons.mp ha with rfl | ha
          · exact hf
          · exact hn a ha hab
        · rintro ⟨hb,hp,hn⟩
          have hb' : b ∈ xs := by
            rcases List.mem_cons.mp hb with rfl | hb
            · simp [hf] at hp
            · exact hb
          exact ⟨hb',hp,fun a ha hab => hn a (List.mem_cons_of_mem x ha) hab⟩
  
  have find_max_spec (p : Nat → Bool) (xs : List Nat)
      (hs : xs.Pairwise (fun x y => y ≤ x)) (b : Nat) :
      xs.find? p = some b ↔ b ∈ xs ∧ p b = true ∧ ∀ a ∈ xs, b < a → p a = false := by
    induction xs with
    | nil => simp
    | cons x xs ih =>
      have htail := hs.of_cons
      have hrel := (List.pairwise_cons.mp hs).1
      by_cases hx : p x = true
      · simp only [List.find?_cons_of_pos hx, Option.some.injEq]
        constructor
        · intro he; subst b
          refine ⟨List.mem_cons_self, hx, ?_⟩
          intro a ha hab
          rcases List.mem_cons.mp ha with rfl | ha
          · omega
          · have := hrel a ha; omega
        · rintro ⟨hb, hp, hn⟩
          rcases List.mem_cons.mp hb with rfl | hb
          · rfl
          · have he := hrel b hb
            by_cases hxb : x = b
            · exact hxb
            · have := hn x List.mem_cons_self (by omega)
              simp [hx] at this
      · have hf : p x = false := by cases h : p x <;> simp_all
        rw [List.find?_cons_of_neg (by simpa using hx), ih htail]
        constructor
        · rintro ⟨hb,hp,hn⟩
          refine ⟨List.mem_cons_of_mem x hb,hp,?_⟩
          intro a ha hab
          rcases List.mem_cons.mp ha with rfl | ha
          · exact hf
          · exact hn a ha hab
        · rintro ⟨hb,hp,hn⟩
          have hb' : b ∈ xs := by
            rcases List.mem_cons.mp hb with rfl | hb
            · simp [hf] at hp
            · exact hb
          exact ⟨hb',hp,fun a ha hab => hn a (List.mem_cons_of_mem x ha) hab⟩
  
  have range_sorted (n : Nat) : (List.range n).Pairwise (· ≤ ·) := by
    rw [List.pairwise_iff_getElem]
    intro i j hi hj hij
    simp only [List.length_range] at hi hj
    simp [List.getElem_range, Nat.le_of_lt hij]
  
  have left_some (a : List Nat) (i l : Nat) :
      nearestLeft a i = some l ↔ l < i ∧ priorityAt a l < priorityAt a i ∧
        ∀ k, l < k → k < i → priorityAt a i ≤ priorityAt a k := by
    dsimp only [nearestLeft]
    rw [find_max_spec _ _ (List.pairwise_reverse.mpr (range_sorted i))]
    simp only [List.mem_reverse, List.mem_range, decide_eq_true_eq, decide_eq_false_iff_not]
    constructor
    · rintro ⟨hl,hp,hm⟩; exact ⟨hl,hp,fun k hlk hki => Nat.le_of_not_lt (hm k hki hlk)⟩
    · rintro ⟨hl,hp,hm⟩; exact ⟨hl,hp,fun k hki hlk => Nat.not_lt.mpr (hm k hlk hki)⟩
  
  have left_none (a : List Nat) (i : Nat) :
      nearestLeft a i = none ↔ ∀ k, k < i → priorityAt a i ≤ priorityAt a k := by
    simp only [nearestLeft,List.find?_eq_none,List.mem_reverse,List.mem_range,decide_eq_true_eq]
    constructor
    · intro h k hk; exact Nat.le_of_not_lt (h k hk)
    · intro h k hk; exact Nat.not_lt.mpr (h k hk)
  
  have right_some (a : List Nat) (i r : Nat) :
      nearestRight a i = some r ↔ r < a.length ∧ i < r ∧ priorityAt a r < priorityAt a i ∧
        ∀ k, i < k → k < r → priorityAt a i ≤ priorityAt a k := by
    dsimp only [nearestRight]
    rw [find_min_spec _ _ (range_sorted a.length)]
    simp only [List.mem_range, decide_eq_true_eq, decide_eq_false_iff_not]
    constructor
    · rintro ⟨hr,⟨hir,hp⟩,hm⟩
      exact ⟨hr,hir,hp,fun k hik hkr => Nat.le_of_not_lt (fun h => hm k (by omega) hkr ⟨hik,h⟩)⟩
    · rintro ⟨hr,hir,hp,hm⟩
      refine ⟨hr,⟨hir,hp⟩,?_⟩
      intro k hk hkr h; have := hm k h.1 hkr; omega
  
  have right_none (a : List Nat) (i : Nat) :
      nearestRight a i = none ↔ ∀ k, i < k → k < a.length → priorityAt a i ≤ priorityAt a k := by
    simp only [nearestRight,List.find?_eq_none,List.mem_range,decide_eq_true_eq]
    constructor
    · intro h k hik hk; exact Nat.le_of_not_lt (fun hp => h k hk ⟨hik,hp⟩)
    · intro h k hk hp; have := h k hp.1 hk; omega
  
  have next_some (a : List Nat) (i r : Nat) :
      nextSameLeft a i = some r ↔ r < a.length ∧ i < r ∧ nearestLeft a r = nearestLeft a i ∧
        ∀ k, i < k → k < r → nearestLeft a k ≠ nearestLeft a i := by
    dsimp only [nextSameLeft]
    rw [find_min_spec _ _ (range_sorted a.length)]
    simp only [List.mem_range, decide_eq_true_eq, decide_eq_false_iff_not]
    constructor
    · rintro ⟨hr,⟨hir,hp⟩,hm⟩
      exact ⟨hr,hir,hp,fun k hik hkr => fun h => hm k (by omega) hkr ⟨hik,h⟩⟩
    · rintro ⟨hr,hir,hp,hm⟩
      exact ⟨hr,⟨hir,hp⟩,fun k hk hkr h => hm k h.1 hkr h.2⟩
  
  have next_none (a : List Nat) (i : Nat) :
      nextSameLeft a i = none ↔ ∀ k, i < k → k < a.length → nearestLeft a k ≠ nearestLeft a i := by
    simp only [nextSameLeft,List.find?_eq_none,List.mem_range,decide_eq_true_eq]
    constructor
    · intro h k hik hk he; exact h k hk ⟨hik,he⟩
    · intro h k hk hp; exact h k hp.1 hk hp.2
  
  have priority_ne (a : List Nat) (hd : a.Nodup) (i j : Nat)
      (hi : i < a.length) (hj : j < a.length) (hne : i ≠ j) :
      priorityAt a i ≠ priorityAt a j := by
    intro he
    have hg : a[i] = a[j] := by simpa [priorityAt, List.getElem?_eq_getElem hi, List.getElem?_eq_getElem hj] using he
    have hpairs := List.pairwise_iff_getElem.mp hd
    by_cases hij : i < j
    · exact hpairs i j hi hj hij hg
    · exact hpairs j i hj hi (by omega) hg.symm
  
  have greater_not_same (a : List Nat) (i k : Nat)
      (hik : i < k) (hp : priorityAt a i < priorityAt a k) :
      nearestLeft a k ≠ nearestLeft a i := by
    intro he
    cases hl : nearestLeft a i with
    | none =>
      have hk : nearestLeft a k = none := he.trans hl
      have := (left_none a k).mp hk i hik
      omega
    | some l =>
      have hli := (left_some a i l).mp hl
      have hk : nearestLeft a k = some l := he.trans hl
      have hlk := (left_some a k l).mp hk
      have := hlk.2.2 i hli.1 hik
      omega
  
  have between_not_same (a : List Nat) (hd : a.Nodup) (i r : Nat)
      (hi : i < a.length) (hr : nearestRight a i = some r) :
      ∀ k, i < k → k < r → nearestLeft a k ≠ nearestLeft a i := by
    have hs := (right_some a i r).mp hr
    intro k hik hkr
    have hge := hs.2.2.2 k hik hkr
    have hn := priority_ne a hd i k hi (by omega) (by omega)
    exact greater_not_same a i k hik (by omega)
  
  have none_next (a : List Nat) (hd : a.Nodup) (i : Nat)
      (hi : i < a.length) (hr : nearestRight a i = none) : nextSameLeft a i = none := by
    apply (next_none a i).mpr
    intro k hik hk
    have hge := (right_none a i).mp hr k hik hk
    have hn := priority_ne a hd i k hi hk (by omega)
    exact greater_not_same a i k hik (by omega)
  
  have group_successor_correct : ∀ (a : List Nat), a.Nodup → ∀ i, i < a.length → nearestRight a i = groupRight a i := by
    intro a hd i hi
    cases hl : nearestLeft a i with
    | none =>
      have hs := (left_none a i).mp hl
      cases hr : nearestRight a i with
      | none =>
        have hn := none_next a hd i hi hr
        simp [groupRight, hn, hl]
      | some r =>
        have hrs := (right_some a i r).mp hr
        have hrleft : nearestLeft a r = none := by
          apply (left_none a r).mpr
          intro k hkr
          by_cases hki : k < i
          · have := hs k hki; omega
          · by_cases hke : k = i
            · subst k; omega
            · have := hrs.2.2.2 k (by omega) hkr; omega
        have hn : nextSameLeft a i = some r := (next_some a i r).mpr
          ⟨hrs.1, hrs.2.1, hrleft.trans hl.symm, between_not_same a hd i r hi hr⟩
        simp [groupRight, hn]
    | some l =>
      have hls := (left_some a i l).mp hl
      have hllen : l < a.length := by omega
      cases hr : nearestRight a i with
      | none =>
        have hn := none_next a hd i hi hr
        have hrparent : nearestRight a l = none := by
          apply (right_none a l).mpr
          intro k hlk hk
          by_cases hki : k < i
          · have := hls.2.2 k hlk hki; omega
          · by_cases hke : k = i
            · subst k; omega
            · have := (right_none a i).mp hr k (by omega) hk; omega
        simp [groupRight, hn, hl, hrparent]
      | some r =>
        have hrs := (right_some a i r).mp hr
        have hbetween := between_not_same a hd i r hi hr
        by_cases hcomp : priorityAt a l < priorityAt a r
        · have hrleft : nearestLeft a r = some l := by
            apply (left_some a r l).mpr
            refine ⟨by omega, hcomp, ?_⟩
            intro k hlk hkr
            by_cases hki : k < i
            · have := hls.2.2 k hlk hki; omega
            · by_cases hke : k = i
              · subst k; omega
              · have := hrs.2.2.2 k (by omega) hkr; omega
          have hn : nextSameLeft a i = some r := (next_some a i r).mpr
            ⟨hrs.1, hrs.2.1, hrleft.trans hl.symm, hbetween⟩
          simp [groupRight, hn]
        · have hne := priority_ne a hd l r hllen hrs.1 (by omega)
          have hrl : priorityAt a r < priorityAt a l := by omega
          have hrparent : nearestRight a l = some r := by
            apply (right_some a l r).mpr
            refine ⟨hrs.1, by omega, hrl, ?_⟩
            intro k hlk hkr
            by_cases hki : k < i
            · have := hls.2.2 k hlk hki; omega
            · by_cases hke : k = i
              · subst k; omega
              · have := hrs.2.2.2 k (by omega) hkr; omega
          have hn : nextSameLeft a i = none := by
            apply (next_none a i).mpr
            intro k hik hk he
            by_cases hkr : k < r
            · exact hbetween k hik hkr he
            · have hkl : nearestLeft a k = some l := he.trans hl
              have hkls := (left_some a k l).mp hkl
              by_cases hke : k = r
              · subst k; omega
              · have := hkls.2.2 r (by omega) (by omega)
                omega
          simp [groupRight, hn, hl, hrparent]
  
  exact group_successor_correct