proposition: Lemma Mem_filter (T : Type) (a : pred T) (x : T) (s : seq T) : x \In filter a s <-> a x /\ x \In s.
proof: Proof. elim: s; first by split; case. move=>y s IHs /=; rewrite 2!fun_if /=. case E: (a y). - rewrite InE IHs; split; last first. - by case=>H1 /In_cons [->|]; [left | right]. case=>[->|]; first by split=>//; apply/In_cons; left. by case=>H1 H2; split=>//; apply/In_cons; right. rewrite IHs; split. - by case=>H1 H2; split=>//; apply/In_cons; right. by case=>H1 /In_cons [] // ?; subst y; rewrite E in H1. Qed.
imports: Coq(ssreflect ssrbool ssrfun Setoid) mathcomp(ssrnat seq eqtype) pcm(options)