proposition: Lemma filter_pred1 x xs : x \notin xs -> filter (pred1 x) xs = [::].
proof: Proof. move=>H; apply/eqP; apply/filter_nilP=>z /eqP ->. by rewrite (negbTE H). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)