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

theorem Filter.nonneg_of_eventually_pow_nonneg {α : Type u_1} [LinearOrderedRing α] {a : α} (h : ∀ᶠ (n : ℕ) in Filter.atTop, 0 ≤ a ^ n) : 0 ≤ a