Counting inequalities for equitable recolouring

Split from the upstream counting module to let the structural lemmas build independently.

theorem HajnalSzemeredi.CountHyp.card_Sy {V : Type u_1} {G : SimpleGraph V} {S : Finset V} {c : V → ℕ} {PA PB TU : Finset ℕ} {r s : ℕ} (h : CountHyp G S c PA PB TU r s) {y : V} (hy : y ∈ part S c PB) : TU.card + 1 + (nbr G (part S c PB) y).card ≤ (Sy G S c TU (part S c PB) y).card + PB.card

Desigualdad (2.3): |S^y| ≥ t - q + 1 + d_B(y).

theorem HajnalSzemeredi.CountHyp.deg_B {V : Type u_1} {G : SimpleGraph V} {S : Finset V} {c : V → ℕ} {PA PB TU : Finset ℕ} {r s : ℕ} (h : CountHyp G S c PA PB TU r s) {y : V} (hy : y ∈ part S c PB) : (nbr G (part S c PB) y).card + 1 ≤ PB.card

(2.1), forma de grado: d_B(y) ≤ q - 1 para y ∈ B.

theorem HajnalSzemeredi.CountHyp.lemma_2_2 {V : Type u_1} {G : SimpleGraph V} {S : Finset V} {c : V → ℕ} {PA PB TU : Finset ℕ} {r s : ℕ} (h : CountHyp G S c PA PB TU r s) {W : ℕ} (hW : W ∈ TU) (hW' : ∀ z ∈ cls S c W, (Sz G S c TU (part S c PB) z).Nonempty → ∀ X ∈ PA, X ≠ W → ¬Movable G S c z X) : PB.card + 1 ≤ TU.card ∧ ∀ y ∈ part S c PB, (Sy G S c TU (part S c PB) y).Nonempty

Lema 2.2. Si ningún vértice solo de W ∈ TU es movible a otra clase de PA, entonces q + 1 ≤ t y todo y ∈ B es solo.

theorem HajnalSzemeredi.CountHyp.lemma_2_3 {V : Type u_1} {G : SimpleGraph V} {S : Finset V} {c : V → ℕ} {PA PB TU : Finset ℕ} {r s : ℕ} (h : CountHyp G S c PA PB TU r s) : ∃ z ∈ S, c z ∈ TU ∧ (Sz G S c TU (part S c PB) z).Nonempty ∧ ((∃ X ∈ PA, X ≠ c z ∧ Movable G S c z X) ∨ ∃ y₁ ∈ Sz G S c TU (part S c PB) z, ∃ y₂ ∈ Sz G S c TU (part S c PB) z, y₁ ≠ y₂ ∧ ¬G.Adj y₁ y₂)

Lema 2.3. Existe un vértice solo z (con color en TU) que es movible a otra clase de PA, o que tiene dos vecinos especiales distintos no adyacentes.