proposition: Lemma map_subseq s1 s2 : subseq s1 s2 -> subseq (map f s1) (map f s2).
proof: Proof. case/subseqP=> m sz_m ->; apply/subseqP. by exists m; rewrite ?size_map ?map_mask. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)