proposition: Lemma mask_sort_in s m : all P s -> {m_s : bitseq | mask m_s (sort leT s) = sort leT (mask m s)}.
proof: Proof. move=> /all_sigP [{}s ->]; case: (mask_sort (leT := le_sT) _ _ s m) => //. by move=> m' m'E; exists m'; rewrite -map_mask !sort_map -map_mask m'E. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)