proposition: Lemma size_sort (T : Type) (leT : rel T) s : size (sort leT s) = size s.
proof: Proof. case: s => // x s; have [s1 pp qq] := perm_iota_sort leT x (x :: s). by rewrite qq size_map (perm_size pp) size_iota. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)