proposition: Lemma mask_sort s m : {m_s : bitseq | mask m_s (sort leT s) = sort leT (mask m s)}.
proof: Proof. case Ds: {-}s => [|x s1]; [by rewrite Ds; case: m; exists [::] | clear s1 Ds]. rewrite -(mkseq_nth x s) -map_mask !sort_map. exists [seq i \in mask m (iota 0 (size s)) | i <- sort (xrelpre (nth x s) leT) (iota 0 (size s))]. rewrite -map_mask -filter_mask [in RHS]mask_filter ?iota_uniq ?filter_sort //. by move=> ? ? ?; exact: leT_tr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)