proposition: Lemma subset_imfset f (p q : finmempred _) : {subset p <= q} -> imfset key f p `<=` imfset key f q.
proof: Proof. move=> subPQ; apply/fsubsetP=> x /imfsetP [y /= yA ->]. by rewrite in_imfset //= [in_mem _ _]subPQ. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)