theorem Hex.GraphIso.Nauty.Sparse.pop_push_set (a : Array Nat) (v : Nat) (ha : 0 < a.size) : a.pop.push v = a.setIfInBounds (a.size - 1) v

Replacing the final slot is popping and then pushing the new value.

theorem Hex.GraphIso.Nauty.Sparse.remove_perm (queue : Array Nat) (pos : Nat) (hp : pos < queue.size) : (queue.setIfInBounds pos queue[queue.size - 1]!).pop.toList.Perm (queue.toList.erase queue[pos]!)

The executed replacement-by-last-and-pop operation removes precisely the selected occurrence, even when it is already the last entry.

theorem Hex.GraphIso.Nauty.Sparse.ActiveQueue.remove {n✝ : Nat} {active : VSet n✝} {queue : Array Nat} {pos : Nat} (h : ActiveQueue active queue) (hp : pos < queue.size) : ActiveQueue (active.erase queue[pos]!) (queue.setIfInBounds pos queue[queue.size - 1]!).pop

Removing the selected splitter retains exact agreement with the active bitset, including last-position removal.