proposition: Lemma imsetS (A B : {pred aT}) : A \subset B -> f @: A \subset f @: B.
proof: Proof. move=> sAB; apply/subsetP => _ /imsetP[x Ax ->]. by apply/imsetP; exists x; rewrite ?(subsetP sAB). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)