fact: Fixpoint rfilter {A} (p : pred A) (ts : seq A) : seq A := if ts is t :: ts' then if p t then ts' else t :: rfilter p ts' else [::].
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq eqtype) pcm(options prelude)