proposition: Lemma pairwise_sort s : pairwise leT s -> sort s = s.
proof: Proof. pose catss := foldr (fun x => cat ^~ x) (Nil T). rewrite -{1 3}[s]/(catss [::] ++ s) sortE; elim: s [::] => /= [|x s ihs] ss. elim: ss [::] => //= s ss ihss t; rewrite -catA => ssst. rewrite -ihss ?allrel_merge //; move: ssst; rewrite !pairwise_cat. by case/and4P. rewrite (catA _ [:: _]) => ssxs. suff x_ss_E: catss (merge_sort_push [:: x] ss) = catss ([:: x] :: ss). by rewrite -[catss _ ++ _]/(catss ([:: x] :: ss)) -x_ss_E ihs // x_ss_E. move: ssxs; rewrite pairwise_cat => /and3P [_ + _]. elim: ss [:: x] => {x s ihs} //= -[|x s] ss ihss t h_pairwise; rewrite /= cats0 // allrel_merge ?ihss ?catA //. by move: h_pairwise; rewrite -catA !pairwise_cat => /and4P []. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)