proposition: Lemma bij_imset_f (aT rT : finType) (f : bij aT rT) (x : aT) (A : {set aT}): (f x \in [set f x | x in A]) = (x \in A).
proof: Proof. apply/imsetP/idP; last by exists x. case => x0 xA. by move/(@bij_injective _ _ f) ->. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries)