proposition: Lemma filter_predC1 x xs : x \notin xs -> filter (predC1 x) xs = xs.
proof: Proof. by move=>H; apply/all_filterP/allP=>y /=; case: eqP=>// ->; apply/contraL. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)