proposition: Lemma leqwset A B : A \subset B -> W A <= W B.
proof: Proof. move=> AsubB ; by rewrite [X in _ <= X](big_setID A) /= (setIidPr AsubB) leq_addr. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries digraph sgraph)