proposition: Proposition Gamma_w_leq_IR_w : Gamma_w <= IR_w.
proof: Proof. rewrite /Gamma_w. have [D min_domD _] := arg_maxnP W inhb_min_dom_is_minimal_dominating. have irrD := maxsetp (minimal_dom_is_maximal_irr min_domD). exact: IR_max. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries digraph sgraph)