proposition: Lemma preimsetS (A B : {pred rT}) : A \subset B -> (f @^-1: A) \subset (f @^-1: B).
proof: Proof. by move=> sAB; apply/subsetP=> y /[!inE]; apply: subsetP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)