proposition: Lemma replication (G : sgraph) (v : G) : perfect G -> perfect (replicate v).
proof: Proof. move => perfG; apply: (@replication_aux (replicate v) (Some v) None). - by rewrite /edge_rel/= v_in_clneigh. - by apply/setP => -[x|] ; rewrite !inE /edge_rel//= ?v_in_clneigh ?Some_eqE ?in_cln 1?eq_sym. - by rewrite -perfect_induced -(diso_perfectT (diso_replicate v)). Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries bij digraph sgraph) GraphTheory(dom partition coloring)