proposition: Lemma in_imfset (T : choiceType) (f : T -> K) (p : finmempred T) (x : T) : in_mem x p -> f x \in imfset key f p.
proof: Proof. by move=> px; apply/imfsetP; exists x. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)