proposition: Lemma min_imperfect0 : min_imperfect (set0 : {set G}) = false.
proof: Proof. by rewrite /min_imperfect_mem omega0 chi0. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries bij digraph sgraph) GraphTheory(dom partition coloring) mathcomp(ssrint) mathcomp(all_algebra)