proposition: Lemma path_filter (r : rel T) (tr : transitive r) s (p : pred T) x : path r x s -> path r x (filter p s).
proof: Proof. exact: (subseq_path tr (filter_subseq p s)). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path fintype) pcm(options)