LeanPool.ErdosTuzaValtr.Main.CapCup

Imported Lean Pool material for LeanPool.ErdosTuzaValtr.Main.CapCup.

theorem Config.has_cap2_cup2 {α : Type u_1} [LinearOrder α] (C : Config α) {S : Finset α} (hS : 1 < S.card) : C.HasNCap 2 S ∧ C.HasNCup 2 S

theorem Config.binom_eq (a b : ℕ) : (a + b + 2).choose (a + 1) = (a + b + 1).choose a + (a + b + 1).choose (a + 1)

theorem Config.cap_cup {α : Type u_1} [LinearOrder α] (C : Config α) (a b : ℕ) (S : Finset α) (hS : (a + b).choose a < S.card) : C.HasNCap (a + 2) S ∨ C.HasNCup (b + 2) S