proposition: Lemma replication_aux (G : sgraph) (v v' : G) : v -- v' -> N[v] = N[v'] -> perfect [set~ v'] -> perfect G.
proof: Proof. move => vv' Nvv' perfNv'; rewrite -perfectT; apply: perfectIweak => H _ /set0Pn [z zH]. have [vv'_H|] := boolP ([set v;v'] \subset H); last first. - have perfNv : perfect [set~ v]. { apply: diso_perfect_induced perfNv'. exact: eq_cln_iso. } rewrite subUset !sub1set negb_and => vNH. wlog vNH : v v' vv' {Nvv'} {perfNv'} perfNv {vNH} / v \notin H. by case/orP: vNH => [vNH /(_ v v') |v'NH /(_ v' v)]; apply; rewrite // sgP. have [|S [S1 S2 _ S3]] := @perfectEstrong _ [set~ v] H z perfNv _ zH. by rewrite subsetC sub1set inE. by exists S. - have Hvv' : H :\ v' \subset [set~ v'] by rewrite subDset setUCr subsetT. have vHv' : v \in H :\ v' by rewrite !inE (sg_edgeNeq vv') (subsetP vv'_H) // !inE eqxx. have perfHv : perfect (H :\ v') by apply: sub_perfect perfNv'. have := @perfectEstrong _ [set~ v'] (H :\ v') v perfNv' Hvv' vHv'. move => [S] [stabS subSH vS cutS]; exists S; split => //. exact: subset_trans subSH (subsetDl _ _). apply/forall_inP => K maxK. have [v'K|v'NK] := boolP (v' \in K). - suff vK : v \in K by apply/set0Pn; exists v; rewrite inE vS vK. apply: wlog_neg => v'NK. apply: maxclique_opn (maxK) _ ; first by case/setD1P : vHv'. apply/subsetP => x xK; case: (eqVneq x v) => [xv|xDv]; first by rewrite -xv xK in v'NK. rewrite opn_cln Nvv' !inE xDv -implyNb sgP; apply/implyP => xDv'. by rewrite (maxclique_clique maxK). - suff: K \in maxcliques (H :\ v') by move/(forall_inP cutS). by apply: maxclique_disjoint => //; rewrite disjoint_sym disjoints1. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries bij digraph sgraph) GraphTheory(dom partition coloring)