proposition: Lemma all_sort (T : Type) (P : {pred T}) (leT : rel T) s : all P (sort leT s) = all P s.
proof: Proof. case: s => // x s; move: (x :: s) => {}s. by rewrite -(mkseq_nth x s) sort_map !all_map; apply/perm_all/permPl/perm_sort. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)