proposition: Lemma subset_filter p s1 s2 : s1 \subset s2 -> [seq a <- s1 | p a] \subset [seq a <- s2 | p a].
proof: Proof. by move/subsetP=> s12; apply/subsetP=> x; rewrite !mem_filter=> /andP[-> /s12]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)