proposition: Lemma sort_iota_stable n : sorted lt_lex (sort leN (iota 0 n)).
proof: Proof. rewrite sortE. have/andP[]: all (gtn 0) (flatten [::]) && push_invariant [::] by []. elim: n 0 [::] => [|n ihn] m ss hss1 hss2; first exact: pop_stable. apply/ihn/push_stable; last by rewrite /= allrel1l hss1. have: all (gtn m.+1) (flatten ([:: m] :: ss)). by rewrite /= leqnn; apply: sub_all hss1 => ? /leqW. elim: ss [:: _] {hss1 hss2} => [|[|? ?] ? ihss] //= ? ?. by rewrite ihss //= all_cat all_merge -andbA andbCA -!all_cat. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)