proposition: Theorem minimal_dom_is_maximal_irr : minset dominating D -> maxset irredundant D.
proof: Proof. rewrite minimal_dom_iff_dom_irr -(rwP (maximal_indsysP _ irr_hereditary)). move=> [dominatingD irredundantD]; split=> // v vnotinD. apply/irredundantPn; exists v; first by rewrite in_setU1 eqxx. apply: contraNT vnotinD => /set0Pn [x /privateP [vdomx xpriv]]. have/bigcupP [u uinD udomx] := forallP dominatingD x. by rewrite -[v](xpriv u) -?in_cln // inE uinD orbT. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries digraph sgraph)