proposition: Lemma sorted_mask_sort s m : sorted leT (mask m s) -> {m_s | mask m_s (sort leT s) = mask m s}.
proof: Proof. by move/(sorted_sort leT_tr) <-; exact: mask_sort. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)