theorem Hex.GraphIso.Nauty.Sparse.Minima.constant_sorted {lab hits : Array Nat} {first upto value : Nat} (hc : ∀ (q : Nat), first ≤ q → q < upto → hits[lab[q]!]! = value) : «Sort».Sorted lab hits first (upto - first)

theorem Hex.GraphIso.Nauty.Sparse.Minima.before_le {q : Nat} {lab hits : Array Nat} {first v2 v3 upto w1 w2 : Nat} (h : Minima lab hits first v2 v3 upto w1 w2) (hq : first ≤ q) (hqt : q < v3) : hits[lab[q]!]! ≤ w2

theorem Hex.GraphIso.Nauty.Sparse.Minima.before_sorted {lab hits : Array Nat} {first v2 v3 upto w1 w2 : Nat} (h : Minima lab hits first v2 v3 upto w1 w2) : «Sort».Sorted lab hits first (v3 - first)

theorem Hex.GraphIso.Nauty.Sparse.Minima.done_sorted {lab hits : Array Nat} {first v2 v3 upto w1 w2 : Nat} (h : Minima lab hits first v2 v3 upto w1 w2) (he : upto = v2 ∨ upto = v3) : «Sort».Sorted lab hits first (upto - first)

theorem Hex.GraphIso.Nauty.Sparse.Minima.sort_tail {lab hits : Array Nat} {first v2 v3 upto w1 w2 : Nat} (h : Minima lab hits first v2 v3 upto w1 w2) (hb : upto ≤ lab.size) : «Sort».Sorted («Sort».indirect lab hits v3 (upto - v3)) hits first (upto - first)

Sorting the larger-count tail completes the ordering of the whole cell. The proof uses the exact sort's executed permutation, exterior, and ordering contracts; tied labels may be rearranged.