proposition: Lemma pairwise_mask m xs : pairwise xs -> pairwise (mask m xs).
proof: Proof. by elim: m xs => [|[] m IHm] [|x xs] //= /andP [? ?]; rewrite ?IHm // all_mask. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)