proposition: Lemma bij_imsetC (aT rT : finType) (f : bij aT rT) (A : {set aT}) : ~: [set f x | x in A] = [set f x | x in ~: A].
proof: Proof. apply/setP => x. by rewrite -[x](bijK' f) !inE !bij_imset_f inE. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries)