First indices and cardinality bounds in natural-number ranges

Range index and duplicate-free natural-list length bounds shared across certificate modules.

Main results

• List.idxOf_range_of_lt, List.length_filter_lt_le, List.length_le_of_nodup_lt.
• List.length_filter_range_eq_one_iff: exactly one number below n passes a test.

theorem List.idxOf_range_of_lt {i n : ℕ} (hi : i < n) : idxOf i (range n) = i

An in-range natural number occurs at its own position in range.

theorem List.length_filter_lt_le {S : List ℕ} (hS : S.Nodup) (u : ℕ) : (filter (fun (x : ℕ) => decide (x < u)) S).length ≤ u

In a duplicate-free list of naturals, at most u elements are strictly below u.

theorem List.length_le_of_nodup_lt {n : ℕ} {S : List ℕ} (hS : S.Nodup) (hSn : ∀ s ∈ S, s < n) : S.length ≤ n

A duplicate-free list of naturals all strictly below n has length at most n.

theorem List.length_filter_range_eq_one_iff {n : ℕ} {p : ℕ → Bool} : (filter p (range n)).length = 1 ↔ ∃! j : ℕ, j < n ∧ p j = true

Filtering range n leaves one entry exactly when one number below n passes the test.