proposition: Lemma morphpreS R S : R \subset S -> f @*^-1 R \subset f @*^-1 S.
proof: Proof. by move=> sRS; rewrite setIS ?preimsetS. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)