proposition: Fact ir_witness : exists2 D, max_irr D & W D = ir_w.
proof: Proof. rewrite /ir_w. case: (arg_minnP W inhb_max_irr_is_maximal_irredundant) => D. by exists D. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries digraph sgraph)