proposition: Lemma fsetD_bijE k (p : k \in A `\` C) q : fsetD_bij (Sub k p) = Sub (val (f (Sub k (fsetDl p)))) q.
proof: Proof. apply: val_inj => /=. do 2 f_equal. exact: val_inj. Qed.
imports: mathcomp(all_ssreflect) Coq(Relations.Relation_Definitions) GraphTheory(edone preliminaries) GraphTheory(bij)