proposition: Proposition irredundantPn : reflect (exists2 v, v \in D & private_set v == set0) (~~ irredundant).
proof: Proof. rewrite /irredundant ; apply: (iffP forall_inPn) ; last first. - case => x xinD H1. by exists x ; rewrite ?xinD ?H1. - case => x xinD H2; rewrite negbK in H2. by exists x. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries digraph sgraph)