proposition: Lemma subseq_filter s1 s2 a : subseq s1 (filter a s2) = all a s1 && subseq s1 s2.
proof: Proof. elim: s2 s1 => [|x s2 IHs] [|y s1] //=; rewrite ?andbF ?sub0seq //. by case a_x: (a x); rewrite /= !IHs /=; case: eqP => // ->; rewrite a_x. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)