proposition: Lemma perm_sort s : perm_eql (sort leT s) s.
proof: Proof. apply/permPl; rewrite sortE perm_sym -{1}[s]/(flatten [::] ++ s). elim: s [::] => /= [|x s ihs] ss. - elim: ss [::] => //= s ss ihss t. by rewrite -(permPr (ihss _)) -catA perm_catCA perm_cat2l -perm_merge. - rewrite -(permPr (ihs _)) -(perm_catCA [:: x]) catA perm_cat2r. elim: {x s ihs} ss [:: x] => [|[|x s] ss ihss] t //. by rewrite -(permPr (ihss _)) catA perm_cat2r perm_catC -perm_merge. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)