theorem Hex.GraphIso.Nauty.sum_range_succ (f : Nat → Nat) (m : Nat) : (List.map f (List.range (m + 1))).sum = (List.map f (List.range m)).sum + f m

Peel the last summand off a sum over List.range.

theorem Hex.GraphIso.Nauty.sum_range_two (f : Nat → Nat) : (List.map f (List.range 2)).sum = f 0 + f 1

A sum over List.range 2 in closed form.

theorem Hex.GraphIso.Nauty.sum_range_three (f : Nat → Nat) : (List.map f (List.range 3)).sum = f 0 + f 1 + f 2

A sum over List.range 3 in closed form.

theorem Hex.GraphIso.Nauty.sum_range_const (c m : Nat) : (List.map (fun (x : Nat) => c) (List.range m)).sum = m * c

A constant sum over List.range.

theorem Hex.GraphIso.Nauty.sum_range_le (f : Nat → Nat) (m : Nat) : (∀ (o : Nat), o < m → f o ≤ 1) → (List.map f (List.range m)).sum ≤ m

A sum of values at most one over List.range m is at most m.

theorem Hex.GraphIso.Nauty.sum_range_eq_zero {f : Nat → Nat} (m : Nat) : (List.map f (List.range m)).sum = 0 → ∀ (o : Nat), o < m → f o = 0

A vanishing sum over List.range has every summand zero.

theorem Hex.GraphIso.Nauty.sum_range_eq_len {f : Nat → Nat} (m : Nat) : (∀ (o : Nat), o < m → f o ≤ 1) → (List.map f (List.range m)).sum = m → ∀ (o : Nat), o < m → f o = 1

A sum of values at most one over List.range m that reaches m has every summand one.

theorem Hex.GraphIso.Nauty.countP_zero_of_none {p : Nat → Bool} (l : List Nat) : (∀ (i : Nat), i ∈ l → ¬p i = true) → List.countP p l = 0

A predicate satisfied nowhere in a list counts zero.

theorem Hex.GraphIso.Nauty.countP_range_le_one {p : Nat → Bool} {n : Nat} (h : ∀ (i j : Nat), i < n → j < n → p i = true → p j = true → i = j) : List.countP p (List.range n) ≤ 1

A predicate satisfied at no two distinct positions counts at most one over List.range.

theorem Hex.GraphIso.Nauty.countP_range_one {p : Nat → Bool} {n i₀ : Nat} (hi₀ : i₀ < n) (hp : p i₀ = true) (huniq : ∀ (j : Nat), j < n → p j = true → j = i₀) : List.countP p (List.range n) = 1

A predicate satisfied at exactly one position of List.range n counts one.

theorem Hex.GraphIso.Nauty.countP_le_one_unique {p : Nat → Bool} (l : List Nat) : List.countP p l ≤ 1 → ∀ (w : Nat), w ∈ l → p w = true → ∀ (w' : Nat), w' ∈ l → p w' = true → w = w'

A predicate counting at most one is satisfied by at most one member.

theorem Hex.GraphIso.Nauty.sum_sizes_split (l : List (Nat × Nat)) : (∀ (p : Nat × Nat), p ∈ l → p.fst ≤ p.snd) → (List.map (fun (p : Nat × Nat) => p.snd + 1 - p.fst) l).sum = (List.map (fun (p : Nat × Nat) => p.snd - p.fst) l).sum + l.length

The window sizes of a list of intervals split into the excesses plus the number of intervals.

theorem Hex.GraphIso.Nauty.sum_excess_ge_countP (l : List (Nat × Nat)) : (∀ (p : Nat × Nat), p ∈ l → p.fst ≤ p.snd) → (List.map (fun (p : Nat × Nat) => p.snd - p.fst) l).sum ≥ List.countP (fun (p : Nat × Nat) => decide (p.fst < p.snd)) l

The excesses of a list of intervals sum to at least the number of nontrivial ones.

theorem Hex.GraphIso.Nauty.sum_excess_ge_countP_add {q : Nat × Nat} (l : List (Nat × Nat)) : (∀ (p : Nat × Nat), p ∈ l → p.fst ≤ p.snd) → q ∈ l → (List.map (fun (p : Nat × Nat) => p.snd - p.fst) l).sum ≥ List.countP (fun (p : Nat × Nat) => decide (p.fst < p.snd)) l + (q.snd - q.fst) - 1

The excess sum also carries one distinguished interval's excess in full.

theorem Hex.GraphIso.Nauty.sum_excess_ge_countP_add2 {q q' : Nat × Nat} (l : List (Nat × Nat)) : (∀ (p : Nat × Nat), p ∈ l → p.fst ≤ p.snd) → q ∈ l → q' ∈ l → q ≠ q' → (List.map (fun (p : Nat × Nat) => p.snd - p.fst) l).sum ≥ List.countP (fun (p : Nat × Nat) => decide (p.fst < p.snd)) l + (q.snd - q.fst) + (q'.snd - q'.fst) - 2

The excess sum also carries two distinct distinguished intervals' excesses in full.

theorem Hex.GraphIso.Nauty.exc_ge_one {q : Nat × Nat} (l : List (Nat × Nat)) : q ∈ l → (List.map (fun (p : Nat × Nat) => p.snd - p.fst) l).sum ≥ q.snd - q.fst

The excesses of a list of intervals sum to at least one member's excess.

theorem Hex.GraphIso.Nauty.exc_ge_two {q q' : Nat × Nat} (l : List (Nat × Nat)) : q ∈ l → q' ∈ l → q ≠ q' → (List.map (fun (p : Nat × Nat) => p.snd - p.fst) l).sum ≥ q.snd - q.fst + (q'.snd - q'.fst)

The excesses of a list of intervals sum to at least two distinct members' excesses.

theorem Hex.GraphIso.Nauty.exc_ge_three {q q' q'' : Nat × Nat} (l : List (Nat × Nat)) : q ∈ l → q' ∈ l → q'' ∈ l → q ≠ q' → q ≠ q'' → q' ≠ q'' → (List.map (fun (p : Nat × Nat) => p.snd - p.fst) l).sum ≥ q.snd - q.fst + (q'.snd - q'.fst) + (q''.snd - q''.fst)

The excesses of a list of intervals sum to at least three distinct members' excesses.