proposition: Lemma fsetD_bij_can_fwd : cancel fsetD_bij_fwd fsetD_bij_bwd.
proof: Proof. move => x. apply: val_inj => //=. by rewrite !(fsvalK,bijK). Qed.
imports: mathcomp(all_ssreflect) Coq(Relations.Relation_Definitions) GraphTheory(edone preliminaries) GraphTheory(bij)