proposition: Lemma map_subset {T T' : finType} (s1 s2 : seq T) (f : T -> T') : s1 \subset s2 -> [seq f x | x <- s1 ] \subset [seq f x | x <- s2].
proof: Proof. move=> s1s2; apply/subsetP => _ /mapP[y] /[swap] -> ys1. by apply/mapP; exists y => //; move/subsetP : s1s2; exact. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)