proposition: Lemma inj_imsetS (aT rT : finType) (f : aT -> rT) (A B : {pred aT}) : injective f -> (f @: A \subset f @: B) = (A \subset B).
proof: Proof. move=> inj_f; apply/subsetP/subsetP => [/= subAB x xA|subAB ? /imsetP[x xA ->]]. by move: (subAB (f x)); rewrite !(mem_imset _ _ inj_f); apply. by rewrite (mem_imset _ _ inj_f); apply: subAB. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)