theorem Hex.GraphIso.Nauty.Sparse.RowOrder.degree_lt {n : Nat} {a b : List (Fin n)} (h : b.length < a.length) : rowCmp a b = Ordering.lt

theorem Hex.GraphIso.Nauty.Sparse.RowOrder.degree_gt {n : Nat} {a b : List (Fin n)} (h : a.length < b.length) : rowCmp a b = Ordering.gt

theorem Hex.GraphIso.Nauty.Sparse.RowOrder.lex_lt {n : Nat} {a b : List (Fin n)} {v : 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) (hv : v ∈ a) (hn : ¬v ∈ b) (hmin : ∀ (w : Fin n), w ∈ b → ¬w ∈ a → v < w) : compare a b = Ordering.lt

In equally long sorted rows, an exclusive member smaller than every exclusive member of the other row determines the lexicographic comparison.

theorem Hex.GraphIso.Nauty.Sparse.RowOrder.row_gt {n : Nat} {a b : List (Fin n)} {v : 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) (hv : v ∈ a) (hn : ¬v ∈ b) (hmin : ∀ (w : Fin n), w ∈ b → ¬w ∈ a → v < w) : rowCmp a b = Ordering.gt

Sparse nauty prefers the row containing the first differing vertex when both degrees agree.

theorem Hex.GraphIso.Nauty.Sparse.RowOrder.row_lt {n : Nat} {a b : List (Fin n)} {v : 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) (hv : v ∈ b) (hn : ¬v ∈ a) (hmin : ∀ (w : Fin n), w ∈ a → ¬w ∈ b → v < w) : rowCmp a b = Ordering.lt