LeanPool.ErdosTuzaValtr.Main.Lemmas.JoinN2N2

Imported Lean Pool material for LeanPool.ErdosTuzaValtr.Main.Lemmas.JoinN2N2.

theorem Config.join_n2_n2_case_ff {α : Type u_1} [LinearOrder α] (C : Config α) (S : Finset α) (n : ℕ) (a x b : α) (c1 c2 : List α) (lab : C.Label S) (a_in_S : a ∈ S) (x_in_S : x ∈ S) (b_in_S : b ∈ S) (hc1 : C.NCup (n + 2) (c1 ++ [a, x])) (c1_in_S : c1.In S) (hc2 : C.NCup (n + 2) (x :: b :: c2)) (c2_in_S : c2.In S) (sab : ¬lab.Slope a b) : C.HasNGon (n + 3) S

theorem Config.join_n2_n2_case_tt {α : Type u_1} [LinearOrder α] (C : Config α) (S : Finset α) (n : ℕ) (a x b : α) (c1 c2 : List α) (lab : C.Label S) (a_in_S : a ∈ S) (x_in_S : x ∈ S) (b_in_S : b ∈ S) (hc1 : C.NCup (n + 2) (c1 ++ [a, x])) (c1_in_S : c1.In S) (hc2 : C.NCup (n + 2) (x :: b :: c2)) (c2_in_S : c2.In S) (hab : lab.Slope a b) : C.HasNGon (n + 3) S

theorem Config.join_n2_n2 {α : Type u_1} [LinearOrder α] (C : Config α) (S : Finset α) {n : ℕ} (cap4_free : ¬C.HasNCap 4 S) {c1 : List α} (hc1 : C.NCup (n + 2) c1) (c1_in_S : c1.In S) {c2 : List α} (hc2 : C.NCup (n + 2) c2) (c2_in_S : c2.In S) (x : α) (hx1 : x ∈ c1.getLast?) (hx2 : x ∈ c2.head?) : C.HasNGon (n + 3) S