proposition: Proposition ir_w_leq_gamma_w : ir_w <= gamma_w.
proof: Proof. rewrite /gamma_w. have [D domD minWD] := arg_minnP W domT. have min_domD := minweight_minset positive_weights domD minWD. have max_irrD := minimal_dom_is_maximal_irr min_domD. exact: ir_min. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries digraph sgraph)