proposition: Lemma proper_min_imperfect A H : A \proper H -> min_imperfect H -> perfect A.
proof: Proof. by move => propAH /andP[_ /forall_inP] /(_ _ propAH). Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries bij digraph sgraph) GraphTheory(dom partition coloring) mathcomp(ssrint) mathcomp(all_algebra)