proposition: Lemma sorted_mask_in m s : all P s -> sorted leT s -> sorted leT (mask m s).
proof: Proof. by move=> Ps; rewrite !sorted_pairwise_in ?all_mask //; exact: pairwise_mask. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)