proposition: Fact ir_min D : max_irr D -> ir_w <= W D.
proof: Proof. rewrite /ir_w. by case: (arg_minnP W inhb_max_irr_is_maximal_irredundant) => A _ ; apply. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries digraph sgraph)