proposition: Lemma sub_imset_pre (A : {pred aT}) (B : {pred rT}) : (f @: A \subset B) = (A \subset f @^-1: B).
proof: Proof. apply/subsetP/subsetP=> [sfAB x Ax | sAf'B fx]. by rewrite inE sfAB ?imset_f. by move=> /imsetP[a + ->] => /sAf'B /[!inE]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)