proposition: Lemma min_imperfect_neq0 H : min_imperfect H -> H != set0.
proof: Proof. by apply: contraTneq => ->; rewrite min_imperfect0. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries bij digraph sgraph) GraphTheory(dom partition coloring) mathcomp(ssrint) mathcomp(all_algebra)