proposition: Lemma ltnwset A B : A \proper B -> W A < W B.
proof: Proof. move => /properP [AsubB]. elim=> x xinB xnotinA. rewrite {2}/W /weight_set (big_setID A) /= (setIidPr AsubB). rewrite -[X in X <= _]addn0 addSn -addnS leq_add2l lt0n. rewrite -/(weight_set _) -wset0. by apply/set0Pn; exists x; apply/setDP. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries digraph sgraph)