theorem Hex.GraphIso.Nauty.Sparse.Sort.partition_congr {y z : Array Nat} {start len : Nat} {x : Array Nat} (h : Agree y z start (start + len) x) (hl : 0 < len) : partition x y start len = partition x z start len

The exact Bentley–McIlroy partition, including both returned sizes, depends only on keys stored in its current segment.