proposition: Lemma Lovasz_perfect (G : sgraph) (m : G -> nat) : perfect G -> perfect (Lovasz m).
proof: Proof. have [n leMn] := ubnP (\sum_(x : G) `|m x - 1|%N). elim: n G m leMn => // n IHn G m leMn perfG; rewrite ltnS in leMn. have [/eqP|] := posnP (\sum_x `|m x - 1|). - rewrite sum_nat_eq0 => /forallP/= sum0. have M1 x : m x = 1 by move: (sum0 x); rewrite distn_eq0 => /eqP. suff i : G ≃ Lovasz m by rewrite -(diso_perfectT i). exact: iso_Lovasz_const1. - rewrite lt0n sum_nat_eq0 negb_forall/= => /existsP[x]; rewrite distn_eq0 => M1. have [lt_1_mx|lt_mx_2] := leqP 2 (m x). + pose m' := m[upd x := (m x).-1]. have mxP : 0 < m' x by rewrite /m' updateE -ltnS ?(ltn_predK lt_1_mx). have/IHn/(_ perfG) perfG' : \sum_x `|m' x - 1| < n. { apply: leq_trans leMn. apply: (ltn_sum x) => // [y _ yDx|]; first by rewrite /m' updateE. rewrite !distnEl //; last by rewrite ltnW. by rewrite -subSn // /m' updateE ?(ltn_predK lt_1_mx). } suff i : @replicate (Lovasz m') ⟨ x , Ordinal mxP ⟩ ≃ Lovasz m. { by rewrite -(diso_perfectT i); apply: replication. } apply: diso_comp (iso_Lovasz_repl _) (eq_iso_Lovasz _). move => y; have [->|yDx] := eqVneq y x; rewrite /m' !updateE //. by rewrite (ltn_predK lt_1_mx). + have {M1 lt_mx_2} mx0 : m x = 0 by move: (m x) M1 lt_mx_2 => [|[|[|]]]. pose m' := m[upd x := 1]. have/IHn/(_ perfG) perfG' : \sum_x `|m' x - 1| < n. { apply: leq_trans leMn. apply: (ltn_sum x) => // [y _ yDx|]; first by rewrite /m' updateE. by rewrite /m' updateE mx0 distnn distnS. } suff i : Lovasz m ⇀ Lovasz m' by apply: isubgraph_perfect i perfG'. apply: isubgraph_Lovasz => y. by have [->|yDx] := eqVneq y x; rewrite /m' !updateE // mx0. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries bij digraph sgraph) GraphTheory(dom partition coloring) mathcomp(ssrint)