proposition: Lemma wset0 A : (A == set0) = (W A == 0).
proof: Proof. apply/eqP/eqP. - move=> Dempty ; rewrite /weight_set. move: Dempty ->. exact: big_set0. - move=> /eqP weightzero. apply/eqP ; move: weightzero. apply: contraLR => /set0Pn. elim=> x xinD. apply: lt0n_neq0 ; rewrite /W /weight_set (bigD1 x) //=. exact/ltn_addr/positive_weights. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries digraph sgraph)