proposition: Lemma rfilter_rem {T : eqType} (ts : seq T) x : rfilter (pred1 x) ts = rem x ts.
proof: Proof. by elim: ts=> [|t ts IH] //=; case: eqP=>//= _; rewrite IH. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq eqtype) pcm(options prelude)