proposition: Lemma path_filter_in x a s : all P (x :: s) -> path leT x s -> path leT x (filter a s).
proof: Proof. by move=> Pxs; rewrite filter_mask; exact: path_mask_in. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)