proposition: Lemma sortE s : sort s = sort_rec1 [::] s.
proof: Proof. transitivity (sort_rec1 [:: nil] s); last by case: s. rewrite /sort; move: [::] {2}_.+1 (ltnSn (size s)./2) => ss n. by elim: n => // n IHn in ss s *; case: s => [|x [|y s]] //= /IHn->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)