proposition: Fact ir_minset D : max_irr D -> W D = ir_w -> minset max_irr D.
proof: Proof. move => max_irrD irD; apply: minweight_minset => // A. rewrite -/W irD; exact: ir_min. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries digraph sgraph)