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.

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.