proposition: Theorem minimal_dom_iff_dom_irr : minset dominating D <-> (dominating D /\ irredundant D).
proof: Proof. rewrite -(rwP (minimal_indsysP _ dom_superhereditary)); split ; last first. - move=> [dominatingD /irredundantP irredundantD]; split => // v vinD. have/set0Pn [w /privateP [vdomw H1]] := irredundantD v vinD. apply/dominatingPn; exists w. + rewrite in_setD1 negb_and negbK orbC. case: (boolP (w \in D)) => //= /H1 -> //. exact: dominates_refl. + move=> u /setD1P [uneqv uinD]. apply: contra_neqN uneqv => uv. by apply: H1 => //; rewrite /dominates uv orbT. - move => [dominatingD H2] ; split=> //. apply/irredundantP => v vinD. have/dominatingPn[w wnotinDminusv H3] := H2 v vinD. apply/set0Pn; exists w; apply/privateP ; split ; last first. + move=> u uinD udomw. apply: contraTeq udomw => uneqv. have uinDminusv : u \in D :\ v by rewrite in_setD1 uneqv uinD. rewrite /dominates negb_or (H3 u uinDminusv) andbT. by apply: contraNneq wnotinDminusv => <-. + rewrite /dominates ; case: (boolP (v == w)) => //= vneqw. move: wnotinDminusv ; rewrite in_setD1 eq_sym vneqw andTb => wnotinD. have [u uinD] := dominatingP _ dominatingD w wnotinD. case: (boolP (u == v)) => [|uneqv] ; first by move/eqP->. have uinDminusv : u \in D :\ v by rewrite in_setD1 uneqv uinD. by rewrite (negbTE (H3 u uinDminusv)). Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries digraph sgraph)