Numbers are frequently ModEq to fixed numbers

In this file we prove that m ≡ d [MOD n] frequently as m → ∞.

theorem Nat.frequently_modEq {n : ℕ} (h : n ≠ 0) (d : ℕ) : ∃ᶠ (m : ℕ) in Filter.atTop, m ≡ d [MOD n]

Infinitely many natural numbers are equal to d mod n.

theorem Nat.frequently_mod_eq {d : ℕ} {n : ℕ} (h : d < n) : ∃ᶠ (m : ℕ) in Filter.atTop, m % n = d

theorem Nat.frequently_even : ∃ᶠ (m : ℕ) in Filter.atTop, Even m

theorem Nat.frequently_odd : ∃ᶠ (m : ℕ) in Filter.atTop, Odd m