proposition: Lemma fsetD_bij_fwd_proof (k : A `\` C) : val (f (Sub (val k) (fsetDl (valP k)))) \in B `\` C'.
proof: Proof. subst. rewrite inE [_ \in B]valP andbT. apply/imfsetP => [/= [x]]. rewrite inE => xC /val_inj. move/(@bij_injective _ _ f) => ?. subst. rewrite /= in xC. case/fsetDP: (valP k). by rewrite xC. Qed.
imports: mathcomp(all_ssreflect) Coq(Relations.Relation_Definitions) GraphTheory(edone preliminaries) GraphTheory(bij)