proposition: Lemma can_preimset (aT rT : finType) (f : aT -> rT) (A : {set rT}) : A \subset codom f -> [set f x | x in f @^-1: A] = A.
proof: Proof. move/subsetP => subAi; apply/setP => z; apply/imsetP/idP => [[x]|zA]. by rewrite inE => ? ->. by exists (iinv (subAi _ zA)); rewrite ?inE f_iinv. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)