proposition: Lemma imset_codom (aT rT : finType) (f : aT -> rT) (A : {set aT}) : [set f x | x in A] \subset codom f.
proof: Proof. apply/subsetP => ? /imsetP[x xA ->]; exact: codom_f. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)