Catalan, central binomial and derangement numbers at primes

For every prime p: C(2p, p) ≡ 2, Catalan(p) ≡ 2 and the number of derangements D(p) ≡ -1 (mod p). The first follows from Vandermonde's identity C(2p, p) = Σ C(p, i)² and p ∣ C(p, i) for 0 < i < p; the second from (p + 1) Catalan(p) = C(2p, p); the third from the recurrence of numDerangements (p = 2 checked directly, odd p by parity).

Main results

• PrimeCongruences.centralBinom_prime: C(2p, p) = 2 in ZMod p
• PrimeCongruences.catalan_prime: Catalan(p) = 2 in ZMod p
• PrimeCongruences.numDerangements_prime: D(p) = -1 in ZMod p

References

• Classical congruences; found missing from Mathlib by excovery.identidades_mathlib (28-oct-2026).

theorem PrimeCongruences.centralBinom_prime (p : ℕ) [hp : Fact (Nat.Prime p)] : ↑p.centralBinom = 2

The central binomial coefficient C(2p, p) is ≡ 2 (mod p) for a prime p.

theorem PrimeCongruences.catalan_prime (p : ℕ) [hp : Fact (Nat.Prime p)] : ↑(catalan p) = 2

Catalan(p) ≡ 2 (mod p) for a prime p.

theorem PrimeCongruences.numDerangements_prime (p : ℕ) [hp : Fact (Nat.Prime p)] : ↑↑(numDerangements p) = -1

The number of derangements satisfies D(p) ≡ -1 (mod p) for a prime p.