proposition: Lemma sub_map s1 s2 : {subset s1 <= s2} -> {subset map f s1 <= map f s2}.
proof: Proof. by move=> sub_s ? /mapP[x x_s ->]; rewrite map_f ?sub_s. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)