proposition: Fact IR_maxset D : irredundant D -> W D = IR_w -> maxset irredundant D.
proof: Proof. move => irrD IRD; apply: maxweight_maxset => // A. rewrite -/W IRD; exact: IR_max. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries digraph sgraph)