theorem Hex.GraphIso.Nauty.Sparse.Sort.partition_order (x y : Array Nat) (start len : Nat) (hb : start + len ≤ x.size) (hl : 0 < len) : Separated (partition x y start len).fst y start (start + len) (pivot x y start len) (start + (partition x y start len).snd.fst) (start + len - (partition x y start len).snd.snd)

The scans exhaust their unclassified interval before the loop bound. The final block swaps then separate strictly smaller, equal, and strictly larger keys at exactly the two fragment boundaries returned by the code.