Ported to Lean Pool from jtraverso/hajnal-szemeredi, commit ba34061e3cf12dfc8297610d5d7b3f0afac7ec54; import paths adapted.

Lemas genéricos de alcanzabilidad

Dos herramientas sobre Relation.ReflTransGen que reemplazan el uso de "caminos simples" en el argumento de Kierstead–Kostochka:

• transfer: si x alcanza z por R, y R' contiene todos los arcos de R cuyo destino no es x, entonces x alcanza z por R' (se usa la última visita a x).
• exists_step_avoid: si x ≠ z y x alcanza z, hay un primer paso x → j con j ≠ x tal que j alcanza z sin pasar por x.

theorem HajnalSzemeredi.transfer {α : Type u_1} {R R' : α → α → Prop} {x z : α} (h : Relation.ReflTransGen R x z) (hR : ∀ (a b : α), R a b → b ≠ x → R' a b) : Relation.ReflTransGen R' x z

theorem HajnalSzemeredi.exists_step_avoid {α : Type u_1} {R : α → α → Prop} {x z : α} (h : Relation.ReflTransGen R x z) (hxz : x ≠ z) : ∃ (j : α), R x j ∧ j ≠ x ∧ Relation.ReflTransGen (fun (a b : α) => R a b ∧ a ≠ x ∧ b ≠ x) j z