proposition: Lemma fsetD_bij_bwd_proof (k : B `\` C') : val (f^-1 (Sub (val k) (fsetDl (valP k)))) \in A `\` C.
proof: Proof. subst. rewrite inE [_ \in A]valP andbT. apply: contraTN (valP k) => X. rewrite inE negb_and negbK. apply/orP;left. apply/imfsetP => /=. exists (f^-1 (Sub (val k) (fsetDl (valP k)))); by rewrite ?inE ?bijK'. Qed.
imports: mathcomp(all_ssreflect) Coq(Relations.Relation_Definitions) GraphTheory(edone preliminaries) GraphTheory(bij)