theorem Hex.GraphIso.Nauty.Sparse.CountSort.firstRun_congr {y z : Array Nat} {first last : Nat} {lab : Array Nat} (h : «Sort».Agree y z first last lab) (hf : first < last) : firstRun lab y first last = firstRun lab z first last ∧ first < firstRun lab y first last ∧ firstRun lab y first last ≤ last

The initial equal-count scan has the same stopping position under local key agreement, including exhaustion at the exclusive cell end.

theorem Hex.GraphIso.Nauty.Sparse.CountSort.minima_congr {y z : Array Nat} {first last : Nat} {lab : Array Nat} {begin : Nat} (h : «Sort».Agree y z first last lab) (hb : first < begin ∧ begin ≤ last) (cap : Nat) : minima lab y cap first last begin = minima lab z cap first last begin ∧ have r := minima lab y cap first last begin; «Sort».Agree y z first last r.snd.snd.snd.snd ∧ first < r.snd.fst ∧ r.snd.fst ≤ r.snd.snd.snd.fst ∧ r.snd.snd.snd.fst ≤ last

The literal three-way insertion, including aliasing reads after the first write, observes only keys of vertices in the original cell. Its returned cuts, minima and complete label array agree.