proposition: Lemma subseq_pairwise xs ys : subseq xs ys -> pairwise r ys -> pairwise r xs.
proof: Proof. by case/subseqP => m _ ->; apply: pairwise_mask. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)