Counting ordered pairs in Fin n × Fin n

The number of strictly increasing pairs (i, j) with i < j drawn from Fin n is the binomial coefficient n.choose 2. This is the combinatorial core of the union-bound step in birthday-style arguments, where the collision event ranges over the unordered pairs of query positions.

theorem Finset.card_filter_fst_lt_snd_eq_sum_range (m : ℕ) : {p : Fin m × Fin m | p.1 < p.2}.card = ∑ k ∈ range m, k

The strictly-increasing pairs over Fin m are counted by the Gauss sum ∑_{k < m} k.

theorem Finset.card_filter_fst_lt_snd (n : ℕ) : {p : Fin n × Fin n | p.1 < p.2}.card = n.choose 2

The number of strictly increasing pairs (i, j) with i < j in Fin n × Fin n is the binomial coefficient n.choose 2.