proposition: Lemma perm_iota_sort (T : Type) (leT : rel T) x0 s : {i_s : seq nat | perm_eq i_s (iota 0 (size s)) & sort leT s = map (nth x0 s) i_s}.
proof: Proof. exists (sort (relpre (nth x0 s) leT) (iota 0 (size s))). by rewrite perm_sort. by rewrite -[s in LHS](mkseq_nth x0) sort_map. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)