proposition: Lemma sorted_mask_sort_in s m : all P s -> sorted leT (mask m s) -> {m_s | mask m_s (sort leT s) = mask m s}.
proof: Proof. move=> ? /(sorted_sort_in leT_tr _) <-; [exact: mask_sort_in | exact: all_mask]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)