proposition: Lemma sorting_sorted n (t : m.-tuple A) : n \is sorting -> sorted <=%O (nfun n t).
proof: Proof. apply: contraLR => /sortedPn[[[x1 x2]][s1 s2] /= nfunE x2Lx1]. rewrite negb_forall. pose g x := if (x <= x2)%O then false else true. have gM : {homo g : x y / (x <= y)%O >-> (x <= y)%O}. move=> i j; rewrite /g. case: (leP i x2); case: (leP j x2) => // jLx2 x2Li. by rewrite leNgt (le_lt_trans jLx2). apply/existsP; exists (tmap g t). apply/sortedPn; exists ((g x1, g x2), (map g s1, map g s2)) => /=. by rewrite -tmap_network // val_tmap nfunE map_cat. by rewrite /g lexx leNgt x2Lx1. Qed.
imports: mathcomp(all_ssreflect perm algebra.zmodp) mathcomp(zify) more_tuple