@[simp]

theorem Hex.GraphIso.Nauty.Sparse.RowOrder.mem_values {n : Nat} (row : List (Fin n)) (v : Fin n) : ↑v ∈ List.map Fin.val row ↔ v ∈ row

theorem Hex.GraphIso.Nauty.Sparse.RowOrder.eq_of_subset {n : Nat} {a b : List (Fin n)} (ha : List.Pairwise (fun (x1 x2 : Fin n) => x1 < x2) a) (hb : List.Pairwise (fun (x1 x2 : Fin n) => x1 < x2) b) (hlen : a.length = b.length) (hsub : a ⊆ b) : a = b

theorem Hex.GraphIso.Nauty.Sparse.Diff.congr_seen {n stamp : Nat} {old seen : List Nat} {marks : Array Nat} {mina : Nat} (h : Diff n stamp old seen marks mina) {other : List Nat} (he : ∀ (v : Nat), v ∈ seen ↔ v ∈ other) : Diff n stamp old other marks mina

theorem Hex.GraphIso.Nauty.Sparse.Diff.equal {n stamp : Nat} {marks : Array Nat} {mina : Nat} {a b : List (Fin n)} (h : Diff n stamp (List.map Fin.val b) (List.map Fin.val a) marks mina) (ha : List.Pairwise (fun (x1 x2 : Fin n) => x1 < x2) a) (hb : List.Pairwise (fun (x1 x2 : Fin n) => x1 < x2) b) (hlen : a.length = b.length) (hm : mina = n) : a = b

theorem Hex.GraphIso.Nauty.Sparse.Diff.smaller {n stamp : Nat} {marks : Array Nat} {mina : Nat} {a b : List (Fin n)} (h : Diff n stamp (List.map Fin.val b) (List.map Fin.val a) marks mina) (ha : List.Pairwise (fun (x1 x2 : Fin n) => x1 < x2) a) (hb : List.Pairwise (fun (x1 x2 : Fin n) => x1 < x2) b) (hlen : a.length = b.length) {v : Fin n} (hmark : marks[↑v]! = stamp) (hlt : ↑v < mina) : rowCmp a b = Ordering.lt

A surviving old mark below the candidate's least exclusive vertex determines a strict loss for the candidate row.

theorem Hex.GraphIso.Nauty.Sparse.Diff.greater {n stamp : Nat} {marks : Array Nat} {mina : Nat} {a b : List (Fin n)} (h : Diff n stamp (List.map Fin.val b) (List.map Fin.val a) marks mina) (ha : List.Pairwise (fun (x1 x2 : Fin n) => x1 < x2) a) (hb : List.Pairwise (fun (x1 x2 : Fin n) => x1 < x2) b) (hlen : a.length = b.length) (hm : mina < n) (hscan : ∀ (v : Nat), v ∈ List.map Fin.val b → marks[v]! = stamp → mina ≤ v) : rowCmp a b = Ordering.gt

Exhausting the old row without a smaller surviving mark determines a strict win whenever the candidate has an exclusive vertex.