Complete residue blocks inside real short intervals

theorem NairTenenbaum.residue_count_complete_block (a v : ℕ) {q : ℕ} (hq : 0 < q) : {n ∈ Finset.Ioc a (a + q) | n ≡ v [MOD q]}.card = 1

theorem NairTenenbaum.polynomial_count_complete_block (Q : Polynomial ℤ) (a : ℕ) {q : ℕ} (hq : 0 < q) : {n ∈ Finset.Ioc a (a + q) | q ∣ (Polynomial.eval (↑n) Q).natAbs}.card = rootCount Q q

theorem NairTenenbaum.shortInterval_polynomial_congruence_count_ge (Q : Polynomial ℤ) {x y : ℝ} (hx : 0 ≤ x) {q : ℕ} (hq : 0 < q) (hqy : ↑q ≤ y) : rootCount Q q ≤ {n ∈ shortInterval x y | q ∣ (Polynomial.eval (↑n) Q).natAbs}.card