theorem Hex.GraphIso.Nauty.Sparse.splitCounts_sorted {n : Nat} (level first : Nat) (distance : Bool) (s : RefineSt n) (hf : first ≤ s.cellend[first]!) (hb : s.cellend[first]! < s.lab.size) (hk : s.hits[s.lab[first]!]! < n + 2) : «Sort».Sorted (splitCounts level first distance s).lab s.hits first (s.cellend[first]! + 1 - first)

The executed count splitter orders the whole cell by its hit values. Its initial key lies below the n + 2 sentinel used for the second minimum.