proposition: Lemma Sub_imset (T : finType) (P : {pred T}) (s : subFinType P) {A : {set s}} (x : T) (Px : P x) : (Sub x Px \in A) = (x \in val @: A).
proof: Proof. by rewrite -[X in X \in val @: _](SubK s Px) mem_imset. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)